Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Homework 9

This is the task corresponding to homework 9.

Resources

Download Files

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

Terms and Conditions