author | nipkow |
Fri, 17 May 2013 08:19:52 +0200 | |
changeset 52046 | bc01725d7918 |
parent 47818 | 151d137f1095 |
child 52165 | b8ea3e7a1b07 |
permissions | -rw-r--r-- |
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 |
||
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
47818
diff
changeset
|
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 = |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
47818
diff
changeset
|
48 |
wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s" |
43158 | 49 |
unfolding wp_def by (metis unfold_while) |
50 |
||
51 |
lemma wp_While_True[simp]: "bval b s \<Longrightarrow> |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
47818
diff
changeset
|
52 |
wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s" |
43158 | 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 |