35754
|
1 |
(* Title: HOL/IMP/Hoare_Def.thy
|
|
2 |
Author: Tobias Nipkow
|
|
3 |
*)
|
|
4 |
|
|
5 |
header "Soundness and Completeness wrt Denotational Semantics"
|
|
6 |
|
|
7 |
theory Hoare_Den imports Hoare Denotation begin
|
|
8 |
|
|
9 |
definition
|
|
10 |
hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
|
|
11 |
"|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
|
|
12 |
|
|
13 |
|
|
14 |
lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
|
|
15 |
proof(induct rule: hoare.induct)
|
|
16 |
case (While P b c)
|
|
17 |
{ fix s t
|
|
18 |
let ?G = "Gamma b (C c)"
|
|
19 |
assume "(s,t) \<in> lfp ?G"
|
|
20 |
hence "P s \<longrightarrow> P t \<and> \<not> b t"
|
|
21 |
proof(rule lfp_induct2)
|
|
22 |
show "mono ?G" by(rule Gamma_mono)
|
|
23 |
next
|
|
24 |
fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
|
|
25 |
thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
|
|
26 |
by(auto simp: hoare_valid_def Gamma_def)
|
|
27 |
qed
|
|
28 |
}
|
|
29 |
thus ?case by(simp add:hoare_valid_def)
|
|
30 |
qed (auto simp: hoare_valid_def)
|
|
31 |
|
|
32 |
|
|
33 |
definition
|
|
34 |
wp :: "com => assn => assn" where
|
|
35 |
"wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
|
|
36 |
|
|
37 |
lemma wp_SKIP: "wp \<SKIP> Q = Q"
|
|
38 |
by (simp add: wp_def)
|
|
39 |
|
|
40 |
lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
|
|
41 |
by (simp add: wp_def)
|
|
42 |
|
|
43 |
lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
|
|
44 |
by (rule ext) (auto simp: wp_def)
|
|
45 |
|
|
46 |
lemma wp_If:
|
|
47 |
"wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
|
|
48 |
by (rule ext) (auto simp: wp_def)
|
|
49 |
|
|
50 |
lemma wp_While_If:
|
|
51 |
"wp (\<WHILE> b \<DO> c) Q s =
|
|
52 |
wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
|
|
53 |
by(simp only: wp_def C_While_If)
|
|
54 |
|
|
55 |
(*Not suitable for rewriting: LOOPS!*)
|
|
56 |
lemma wp_While_if:
|
|
57 |
"wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
|
|
58 |
by(simp add:wp_While_If wp_If wp_SKIP)
|
|
59 |
|
|
60 |
lemma wp_While_True: "b s ==>
|
|
61 |
wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
|
|
62 |
by(simp add: wp_While_if)
|
|
63 |
|
|
64 |
lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
|
|
65 |
by(simp add: wp_While_if)
|
|
66 |
|
|
67 |
lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
|
|
68 |
|
|
69 |
lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
|
|
70 |
(s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
|
|
71 |
apply (simp (no_asm))
|
|
72 |
apply (rule iffI)
|
|
73 |
apply (rule weak_coinduct)
|
|
74 |
apply (erule CollectI)
|
|
75 |
apply safe
|
|
76 |
apply simp
|
|
77 |
apply simp
|
|
78 |
apply (simp add: wp_def Gamma_def)
|
|
79 |
apply (intro strip)
|
|
80 |
apply (rule mp)
|
|
81 |
prefer 2 apply (assumption)
|
|
82 |
apply (erule lfp_induct2)
|
|
83 |
apply (fast intro!: monoI)
|
|
84 |
apply (subst gfp_unfold)
|
|
85 |
apply (fast intro!: monoI)
|
|
86 |
apply fast
|
|
87 |
done
|
|
88 |
|
|
89 |
declare C_while [simp del]
|
|
90 |
|
|
91 |
lemma wp_is_pre: "|- {wp c Q} c {Q}"
|
|
92 |
proof(induct c arbitrary: Q)
|
|
93 |
case SKIP show ?case by auto
|
|
94 |
next
|
|
95 |
case Assign show ?case by auto
|
|
96 |
next
|
|
97 |
case Semi thus ?case by auto
|
|
98 |
next
|
|
99 |
case (Cond b c1 c2)
|
|
100 |
let ?If = "IF b THEN c1 ELSE c2"
|
|
101 |
show ?case
|
|
102 |
proof(rule If)
|
|
103 |
show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
|
|
104 |
proof(rule strengthen_pre[OF _ Cond(1)])
|
|
105 |
show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
|
|
106 |
qed
|
|
107 |
show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
|
|
108 |
proof(rule strengthen_pre[OF _ Cond(2)])
|
|
109 |
show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
|
|
110 |
qed
|
|
111 |
qed
|
|
112 |
next
|
|
113 |
case (While b c)
|
|
114 |
let ?w = "WHILE b DO c"
|
|
115 |
show ?case
|
|
116 |
proof(rule While')
|
|
117 |
show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
|
|
118 |
proof(rule strengthen_pre[OF _ While(1)])
|
|
119 |
show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
|
|
120 |
qed
|
|
121 |
show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
|
|
122 |
qed
|
|
123 |
qed
|
|
124 |
|
|
125 |
lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
|
|
126 |
proof(rule conseq)
|
|
127 |
show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
|
|
128 |
by (auto simp: hoare_valid_def wp_def)
|
|
129 |
show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
|
|
130 |
show "\<forall>s. Q s \<longrightarrow> Q s" by auto
|
|
131 |
qed
|
|
132 |
|
|
133 |
end
|