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