author | haftmann |
Fri, 01 Nov 2013 18:51:14 +0100 | |
changeset 54230 | b1d955791529 |
parent 53015 | a1119cf551e8 |
child 54809 | 319358e48bb1 |
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 |
|
52168 | 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 |
|
52168 | 16 |
using While.IH unfolding hoare_valid_def by blast |
43158 | 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 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52373
diff
changeset
|
34 |
lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)" |
43158 | 35 |
by (rule ext) (auto simp: wp_def) |
36 |
||
37 |
lemma wp_If[simp]: |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52373
diff
changeset
|
38 |
"wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52373
diff
changeset
|
39 |
(\<lambda>s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)" |
43158 | 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) |
52373 | 59 |
case If thus ?case by(auto intro: conseq) |
43158 | 60 |
next |
61 |
case (While b c) |
|
62 |
let ?w = "WHILE b DO c" |
|
52193 | 63 |
show "\<turnstile> {wp ?w Q} ?w {Q}" |
64 |
proof(rule While') |
|
43158 | 65 |
show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}" |
52193 | 66 |
proof(rule strengthen_pre[OF _ While.IH]) |
43158 | 67 |
show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto |
68 |
qed |
|
69 |
show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto |
|
70 |
qed |
|
71 |
qed auto |
|
72 |
||
52291 | 73 |
lemma hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}" |
43158 | 74 |
proof(rule strengthen_pre) |
75 |
show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms |
|
76 |
by (auto simp: hoare_valid_def wp_def) |
|
77 |
show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre) |
|
78 |
qed |
|
79 |
||
80 |
end |