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 |
|
47818
|
38 |
lemma wp_Seq[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
|
43158
|
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)
|
47818
|
63 |
case Seq thus ?case by(auto intro: Seq)
|
43158
|
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
|