author | nipkow |
Mon, 27 May 2013 07:42:10 +0200 | |
changeset 52165 | b8ea3e7a1b07 |
parent 52046 | bc01725d7918 |
child 52168 | 785d39ee8753 |
permissions | -rw-r--r-- |
43158 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Hoare_Sound_Complete imports Hoare begin |
|
4 |
||
5 |
subsection "Soundness" |
|
6 |
||
7 |
lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}" |
|
45015 | 8 |
proof(induction rule: hoare.induct) |
43158 | 9 |
case (While P b c) |
10 |
{ fix s t |
|
11 |
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> P s \<longrightarrow> P t \<and> \<not> bval b t" |
|
45015 | 12 |
proof(induction "WHILE b DO c" s t rule: big_step_induct) |
43158 | 13 |
case WhileFalse thus ?case by blast |
14 |
next |
|
15 |
case WhileTrue thus ?case |
|
16 |
using While(2) unfolding hoare_valid_def by blast |
|
17 |
qed |
|
18 |
} |
|
19 |
thus ?case unfolding hoare_valid_def by blast |
|
20 |
qed (auto simp: hoare_valid_def) |
|
21 |
||
22 |
||
23 |
subsection "Weakest Precondition" |
|
24 |
||
25 |
definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where |
|
26 |
"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t \<longrightarrow> Q t)" |
|
27 |
||
28 |
lemma wp_SKIP[simp]: "wp SKIP Q = Q" |
|
29 |
by (rule ext) (auto simp: wp_def) |
|
30 |
||
31 |
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))" |
|
32 |
by (rule ext) (auto simp: wp_def) |
|
33 |
||
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
47818
diff
changeset
|
34 |
lemma wp_Seq[simp]: "wp (c\<^isub>1;;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)" |
43158 | 35 |
by (rule ext) (auto simp: wp_def) |
36 |
||
37 |
lemma wp_If[simp]: |
|
38 |
"wp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = |
|
39 |
(\<lambda>s. (bval b s \<longrightarrow> wp c\<^isub>1 Q s) \<and> (\<not> bval b s \<longrightarrow> wp c\<^isub>2 Q s))" |
|
40 |
by (rule ext) (auto simp: wp_def) |
|
41 |
||
42 |
lemma wp_While_If: |
|
43 |
"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
|
44 |
wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s" |
43158 | 45 |
unfolding wp_def by (metis unfold_while) |
46 |
||
47 |
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
|
48 |
wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s" |
43158 | 49 |
by(simp add: wp_While_If) |
50 |
||
51 |
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s" |
|
52 |
by(simp add: wp_While_If) |
|
53 |
||
54 |
||
55 |
subsection "Completeness" |
|
56 |
||
57 |
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}" |
|
45015 | 58 |
proof(induction c arbitrary: Q) |
47818 | 59 |
case Seq thus ?case by(auto intro: Seq) |
43158 | 60 |
next |
61 |
case (If b c1 c2) |
|
62 |
let ?If = "IF b THEN c1 ELSE c2" |
|
63 |
show ?case |
|
64 |
proof(rule hoare.If) |
|
65 |
show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}" |
|
66 |
proof(rule strengthen_pre[OF _ If(1)]) |
|
67 |
show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto |
|
68 |
qed |
|
69 |
show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}" |
|
70 |
proof(rule strengthen_pre[OF _ If(2)]) |
|
71 |
show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto |
|
72 |
qed |
|
73 |
qed |
|
74 |
next |
|
75 |
case (While b c) |
|
76 |
let ?w = "WHILE b DO c" |
|
77 |
have "\<turnstile> {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> bval b s}" |
|
78 |
proof(rule hoare.While) |
|
79 |
show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}" |
|
80 |
proof(rule strengthen_pre[OF _ While(1)]) |
|
81 |
show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto |
|
82 |
qed |
|
83 |
qed |
|
84 |
thus ?case |
|
85 |
proof(rule weaken_post) |
|
86 |
show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto |
|
87 |
qed |
|
88 |
qed auto |
|
89 |
||
90 |
lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}" |
|
91 |
proof(rule strengthen_pre) |
|
92 |
show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms |
|
93 |
by (auto simp: hoare_valid_def wp_def) |
|
94 |
show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre) |
|
95 |
qed |
|
96 |
||
97 |
end |