43158

1 
(* Author: Tobias Nipkow *)


2 


3 
theory Hoare_Sound_Complete imports Hoare begin


4 


5 
subsection "Soundness"


6 


7 
definition


8 
hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where


9 
"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"


10 


11 
lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}"

45015

12 
proof(induction rule: hoare.induct)

43158

13 
case (While P b c)


14 
{ fix s t


15 
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> P s \<longrightarrow> P t \<and> \<not> bval b t"

45015

16 
proof(induction "WHILE b DO c" s t rule: big_step_induct)

43158

17 
case WhileFalse thus ?case by blast


18 
next


19 
case WhileTrue thus ?case


20 
using While(2) unfolding hoare_valid_def by blast


21 
qed


22 
}


23 
thus ?case unfolding hoare_valid_def by blast


24 
qed (auto simp: hoare_valid_def)


25 


26 


27 
subsection "Weakest Precondition"


28 


29 
definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where


30 
"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t \<longrightarrow> Q t)"


31 


32 
lemma wp_SKIP[simp]: "wp SKIP Q = Q"


33 
by (rule ext) (auto simp: wp_def)


34 


35 
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"


36 
by (rule ext) (auto simp: wp_def)


37 


38 
lemma wp_Semi[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"


39 
by (rule ext) (auto simp: wp_def)


40 


41 
lemma wp_If[simp]:


42 
"wp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =


43 
(\<lambda>s. (bval b s \<longrightarrow> wp c\<^isub>1 Q s) \<and> (\<not> bval b s \<longrightarrow> wp c\<^isub>2 Q s))"


44 
by (rule ext) (auto simp: wp_def)


45 


46 
lemma wp_While_If:


47 
"wp (WHILE b DO c) Q s =


48 
wp (IF b THEN c;WHILE b DO c ELSE SKIP) Q s"


49 
unfolding wp_def by (metis unfold_while)


50 


51 
lemma wp_While_True[simp]: "bval b s \<Longrightarrow>


52 
wp (WHILE b DO c) Q s = wp (c; WHILE b DO c) Q s"


53 
by(simp add: wp_While_If)


54 


55 
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"


56 
by(simp add: wp_While_If)


57 


58 


59 
subsection "Completeness"


60 


61 
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"

45015

62 
proof(induction c arbitrary: Q)

43158

63 
case Semi thus ?case by(auto intro: Semi)


64 
next


65 
case (If b c1 c2)


66 
let ?If = "IF b THEN c1 ELSE c2"


67 
show ?case


68 
proof(rule hoare.If)


69 
show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}"


70 
proof(rule strengthen_pre[OF _ If(1)])


71 
show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto


72 
qed


73 
show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}"


74 
proof(rule strengthen_pre[OF _ If(2)])


75 
show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto


76 
qed


77 
qed


78 
next


79 
case (While b c)


80 
let ?w = "WHILE b DO c"


81 
have "\<turnstile> {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> bval b s}"


82 
proof(rule hoare.While)


83 
show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"


84 
proof(rule strengthen_pre[OF _ While(1)])


85 
show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto


86 
qed


87 
qed


88 
thus ?case


89 
proof(rule weaken_post)


90 
show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto


91 
qed


92 
qed auto


93 


94 
lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"


95 
proof(rule strengthen_pre)


96 
show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms


97 
by (auto simp: hoare_valid_def wp_def)


98 
show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)


99 
qed


100 


101 
end
