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.
theory Defs imports "HOL-IMP.Big_Step" "HOL-Library.Extended_Nat" begin end
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
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