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 Main
begin
type_synonym vname = string
type_synonym val = int
type_synonym state = "vname \<Rightarrow> val"
datatype aexp
= N int | V vname | Plus aexp aexp
| Minus aexp aexp | Mul aexp aexp | Div aexp aexp
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" |
"aval (Div a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s div aval a\<^sub>2 s" |
"aval (Mul a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s * aval a\<^sub>2 s" |
"aval (Minus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s - aval a\<^sub>2 s"
definition null_state ("<>") where
"null_state \<equiv> \<lambda>x. 0"
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
"_State ms" == "_Update <> ms"
"_State (_updbinds b bs)" <= "_Update (_State b) bs"
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (\<not> bval b s)" |
"bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \<and> bval b\<^sub>2 s)" |
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
inductive
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2; (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s; (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1; (c,s\<^sub>1) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk>
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3"
code_pred big_step .
declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
thm big_step_induct
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
thm SkipE
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
thm AssignE
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
thm IfE
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
thm WhileE
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
by (induction arbitrary: u rule: big_step.induct) blast+
abbreviation
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
"c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)"
lemma unfold_while:
"(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
proof -
have "(?iw, s) \<Rightarrow> t" if assm: "(?w, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
proof cases
case WhileFalse
thus ?thesis by blast
next
case WhileTrue
from \<open>bval b s\<close> \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq)
with \<open>bval b s\<close> show ?thesis by (rule IfTrue)
qed
qed
moreover
have "(?w, s) \<Rightarrow> t" if assm: "(?iw, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
proof cases
case IfFalse
hence "s = t" using \<open>(?iw, s) \<Rightarrow> t\<close> by blast
thus ?thesis using \<open>\<not>bval b s\<close> by blast
next
case IfTrue
from \<open>(c;; ?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
with \<open>bval b s\<close> show ?thesis by (rule WhileTrue)
qed
qed
ultimately
show ?thesis by blast
qed
paragraph "Hoare"
type_synonym assn = "state \<Rightarrow> bool"
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"
paragraph "Partial correctness"
definition
partial_hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile> {P}c{Q} = (\<forall>s t. P s \<and> (c,s) \<Rightarrow> t \<longrightarrow> Q t)"
inductive
partial_hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
where
partial_Skip: "\<turnstile> {P} SKIP {P}" |
partial_Assign: "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}" |
partial_Seq: "\<lbrakk> \<turnstile> {P} c\<^sub>1 {Q}; \<turnstile> {Q} c\<^sub>2 {R} \<rbrakk>
\<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {R}" |
partial_If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
\<Longrightarrow> \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
partial_While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
\<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}" |
partial_conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
\<Longrightarrow> \<turnstile> {P'} c {Q'}"
lemmas [simp] = partial_hoare.partial_Skip partial_hoare.partial_Assign partial_hoare.partial_Seq partial_If
lemmas [intro!] = partial_hoare.partial_Skip partial_hoare.partial_Assign partial_hoare.partial_Seq partial_hoare.partial_If
lemma partial_strengthen_pre:
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
by (blast intro: partial_conseq)
lemma partial_weaken_post:
"\<lbrakk> \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile> {P} c {Q'}"
by (blast intro: partial_conseq)
lemma partial_Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
by (simp add: partial_strengthen_pre[OF _ partial_Assign])
lemma partial_While':
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
shows "\<turnstile> {P} WHILE b DO c {Q}"
by(rule partial_weaken_post[OF partial_While[OF assms(1)] assms(2)])
definition partial_wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
"partial_wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t \<longrightarrow> Q t)"
lemma partial_wp_SKIP[simp]: "partial_wp SKIP Q = Q"
by (rule ext) (auto simp: partial_wp_def)
lemma partial_wp_Ass[simp]: "partial_wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
by (rule ext) (auto simp: partial_wp_def)
lemma partial_wp_partial_Seq[simp]: "partial_wp (c\<^sub>1;;c\<^sub>2) Q = partial_wp c\<^sub>1 (partial_wp c\<^sub>2 Q)"
by (rule ext) (auto simp: partial_wp_def)
lemma partial_wp_partial_If[simp]:
"partial_wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q =
(\<lambda>s. if bval b s then partial_wp c\<^sub>1 Q s else partial_wp c\<^sub>2 Q s)"
by (rule ext) (auto simp: partial_wp_def)
lemma partial_wp_partial_While_partial_If:
"partial_wp (WHILE b DO c) Q s =
partial_wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
unfolding partial_wp_def by (metis unfold_while)
lemma partial_wp_partial_While_True[simp]: "bval b s \<Longrightarrow>
partial_wp (WHILE b DO c) Q s = partial_wp (c;; WHILE b DO c) Q s"
by(simp add: partial_wp_partial_While_partial_If)
lemma partial_wp_partial_While_False[simp]: "\<not> bval b s \<Longrightarrow> partial_wp (WHILE b DO c) Q s = Q s"
by(simp add: partial_wp_partial_While_partial_If)
lemma partial_wp_is_pre: "\<turnstile> {partial_wp c Q} c {Q}"
proof(induction c arbitrary: Q)
case If thus ?case by(auto intro: partial_hoare.partial_conseq)
next
case (While b c)
let ?w = "WHILE b DO c"
show "\<turnstile> {partial_wp ?w Q} ?w {Q}"
proof(rule partial_While')
show "\<turnstile> {\<lambda>s. partial_wp ?w Q s \<and> bval b s} c {partial_wp ?w Q}"
proof(rule partial_strengthen_pre[OF _ While.IH])
show "\<forall>s. partial_wp ?w Q s \<and> bval b s \<longrightarrow> partial_wp c (partial_wp ?w Q) s" by auto
qed
show "\<forall>s. partial_wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
qed
qed auto
lemma partial_hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
proof(rule partial_strengthen_pre)
show "\<forall>s. P s \<longrightarrow> partial_wp c Q s" using assms
by (auto simp: partial_hoare_valid_def partial_wp_def)
show "\<turnstile> {partial_wp c Q} c {Q}" by(rule partial_wp_is_pre)
qed
paragraph "Annotated commands"
datatype acom =
Askip ("SKIP") |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) |
Aseq acom acom ("_;;/ _" [60, 61] 60) |
Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
Awhile assn bexp acom
("({_}/ WHILE _/ DO _)" [0, 0, 61] 61)
bundle ACOM begin
no_notation SKIP ("SKIP")
no_notation Assign ("_ ::= _" [1000, 61] 61)
no_notation Seq ("_;;/ _" [60, 61] 60)
no_notation If ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
notation Askip ("SKIP")
notation Aassign ("(_ ::= _)" [1000, 61] 61)
notation Aseq ("_;;/ _" [60, 61] 60)
notation Aif ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
end
bundle COM begin
no_notation Askip ("SKIP")
no_notation Aassign ("(_ ::= _)" [1000, 61] 61)
no_notation Aseq ("_;;/ _" [60, 61] 60)
no_notation Aif ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
notation SKIP ("SKIP")
notation Assign ("_ ::= _" [1000, 61] 61)
notation Seq ("_;;/ _" [60, 61] 60)
notation If ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
end
unbundle ACOM
fun strip :: "acom \<Rightarrow> com" where
"strip SKIP = com.SKIP" |
"strip (x ::= a) = com.Assign x a" |
"strip (C\<^sub>1;; C\<^sub>2) = com.Seq (strip C\<^sub>1) (strip C\<^sub>2)" |
"strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = com.If b (strip C\<^sub>1) (strip C\<^sub>2)" |
"strip ({_} WHILE b DO C) = com.While b (strip C)"
paragraph "VCG for partial correctness"
fun partial_pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
"partial_pre SKIP Q = Q" |
"partial_pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
"partial_pre (C\<^sub>1;; C\<^sub>2) Q = partial_pre C\<^sub>1 (partial_pre C\<^sub>2 Q)" |
"partial_pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q =
(\<lambda>s. if bval b s then partial_pre C\<^sub>1 Q s else partial_pre C\<^sub>2 Q s)" |
"partial_pre ({I} WHILE b DO C) Q = I"
fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where
"vc SKIP Q = True" |
"vc (x ::= a) Q = True" |
"vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (partial_pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" |
"vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" |
"vc ({I} WHILE b DO C) Q =
((\<forall>s. (I s \<and> bval b s \<longrightarrow> partial_pre C I s) \<and>
(I s \<and> \<not> bval b s \<longrightarrow> Q s)) \<and>
vc C I)"
lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile> {partial_pre C Q} strip C {Q}"
proof(induction C arbitrary: Q)
case (Awhile I b C)
show ?case
proof(simp, rule partial_While')
from \<open>vc (Awhile I b C) Q\<close>
have vc: "vc C I" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
partial_pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> partial_pre C I s" by simp_all
have "\<turnstile> {partial_pre C I} strip C {I}" by(rule Awhile.IH[OF vc])
with partial_pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip C {I}"
by(rule partial_strengthen_pre)
show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
qed
qed (auto intro: partial_conseq)
corollary vc_sound':
"\<lbrakk> vc C Q; \<forall>s. P s \<longrightarrow> partial_pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}"
by (metis partial_strengthen_pre vc_sound)
unbundle COM
paragraph "Total correctness"
definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))"
inductive
hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
where
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" |
Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" |
Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" |
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
\<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
While:
"(\<And>n::nat.
\<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'<n. T s n')})
\<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>
\<turnstile>\<^sub>t {P'}c{Q'}"
lemma While_fun:
"\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
\<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"
by (rule While [where T="\<lambda>s n. n = f s", simplified])
lemma strengthen_pre:
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
by (metis conseq)
lemma weaken_post:
"\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}"
by (metis conseq)
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])
lemma While_fun':
assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}"
and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
by(blast intro: assms(1) weaken_post[OF While_fun assms(2)])
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
case (While P b T c)
have "\<lbrakk> P s; T s n \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t" for s n
proof(induction "n" arbitrary: s rule: less_induct)
case (less n) thus ?case by (metis While.IH WhileFalse WhileTrue)
qed
thus ?case by auto
next
case If thus ?case by auto blast
qed fastforce+
definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
"wp\<^sub>t c Q = (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
lemma [simp]: "wp\<^sub>t SKIP Q = Q"
by(auto intro!: ext simp: wpt_def)
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
by(auto intro!: ext simp: wpt_def)
lemma [simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
unfolding wpt_def
apply(rule ext)
apply auto
done
lemma [simp]:
"wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q s)"
apply(unfold wpt_def)
apply(rule ext)
apply auto
done
inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where
Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" |
Its_Suc: "\<lbrakk> bval b s; (c,s) \<Rightarrow> s'; Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"
lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
proof(induction arbitrary: n' rule:Its.induct)
case Its_0 thus ?case by(metis Its.cases)
next
case Its_Suc thus ?case by(metis Its.cases big_step_determ)
qed
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by (metis Its_0)
next
case WhileTrue thus ?case by (metis Its_Suc)
qed
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
proof (induction c arbitrary: Q)
case SKIP show ?case by (auto intro:hoaret.Skip)
next
case Assign show ?case by (auto intro:hoaret.Assign)
next
case Seq thus ?case by (auto intro:hoaret.Seq)
next
case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
next
case (While b c)
let ?w = "WHILE b DO c"
let ?T = "Its b c"
have 1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)"
unfolding wpt_def by (metis WHILE_Its)
let ?R = "\<lambda>n s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')"
have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> wp\<^sub>t c (?R n) s" for n
proof -
have "wp\<^sub>t c (?R n) s" if "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t" for s t
proof -
from \<open>bval b s\<close> and \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where
"(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto
from \<open>(?w, s') \<Rightarrow> t\<close> obtain n' where "?T s' n'"
by (blast dest: WHILE_Its)
with \<open>bval b s\<close> and \<open>(c, s) \<Rightarrow> s'\<close> have "?T s (Suc n')" by (rule Its_Suc)
with \<open>?T s n\<close> have "n = Suc n'" by (rule Its_fun)
with \<open>(c,s) \<Rightarrow> s'\<close> and \<open>(?w,s') \<Rightarrow> t\<close> and \<open>Q t\<close> and \<open>?T s' n'\<close>
show ?thesis by (auto simp: wpt_def)
qed
thus ?thesis
unfolding wpt_def by auto
qed
note 2 = hoaret.While[OF strengthen_pre[OF this While.IH]]
have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s"
by (auto simp add:wpt_def)
with 1 2 show ?case by (rule conseq)
qed
theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
apply(rule strengthen_pre[OF _ wpt_is_pre])
apply(auto simp: hoare_tvalid_def wpt_def)
done
corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
by (metis hoaret_sound hoaret_complete)
paragraph "Extra:"
lemma total_imp_partial: "\<turnstile>\<^sub>t {P} c {Q} \<Longrightarrow> \<turnstile> {P} c {Q}"
proof -
assume "\<turnstile>\<^sub>t {P} c {Q}"
then have "\<Turnstile>\<^sub>t {P} c {Q}" by (auto simp: hoaret_sound_complete)
then have "\<Turnstile> {P} c {Q}"
unfolding partial_hoare_valid_def hoare_tvalid_def using big_step_determ by blast
thus "\<turnstile> {P} c {Q}"
by (simp add: partial_hoare_complete)
qed
paragraph \<open>Square Root Program\<close>
unbundle COM
definition "SQRT_vars \<equiv> {''L'',''R'',''M''}"
(*takes lower and upper bound for root*)
definition SQRT :: com where
"SQRT \<equiv>
''L'' ::= N 0;;
''R'' ::= Plus (V ''x'') (N 1);;
WHILE (Less (Plus (V ''L'') (N 1)) (V ''R'')) DO (
''M'' ::= Div (Plus (V ''L'') (V ''R'')) (N 2);;
IF (Less (V ''x'') (Mul (V ''M'') (V ''M'')))
THEN (''R'' ::= V ''M'')
ELSE (''L'' ::= V ''M''))"
unbundle ACOM
definition SQRT_annot :: "(state \<Rightarrow> assn) \<Rightarrow> state \<Rightarrow> acom" where
"SQRT_annot invar sorig \<equiv>
''L'' ::= N 0;;
''R'' ::= Plus (V ''x'') (N 1);;
{invar sorig} WHILE (Less (Plus (V ''L'') (N 1)) (V ''R'')) DO (
''M'' ::= Div (Plus (V ''L'') (V ''R'')) (N 2);;
IF (Less (V ''x'') (Mul (V ''M'') (V ''M'')))
THEN (''R'' ::= V ''M'')
ELSE (''L'' ::= V ''M''))"
unbundle COM
lemma SQRT_annot_strip: "strip (SQRT_annot invar sorig) = SQRT"
unfolding SQRT_annot_def SQRT_def
by auto
consts SQRT_invar :: "state \<Rightarrow> assn"
consts SQRT_measure :: "state \<Rightarrow> nat"
end
theory Submission
imports Defs
begin
definition SQRT_invar :: "state \<Rightarrow> assn" where
"SQRT_invar _ _ = True"
theorem SQRT_partially_correct:
"\<turnstile> {\<lambda>s. s=sorig \<and> 0 \<le> s ''x''}
SQRT
{\<lambda>s. (s ''L'')^2 \<le> s ''x'' \<and> s ''x'' < (s ''L'' + 1)^2 \<and> (\<forall>v. v \<notin> SQRT_vars \<longrightarrow> s v = sorig v)}"
(*Do not changes these lines*)
apply (subst SQRT_annot_strip[of SQRT_invar sorig, symmetric])
apply (rule vc_sound')
(*Complete the proof*)
sorry
definition SQRT_measure :: "state \<Rightarrow> nat" where
"SQRT_measure _ = 0"
lemma SQRT_measure_correct:
assumes "s ''L'' + 1 < s ''R''"
shows "s ''x'' < ((s ''L'' + s ''R'') div 2)^2 \<Longrightarrow>
SQRT_measure (s(''M'' := (s ''L'' + s ''R'') div 2, ''R'' := (s ''L'' + s ''R'') div 2))
< SQRT_measure s"
and "\<not>(s ''x'' < ((s ''L'' + s ''R'') div 2)^2) \<Longrightarrow>
SQRT_measure (s(''M'' := (s ''L'' + s ''R'') div 2, ''L'' := (s ''L'' + s ''R'') div 2))
< SQRT_measure s"
sorry
end
theory Check
imports Submission
begin
theorem SQRT_partially_correct: "\<turnstile> {\<lambda>s. s=sorig \<and> 0 \<le> s ''x''}
SQRT
{\<lambda>s. (s ''L'')^2 \<le> s ''x'' \<and> s ''x'' < (s ''L'' + 1)^2 \<and> (\<forall>v. v \<notin> SQRT_vars \<longrightarrow> s v = sorig v)}"
by (rule Submission.SQRT_partially_correct)
lemma SQRT_measure_correct: "(s ''L'' + 1 < s ''R'') \<Longrightarrow> s ''x'' < ((s ''L'' + s ''R'') div 2)^2 \<Longrightarrow>
SQRT_measure (s(''M'' := (s ''L'' + s ''R'') div 2, ''R'' := (s ''L'' + s ''R'') div 2))
< SQRT_measure s"
by (rule Submission.SQRT_measure_correct)
end