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

### 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