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