Homework 9

Definitions File

theory Defs imports "HOL-IMP.Big_Step" "HOL-Library.Extended_Nat" begin



end

Template File

theory Submission imports Defs begin

theorem fixp:
  assumes "inj (f :: 'a ⇒ 'b)" and "inj (g :: 'b ⇒ 'a)"
  shows "∃h :: 'a ⇒ 'b. inj h ∧ surj h"
proof
  define S where "S ≡ lfp (λX. - (g ` (- (f ` X))))"
  let ?g' = "inv g"
  define h where "h ≡ λz. if z ∈ S then f z else ?g' z"

  have "S = - (g ` (- (f ` S)))"
    sorry
  have *: "?g' ` (- S) = - (f ` S)"
    sorry
  show "inj h ∧ surj h"
  proof
    from * show "surj h"
      sorry
    have "inj_on f S"
      sorry
    moreover have "inj_on ?g' (- S)"
      sorry
    moreover {
      fix a b
      assume "a ∈ S" "b ∈ - S" and eq: "f a = ?g' b"
      have False
        sorry
    } ultimately show "inj h"
      sorry
  qed
qed

paragraph "Step 1"

inductive
  big_step_t :: "com × state ⇒ nat ⇒ state ⇒ bool"  ("_ ⇒^/_ _" 55)
where
Skip: "(SKIP, s) ⇒^1 s" |
Assign: "(x ::= a,s) ⇒^1 s(x := aval a s)" |
Seq: "⟦ (c⇩1,s⇩1) ⇒^n⇩1 s⇩2;  (c⇩2,s⇩2) ⇒^n⇩2 s⇩3; n⇩1+n⇩2 = n⇩3 ⟧ ⟹ (c⇩1;;c⇩2, s⇩1) ⇒^n⇩3 s⇩3" |
IfTrue: "⟦ bval b s;  (c⇩1,s) ⇒^n⇩1 t; n⇩3 = Suc n⇩1 ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒^n⇩3 t" |
IfFalse: "⟦ ¬bval b s;  (c⇩2,s) ⇒^n⇩2 t; n⇩3 = Suc n⇩2 ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒^n⇩3 t" |
WhileFalse: "⟦ ¬bval b s ⟧ ⟹ (WHILE b DO c, s) ⇒^1 s" |
WhileTrue:
"⟦ bval b s⇩1;  (c,s⇩1) ⇒^n⇩1 s⇩2;  (WHILE b DO c, s⇩2) ⇒^n⇩2 s⇩3; n⇩1+n⇩2+1 = n⇩3 ⟧
  ⟹ (WHILE b DO c, s⇩1) ⇒^n⇩3 s⇩3"

declare [[syntax_ambiguity_warning = false]]

code_pred big_step_t .

values "{(t, n). (SKIP, λ_. 0) ⇒^n t}"

text ‹We need to translate the result state into a list to display it.›

values "{map t [''x''] |t x. (SKIP, <''x'' := 42>) ⇒^x t}"

values "{map t [''x''] |t x. (''x'' ::= N 2, <''x'' := 42>) ⇒^x t}"

values "{map t [''x'',''y''] |t x.
  (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
   <''x'' := 0, ''y'' := 13>) ⇒^x t}"


declare big_step_t.intros[intro]

thm big_step_t.induct

lemmas big_step_t_induct = big_step_t.induct[split_format(complete)]
thm big_step_t_induct

inductive_cases Skip_tE[elim!]: "(SKIP,s) ⇒^x t"
inductive_cases Assign_tE[elim!]: "(x ::= a,s) ⇒^p t"
inductive_cases Seq_tE[elim!]: "(c⇩1;;c⇩2,s⇩1) ⇒^p s⇩3"
inductive_cases If_tE[elim!]: "(IF b THEN c⇩1 ELSE c⇩2,s) ⇒^x t"
inductive_cases While_tE[elim]: "(WHILE b DO c,s) ⇒^x t"

paragraph "Step 2"

value "3::enat" ―‹3›
value "∞::enat" ―‹‹∞››
value "(3::enat) + 4" ―‹7›
value "(3::enat) + ∞" ―‹‹∞››
value "eSuc 3" ―‹4›
value "eSuc ∞" ―‹‹∞››

paragraph "Step 3"

type_synonym assn = "state ⇒ bool"
type_synonym qassn = "state ⇒ enat"

fun emb :: "bool ⇒ enat" ("↓") where
   "emb False = ∞"
 | "emb True = 0"

definition hoare_Qvalid :: "qassn ⇒ com ⇒ qassn ⇒ bool"
  ("⊨⇩Q {(1_)}/ (_)/ {(1_)}" 50) where
"⊨⇩Q {P} c {Q}  ⟷  (∀s.  P s < ∞ ⟶ (∃t p. ((c,s) ⇒^p t) ∧ P s ≥ p + Q t))"

abbreviation state_subst :: "state ⇒ aexp ⇒ vname ⇒ state"
  ("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

inductive hoareQ :: "qassn ⇒ com ⇒ qassn ⇒ bool" ("⊢⇩Q ({(1_)}/ (_)/ {(1_)})" 50) where
SkipQ:  "⊢⇩Q {λs. eSuc (P s)} SKIP {P}"  |
AssignQ:  "⊢⇩Q {λs. eSuc (P (s[a/x]))} x::=a {P}"  |
IfQ: "⟦ ⊢⇩Q {λs. P s + ↓( bval b s)} c⇩1 {Q};
       ⊢⇩Q {λs. P s + ↓(¬ bval b s)} c⇩2 {Q} ⟧
  ⟹ ⊢⇩Q {λs. eSuc (P s)} IF b THEN c⇩1 ELSE c⇩2 {Q}"  |
SeqQ: "⟦ ⊢⇩Q {P⇩1} c⇩1 {P⇩2}; ⊢⇩Q {P⇩2} c⇩2 {P⇩3}⟧ ⟹ ⊢⇩Q {P⇩1} c⇩1;;c⇩2 {P⇩3}"  |
WhileQ:
  "⊢⇩Q {λs. I s + ↓(bval b s)} c {λt. I t + 1}
   ⟹ ⊢⇩Q {λs. I s + 1} WHILE b DO c {λs. I s + ↓(¬ bval b s)}" |
conseqQ: "⟦ ⊢⇩Q {P} c {Q}; ⋀s. P s ≤ P' s; ⋀s. Q' s ≤ Q s ⟧ ⟹
           ⊢⇩Q {P'} c {Q'}"

lemma strengthen_pre: "⟦ ∀s. P s ≤ P' s;  ⊢⇩Q {P} c {Q} ⟧ ⟹ ⊢⇩Q {P'} c {Q}"
  using conseqQ by blast

lemma AssignQ': "∀s. P s ≥ eSuc (Q(s[a/x])) ⟹ ⊢⇩Q {P} x ::= a {Q}"
  by (simp add: strengthen_pre[OF _ AssignQ])

paragraph "Step 4"

definition wsum :: com where
"wsum =
  ''y'' ::= N 0;;
  WHILE Less (N 0) (V ''x'')
  DO (''y'' ::= Plus (V ''y'') (V ''x'');;
      ''x'' ::= Plus (V ''x'') (N (- 1)))"

theorem wsum: "⊢⇩Q {λs. enat (2 + 3*n) + ↓ (s ''x'' = int n)} wsum {λs. 0}"
unfolding wsum_def
apply(rule SeqQ[rotated])
 apply(rule conseqQ)
   apply(rule WhileQ[where I="λs. enat (3 * nat (s ''x''))"])
 sorry

paragraph "Step 5"

lemma Skip_sound: "⊨⇩Q {λa. eSuc (P a)} SKIP {P}"
unfolding hoare_Qvalid_def proof (safe)
  fix s assume "eSuc (P s) < ∞"
  then have "(SKIP, s) ⇒^1 s ∧ enat 1 + P s ≤ eSuc (P s)"
    using Skip  eSuc_def by (auto split: enat.splits)
  thus "∃t n. (SKIP, s) ⇒^n t ∧ enat n + P t ≤ eSuc (P s)"
    by blast
qed


lemma Assign_sound: "⊨⇩Q {λb. eSuc (P (b[a/x]))} x::=a {P}"
  sorry

lemma conseq_sound:
  assumes hyps: "⋀s. P s ≤ P' s" "⋀s. Q' s ≤ Q s"
  assumes IH: "⊨⇩Q {P} c {Q}"
  shows "⊨⇩Q {P'} c {Q'}"
  sorry


lemma If_sound:
  assumes "⊨⇩Q {λa. P a + ↓ (bval b a)} c⇩1 {Q}"
  assumes " ⊨⇩Q {λa. P a + ↓ (¬ bval b a)} c⇩2 {Q}"
  shows"⊨⇩Q {λa. eSuc (P a)} IF b THEN c⇩1 ELSE c⇩2 {Q}"
  sorry


lemma Seq_sound:
  assumes "⊨⇩Q {P⇩1} c⇩1 {P⇩2}"
  assumes "⊨⇩Q {P⇩2} c⇩2 {P⇩3}"
  shows "⊨⇩Q {P⇩1} c⇩1;;c⇩2 {P⇩3}"
  sorry


theorem hoareQ_sound: "⊢⇩Q {P} c {Q} ⟹ ⊨⇩Q {P} c {Q}"
  oops

end

Check File

theory Check imports Submission begin

theorem
  assumes "inj (f :: 'a \<Rightarrow> 'b)" and "inj (g :: 'b \<Rightarrow> 'a)"
  shows "\<exists>h :: 'a \<Rightarrow> 'b. inj h \<and> surj h"
  using assms by (rule Submission.fixp)

theorem wsum: "\<turnstile>\<^sub>Q {\<lambda>s. enat (2 + 3*n) + \<down> (s ''x'' = int n)} wsum {\<lambda>s. 0}"
  by (rule Submission.wsum)

lemma Assign_sound: "\<Turnstile>\<^sub>Q {\<lambda>b. eSuc (P (b[a/x]))} x::=a {P}"
  by (rule Submission.Assign_sound)

lemma conseq_sound:
  assumes hyps: "\<And>s. P s \<le> P' s" "\<And>s. Q' s \<le> Q s"
  assumes IH: "\<Turnstile>\<^sub>Q {P} c {Q}"
  shows "\<Turnstile>\<^sub>Q {P'} c {Q'}"
  using assms by (rule Submission.conseq_sound)

lemma If_sound:
  assumes "\<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (bval b a)} c\<^sub>1 {Q}"
  assumes " \<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (\<not> bval b a)} c\<^sub>2 {Q}"
  shows"\<Turnstile>\<^sub>Q {\<lambda>a. eSuc (P a)} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"
  using assms by (rule Submission.If_sound)

lemma Seq_sound:
  assumes "\<Turnstile>\<^sub>Q {P\<^sub>1} c\<^sub>1 {P\<^sub>2}"
  assumes "\<Turnstile>\<^sub>Q {P\<^sub>2} c\<^sub>2 {P\<^sub>3}"
  shows "\<Turnstile>\<^sub>Q {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}"
  using assms by (rule Submission.Seq_sound)

end