author | wenzelm |
Mon, 02 Nov 2015 13:58:19 +0100 | |
changeset 61541 | 846c72206207 |
parent 58882 | 6e2010ab8bd9 |
child 61799 | 4cf66f21b764 |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Hoare.thy |
10148 | 2 |
Author: Markus Wenzel, TU Muenchen |
3 |
||
4 |
A formulation of Hoare logic suitable for Isar. |
|
5 |
*) |
|
6 |
||
58882 | 7 |
section \<open>Hoare Logic\<close> |
10148 | 8 |
|
31758 | 9 |
theory Hoare |
10 |
imports Main |
|
11 |
begin |
|
10148 | 12 |
|
58614 | 13 |
subsection \<open>Abstract syntax and semantics\<close> |
10148 | 14 |
|
61541 | 15 |
text \<open>The following abstract syntax and semantics of Hoare Logic over |
16 |
\<^verbatim>\<open>WHILE\<close> programs closely follows the existing tradition in Isabelle/HOL |
|
17 |
of formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See |
|
18 |
also @{file "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.\<close> |
|
10148 | 19 |
|
41818 | 20 |
type_synonym 'a bexp = "'a set" |
21 |
type_synonym 'a assn = "'a set" |
|
10148 | 22 |
|
58310 | 23 |
datatype 'a com = |
55656 | 24 |
Basic "'a \<Rightarrow> 'a" |
10148 | 25 |
| Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60) |
26 |
| Cond "'a bexp" "'a com" "'a com" |
|
27 |
| While "'a bexp" "'a assn" "'a com" |
|
28 |
||
37671 | 29 |
abbreviation Skip ("SKIP") |
55656 | 30 |
where "SKIP \<equiv> Basic id" |
10148 | 31 |
|
55656 | 32 |
type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
10148 | 33 |
|
55656 | 34 |
primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem" |
37671 | 35 |
where |
55656 | 36 |
"iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'" |
37 |
| "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')" |
|
10148 | 38 |
|
55656 | 39 |
primrec Sem :: "'a com \<Rightarrow> 'a sem" |
40 |
where |
|
41 |
"Sem (Basic f) s s' \<longleftrightarrow> s' = f s" |
|
42 |
| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')" |
|
43 |
| "Sem (Cond b c1 c2) s s' \<longleftrightarrow> |
|
44 |
(if s \<in> b then Sem c1 s s' else Sem c2 s s')" |
|
45 |
| "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')" |
|
10148 | 46 |
|
55656 | 47 |
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" |
48 |
("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50) |
|
49 |
where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)" |
|
10148 | 50 |
|
51 |
lemma ValidI [intro?]: |
|
55656 | 52 |
"(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q" |
10148 | 53 |
by (simp add: Valid_def) |
54 |
||
55 |
lemma ValidD [dest?]: |
|
55656 | 56 |
"\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q" |
10148 | 57 |
by (simp add: Valid_def) |
58 |
||
59 |
||
58614 | 60 |
subsection \<open>Primitive Hoare rules\<close> |
10148 | 61 |
|
61541 | 62 |
text \<open>From the semantics defined above, we derive the standard set of |
63 |
primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually, |
|
64 |
variant forms of these rules are applied in actual proof, see also |
|
65 |
\S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}. |
|
10148 | 66 |
|
61541 | 67 |
\<^medskip> |
68 |
The \<open>basic\<close> rule represents any kind of atomic access to the state space. |
|
69 |
This subsumes the common rules of \<open>skip\<close> and \<open>assign\<close>, as formulated in |
|
70 |
\S\ref{sec:hoare-isar}.\<close> |
|
10148 | 71 |
|
55656 | 72 |
theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P" |
10148 | 73 |
proof |
55656 | 74 |
fix s s' |
75 |
assume s: "s \<in> {s. f s \<in> P}" |
|
10148 | 76 |
assume "Sem (Basic f) s s'" |
37671 | 77 |
then have "s' = f s" by simp |
55656 | 78 |
with s show "s' \<in> P" by simp |
10148 | 79 |
qed |
80 |
||
58614 | 81 |
text \<open>The rules for sequential commands and semantic consequences are |
61541 | 82 |
established in a straight forward manner as follows.\<close> |
10148 | 83 |
|
55656 | 84 |
theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R" |
10148 | 85 |
proof |
55656 | 86 |
assume cmd1: "\<turnstile> P c1 Q" and cmd2: "\<turnstile> Q c2 R" |
87 |
fix s s' |
|
88 |
assume s: "s \<in> P" |
|
10148 | 89 |
assume "Sem (c1; c2) s s'" |
90 |
then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'" |
|
91 |
by auto |
|
55656 | 92 |
from cmd1 sem1 s have "s'' \<in> Q" .. |
93 |
with cmd2 sem2 show "s' \<in> R" .. |
|
10148 | 94 |
qed |
95 |
||
55656 | 96 |
theorem conseq: "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P' c Q'" |
10148 | 97 |
proof |
55656 | 98 |
assume P'P: "P' \<subseteq> P" and QQ': "Q \<subseteq> Q'" |
99 |
assume cmd: "\<turnstile> P c Q" |
|
10148 | 100 |
fix s s' :: 'a |
101 |
assume sem: "Sem c s s'" |
|
55656 | 102 |
assume "s : P'" with P'P have "s \<in> P" .. |
103 |
with cmd sem have "s' \<in> Q" .. |
|
104 |
with QQ' show "s' \<in> Q'" .. |
|
10148 | 105 |
qed |
106 |
||
58614 | 107 |
text \<open>The rule for conditional commands is directly reflected by the |
61541 | 108 |
corresponding semantics; in the proof we just have to look closely which |
109 |
cases apply.\<close> |
|
10148 | 110 |
|
111 |
theorem cond: |
|
55656 | 112 |
assumes case_b: "\<turnstile> (P \<inter> b) c1 Q" |
113 |
and case_nb: "\<turnstile> (P \<inter> -b) c2 Q" |
|
114 |
shows "\<turnstile> P (Cond b c1 c2) Q" |
|
10148 | 115 |
proof |
55656 | 116 |
fix s s' |
117 |
assume s: "s \<in> P" |
|
10148 | 118 |
assume sem: "Sem (Cond b c1 c2) s s'" |
55656 | 119 |
show "s' \<in> Q" |
10148 | 120 |
proof cases |
55656 | 121 |
assume b: "s \<in> b" |
10148 | 122 |
from case_b show ?thesis |
123 |
proof |
|
124 |
from sem b show "Sem c1 s s'" by simp |
|
55656 | 125 |
from s b show "s \<in> P \<inter> b" by simp |
10148 | 126 |
qed |
127 |
next |
|
55656 | 128 |
assume nb: "s \<notin> b" |
10148 | 129 |
from case_nb show ?thesis |
130 |
proof |
|
131 |
from sem nb show "Sem c2 s s'" by simp |
|
55656 | 132 |
from s nb show "s : P \<inter> -b" by simp |
10148 | 133 |
qed |
134 |
qed |
|
135 |
qed |
|
136 |
||
61541 | 137 |
text \<open>The \<open>while\<close> rule is slightly less trivial --- it is the only one based |
138 |
on recursion, which is expressed in the semantics by a Kleene-style least |
|
139 |
fixed-point construction. The auxiliary statement below, which is by |
|
140 |
induction on the number of iterations is the main point to be proven; the |
|
141 |
rest is by routine application of the semantics of \<^verbatim>\<open>WHILE\<close>.\<close> |
|
10148 | 142 |
|
18241 | 143 |
theorem while: |
55656 | 144 |
assumes body: "\<turnstile> (P \<inter> b) c P" |
145 |
shows "\<turnstile> P (While b X c) (P \<inter> -b)" |
|
10148 | 146 |
proof |
55656 | 147 |
fix s s' assume s: "s \<in> P" |
10148 | 148 |
assume "Sem (While b X c) s s'" |
18241 | 149 |
then obtain n where "iter n b (Sem c) s s'" by auto |
55656 | 150 |
from this and s show "s' \<in> P \<inter> -b" |
20503 | 151 |
proof (induct n arbitrary: s) |
19122 | 152 |
case 0 |
37671 | 153 |
then show ?case by auto |
11987 | 154 |
next |
19122 | 155 |
case (Suc n) |
55656 | 156 |
then obtain s'' where b: "s \<in> b" and sem: "Sem c s s''" |
37671 | 157 |
and iter: "iter n b (Sem c) s'' s'" by auto |
55656 | 158 |
from Suc and b have "s \<in> P \<inter> b" by simp |
159 |
with body sem have "s'' \<in> P" .. |
|
11987 | 160 |
with iter show ?case by (rule Suc) |
10148 | 161 |
qed |
162 |
qed |
|
163 |
||
164 |
||
58614 | 165 |
subsection \<open>Concrete syntax for assertions\<close> |
10148 | 166 |
|
58614 | 167 |
text \<open>We now introduce concrete syntax for describing commands (with |
37671 | 168 |
embedded expressions) and assertions. The basic technique is that of |
61541 | 169 |
semantic ``quote-antiquote''. A \<^emph>\<open>quotation\<close> is a syntactic entity |
170 |
delimited by an implicit abstraction, say over the state space. An |
|
171 |
\<^emph>\<open>antiquotation\<close> is a marked expression within a quotation that refers the |
|
172 |
implicit argument; a typical antiquotation would select (or even update) |
|
173 |
components from the state. |
|
10148 | 174 |
|
61541 | 175 |
We will see some examples later in the concrete rules and applications. |
10148 | 176 |
|
61541 | 177 |
\<^medskip> |
178 |
The following specification of syntax and translations is for Isabelle |
|
179 |
experts only; feel free to ignore it. |
|
10148 | 180 |
|
61541 | 181 |
While the first part is still a somewhat intelligible specification of the |
182 |
concrete syntactic representation of our Hoare language, the actual ``ML |
|
183 |
drivers'' is quite involved. Just note that the we re-use the basic |
|
184 |
quote/antiquote translations as already defined in Isabelle/Pure (see @{ML |
|
185 |
Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},).\<close> |
|
10148 | 186 |
|
187 |
syntax |
|
55662 | 188 |
"_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
189 |
"_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000) |
|
190 |
"_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp" ("_[_'/\<acute>_]" [1000] 999) |
|
191 |
"_Assert" :: "'a \<Rightarrow> 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000) |
|
192 |
"_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
|
193 |
"_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" |
|
194 |
("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) |
|
195 |
"_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" |
|
196 |
("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) |
|
197 |
"_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0WHILE _ //DO _ /OD)" [0, 0] 61) |
|
10148 | 198 |
|
199 |
translations |
|
55662 | 200 |
"\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect (_quote b)" |
201 |
"B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>" |
|
202 |
"\<acute>x := a" \<rightharpoonup> "CONST Basic (_quote (\<acute>(_update_name x (\<lambda>_. a))))" |
|
55656 | 203 |
"IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2" |
55662 | 204 |
"WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c" |
205 |
"WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD" |
|
10148 | 206 |
|
58614 | 207 |
parse_translation \<open> |
10148 | 208 |
let |
42284 | 209 |
fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t |
10148 | 210 |
| quote_tr ts = raise TERM ("quote_tr", ts); |
52143 | 211 |
in [(@{syntax_const "_quote"}, K quote_tr)] end |
58614 | 212 |
\<close> |
10148 | 213 |
|
61541 | 214 |
text \<open>As usual in Isabelle syntax translations, the part for printing is |
215 |
more complicated --- we cannot express parts as macro rules as above. |
|
216 |
Don't look here, unless you have to do similar things for yourself.\<close> |
|
10148 | 217 |
|
58614 | 218 |
print_translation \<open> |
10148 | 219 |
let |
220 |
fun quote_tr' f (t :: ts) = |
|
42284 | 221 |
Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) |
10148 | 222 |
| quote_tr' _ _ = raise Match; |
223 |
||
35113 | 224 |
val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); |
10148 | 225 |
|
35113 | 226 |
fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
10148 | 227 |
quote_tr' (Syntax.const name) (t :: ts) |
228 |
| bexp_tr' _ _ = raise Match; |
|
229 |
||
25706 | 230 |
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
42284 | 231 |
quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) |
232 |
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) |
|
10148 | 233 |
| assign_tr' _ = raise Match; |
234 |
in |
|
52143 | 235 |
[(@{const_syntax Collect}, K assert_tr'), |
236 |
(@{const_syntax Basic}, K assign_tr'), |
|
237 |
(@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})), |
|
238 |
(@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))] |
|
10148 | 239 |
end |
58614 | 240 |
\<close> |
10148 | 241 |
|
242 |
||
58614 | 243 |
subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close> |
10148 | 244 |
|
61541 | 245 |
text \<open>We are now ready to introduce a set of Hoare rules to be used in |
246 |
single-step structured proofs in Isabelle/Isar. We refer to the concrete |
|
247 |
syntax introduce above. |
|
10148 | 248 |
|
61541 | 249 |
\<^medskip> |
250 |
Assertions of Hoare Logic may be manipulated in calculational proofs, with |
|
251 |
the inclusion expressed in terms of sets or predicates. Reversed order is |
|
252 |
supported as well.\<close> |
|
10148 | 253 |
|
55656 | 254 |
lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q" |
10148 | 255 |
by (unfold Valid_def) blast |
55656 | 256 |
lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P' c Q" |
10148 | 257 |
by (unfold Valid_def) blast |
258 |
||
55656 | 259 |
lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P c Q'" |
10148 | 260 |
by (unfold Valid_def) blast |
55656 | 261 |
lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q'" |
10148 | 262 |
by (unfold Valid_def) blast |
263 |
||
264 |
lemma [trans]: |
|
55656 | 265 |
"\<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q" |
10148 | 266 |
by (simp add: Valid_def) |
267 |
lemma [trans]: |
|
55656 | 268 |
"(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q" |
10148 | 269 |
by (simp add: Valid_def) |
270 |
||
271 |
lemma [trans]: |
|
55656 | 272 |
"\<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>" |
10148 | 273 |
by (simp add: Valid_def) |
274 |
lemma [trans]: |
|
55656 | 275 |
"(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>" |
10148 | 276 |
by (simp add: Valid_def) |
277 |
||
278 |
||
61541 | 279 |
text \<open>Identity and basic assignments.\footnote{The \<open>hoare\<close> method introduced |
280 |
in \S\ref{sec:hoare-vcg} is able to provide proper instances for any |
|
281 |
number of basic assignments, without producing additional verification |
|
282 |
conditions.}\<close> |
|
10148 | 283 |
|
55656 | 284 |
lemma skip [intro?]: "\<turnstile> P SKIP P" |
10148 | 285 |
proof - |
55656 | 286 |
have "\<turnstile> {s. id s \<in> P} SKIP P" by (rule basic) |
37671 | 287 |
then show ?thesis by simp |
10148 | 288 |
qed |
289 |
||
55656 | 290 |
lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P" |
10148 | 291 |
by (rule basic) |
292 |
||
58614 | 293 |
text \<open>Note that above formulation of assignment corresponds to our |
61541 | 294 |
preferred way to model state spaces, using (extensible) record types in |
295 |
HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>, |
|
296 |
Isabelle/HOL provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update). |
|
297 |
Above, there is only a place-holder appearing for the latter kind of |
|
298 |
function: due to concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains |
|
299 |
\<open>x_update\<close>.\footnote{Note that due to the external nature of HOL record |
|
300 |
fields, we could not even state a general theorem relating selector and |
|
301 |
update functions (if this were required here); this would only work for |
|
302 |
any particular instance of record fields introduced so far.} |
|
10148 | 303 |
|
61541 | 304 |
\<^medskip> |
305 |
Sequential composition --- normalizing with associativity achieves proper |
|
306 |
of chunks of code verified separately.\<close> |
|
10148 | 307 |
|
308 |
lemmas [trans, intro?] = seq |
|
309 |
||
55656 | 310 |
lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q" |
10148 | 311 |
by (auto simp add: Valid_def) |
312 |
||
58614 | 313 |
text \<open>Conditional statements.\<close> |
10148 | 314 |
|
315 |
lemmas [trans, intro?] = cond |
|
316 |
||
317 |
lemma [trans, intro?]: |
|
55656 | 318 |
"\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c1 Q |
319 |
\<Longrightarrow> \<turnstile> \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace> c2 Q |
|
320 |
\<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q" |
|
10148 | 321 |
by (rule cond) (simp_all add: Valid_def) |
322 |
||
58614 | 323 |
text \<open>While statements --- with optional invariant.\<close> |
10148 | 324 |
|
55662 | 325 |
lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)" |
10148 | 326 |
by (rule while) |
327 |
||
55662 | 328 |
lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)" |
10148 | 329 |
by (rule while) |
330 |
||
331 |
||
332 |
lemma [intro?]: |
|
55656 | 333 |
"\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace> |
334 |
\<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b INV \<lbrace>\<acute>P\<rbrace> DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>" |
|
10148 | 335 |
by (simp add: while Collect_conj_eq Collect_neg_eq) |
336 |
||
337 |
lemma [intro?]: |
|
55656 | 338 |
"\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace> |
339 |
\<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>" |
|
10148 | 340 |
by (simp add: while Collect_conj_eq Collect_neg_eq) |
341 |
||
342 |
||
58614 | 343 |
subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close> |
10148 | 344 |
|
61541 | 345 |
text \<open>We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic |
346 |
definition for the Hoare Verification Condition Generator (see @{file |
|
347 |
"~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a |
|
348 |
proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to |
|
349 |
extract purely logical verification conditions. It is important to note |
|
350 |
that the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with |
|
351 |
invariants beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are |
|
352 |
handled --- the underlying tactic fails ungracefully if supplied with |
|
353 |
meta-variables or parameters, for example.\<close> |
|
10148 | 354 |
|
13862 | 355 |
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" |
18193 | 356 |
by (auto simp add: Valid_def) |
13862 | 357 |
|
358 |
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q" |
|
18193 | 359 |
by (auto simp: Valid_def) |
13862 | 360 |
|
361 |
lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R" |
|
18193 | 362 |
by (auto simp: Valid_def) |
13862 | 363 |
|
364 |
lemma CondRule: |
|
18193 | 365 |
"p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')} |
366 |
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q" |
|
367 |
by (auto simp: Valid_def) |
|
13862 | 368 |
|
18241 | 369 |
lemma iter_aux: |
55656 | 370 |
"\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow> |
371 |
(\<And>s s'. s \<in> I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> I \<and> s' \<notin> b)" |
|
372 |
by (induct n) auto |
|
13862 | 373 |
|
374 |
lemma WhileRule: |
|
18193 | 375 |
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q" |
376 |
apply (clarsimp simp: Valid_def) |
|
377 |
apply (drule iter_aux) |
|
378 |
prefer 2 |
|
379 |
apply assumption |
|
380 |
apply blast |
|
381 |
apply blast |
|
382 |
done |
|
13862 | 383 |
|
26303 | 384 |
lemma Compl_Collect: "- Collect b = {x. \<not> b x}" |
385 |
by blast |
|
386 |
||
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
26303
diff
changeset
|
387 |
lemmas AbortRule = SkipRule -- "dummy version" |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
26303
diff
changeset
|
388 |
|
48891 | 389 |
ML_file "~~/src/HOL/Hoare/hoare_tac.ML" |
10148 | 390 |
|
58614 | 391 |
method_setup hoare = |
392 |
\<open>Scan.succeed (fn ctxt => |
|
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
28524
diff
changeset
|
393 |
(SIMPLE_METHOD' |
58614 | 394 |
(Hoare.hoare_tac ctxt |
395 |
(simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))\<close> |
|
10148 | 396 |
"verification condition generator for Hoare logic" |
397 |
||
13703 | 398 |
end |