author | nipkow |
Sat, 23 Jul 2016 13:25:44 +0200 | |
changeset 63538 | d7b5e2a222c2 |
parent 54809 | 319358e48bb1 |
child 67019 | 7a3724078363 |
permissions | -rw-r--r-- |
43158 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
54809
diff
changeset
|
3 |
subsection \<open>Soundness and Completeness\<close> |
43158 | 4 |
|
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
54809
diff
changeset
|
5 |
theory Hoare_Sound_Complete |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
54809
diff
changeset
|
6 |
imports Hoare |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
54809
diff
changeset
|
7 |
begin |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
54809
diff
changeset
|
8 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
54809
diff
changeset
|
9 |
subsubsection "Soundness" |
43158 | 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 |
|
52168 | 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 |
|
52168 | 20 |
using While.IH unfolding hoare_valid_def by blast |
43158 | 21 |
qed |
22 |
} |
|
23 |
thus ?case unfolding hoare_valid_def by blast |
|
24 |
qed (auto simp: hoare_valid_def) |
|
25 |
||
26 |
||
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
54809
diff
changeset
|
27 |
subsubsection "Weakest Precondition" |
43158 | 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 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52373
diff
changeset
|
38 |
lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)" |
43158 | 39 |
by (rule ext) (auto simp: wp_def) |
40 |
||
41 |
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
|
42 |
"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
|
43 |
(\<lambda>s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)" |
43158 | 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 |
||
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
54809
diff
changeset
|
59 |
subsubsection "Completeness" |
43158 | 60 |
|
61 |
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}" |
|
45015 | 62 |
proof(induction c arbitrary: Q) |
52373 | 63 |
case If thus ?case by(auto intro: conseq) |
43158 | 64 |
next |
65 |
case (While b c) |
|
66 |
let ?w = "WHILE b DO c" |
|
52193 | 67 |
show "\<turnstile> {wp ?w Q} ?w {Q}" |
68 |
proof(rule While') |
|
43158 | 69 |
show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}" |
52193 | 70 |
proof(rule strengthen_pre[OF _ While.IH]) |
43158 | 71 |
show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto |
72 |
qed |
|
73 |
show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto |
|
74 |
qed |
|
75 |
qed auto |
|
76 |
||
52291 | 77 |
lemma hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}" |
43158 | 78 |
proof(rule strengthen_pre) |
79 |
show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms |
|
80 |
by (auto simp: hoare_valid_def wp_def) |
|
81 |
show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre) |
|
82 |
qed |
|
83 |
||
54809 | 84 |
corollary hoare_sound_complete: "\<turnstile> {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}" |
85 |
by (metis hoare_complete hoare_sound) |
|
86 |
||
43158 | 87 |
end |