src/HOL/Isar_examples/Hoare.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 18193 54419506df9e permissions -rw-r--r--
Constant "If" is now local
1 (*  Title:      HOL/Isar_examples/Hoare.thy
2     ID:         $Id$
3     Author:     Markus Wenzel, TU Muenchen
5 A formulation of Hoare logic suitable for Isar.
6 *)
8 header {* Hoare Logic *}
10 theory Hoare imports Main
11 uses ("~~/src/HOL/Hoare/hoare.ML") begin
13 subsection {* Abstract syntax and semantics *}
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
20  \url{http://isabelle.in.tum.de/library/Hoare/} and
21  \cite{Nipkow:1998:Winskel}.
22 *}
24 types
25   'a bexp = "'a set"
26   'a assn = "'a set"
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"
34 syntax
35   "_skip" :: "'a com"    ("SKIP")
36 translations
37   "SKIP" == "Basic id"
39 types
40   'a sem = "'a => 'a => bool"
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'))"
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')"
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"
63 syntax (xsymbols)
64   Valid :: "'a bexp => 'a com => 'a bexp => bool"
65     ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
67 lemma ValidI [intro?]:
68     "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
69   by (simp add: Valid_def)
71 lemma ValidD [dest?]:
72     "|- P c Q ==> Sem c s s' ==> s : P ==> s' : Q"
73   by (simp add: Valid_def)
76 subsection {* Primitive Hoare rules *}
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}.
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 *}
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
97 text {*
98  The rules for sequential commands and semantic consequences are
99  established in a straight forward manner as follows.
100 *}
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
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
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 *}
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
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 *}
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
169   have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
170   proof (induct n)
171     case (0 s)
172     thus ?case by auto
173   next
174     case (Suc n s)
175     then obtain s'' where b: "s : b" and sem: "Sem c s s''"
176       and iter: "iter n b (Sem c) s'' s'"
177       by auto
178     from Suc and b have "s : P Int b" by simp
179     with body sem have "s'' : P" ..
180     with iter show ?case by (rule Suc)
181   qed
182   from this iter s show "s' : P Int -b" .
183 qed
186 subsection {* Concrete syntax for assertions *}
188 text {*
189  We now introduce concrete syntax for describing commands (with
190  embedded expressions) and assertions. The basic technique is that of
191  semantic quote-antiquote''.  A \emph{quotation} is a syntactic
192  entity delimited by an implicit abstraction, say over the state
193  space.  An \emph{antiquotation} is a marked expression within a
194  quotation that refers the implicit argument; a typical antiquotation
195  would select (or even update) components from the state.
197  We will see some examples later in the concrete rules and
198  applications.
199 *}
201 text {*
202  The following specification of syntax and translations is for
203  Isabelle experts only; feel free to ignore it.
205  While the first part is still a somewhat intelligible specification
206  of the concrete syntactic representation of our Hoare language, the
207  actual ML drivers'' is quite involved.  Just note that the we
208  re-use the basic quote/antiquote translations as already defined in
209  Isabelle/Pure (see \verb,Syntax.quote_tr, and
210  \verb,Syntax.quote_tr',).
211 *}
213 syntax
214   "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)"  1000)
215   "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_"  1000)
216   "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
217         ("_[_'/\<acute>_]"  999)
218   "_Assert"      :: "'a => 'a set"           ("(.{_}.)"  1000)
219   "_Assign"      :: "idt => 'b => 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
220   "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"
221         ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
222   "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"
223         ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
224   "_While"       :: "'a bexp => 'a com => 'a com"
225         ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
227 syntax (xsymbols)
228   "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)"  1000)
230 translations
231   ".{b}."                   => "Collect .(b)."
232   "B [a/\<acute>x]"                => ".{\<acute>(_update_name x a) \<in> B}."
233   "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x a))."
234   "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
235   "WHILE b INV i DO c OD"   => "While .{b}. i c"
236   "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
238 parse_translation {*
239   let
240     fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
241       | quote_tr ts = raise TERM ("quote_tr", ts);
242   in [("_quote", quote_tr)] end
243 *}
245 text {*
246  As usual in Isabelle syntax translations, the part for printing is
247  more complicated --- we cannot express parts as macro rules as above.
248  Don't look here, unless you have to do similar things for yourself.
249 *}
251 print_translation {*
252   let
253     fun quote_tr' f (t :: ts) =
254           Term.list_comb (f $Syntax.quote_tr' "_antiquote" t, ts) 255 | quote_tr' _ _ = raise Match; 257 val assert_tr' = quote_tr' (Syntax.const "_Assert"); 259 fun bexp_tr' name ((Const ("Collect", _)$ t) :: ts) =
260           quote_tr' (Syntax.const name) (t :: ts)
261       | bexp_tr' _ _ = raise Match;
263     fun upd_tr' (x_upd, T) =
264       (case try (unsuffix RecordPackage.updateN) x_upd of
265         SOME x => (x, if T = dummyT then T else Term.domain_type T)
266       | NONE => raise Match);
268     fun update_name_tr' (Free x) = Free (upd_tr' x)
269       | update_name_tr' ((c as Const ("_free", _)) $Free x) = 270 c$ Free (upd_tr' x)
271       | update_name_tr' (Const x) = Const (upd_tr' x)
272       | update_name_tr' _ = raise Match;
274     fun assign_tr' (Abs (x, _, f $t$ Bound 0) :: ts) =
275           quote_tr' (Syntax.const "_Assign" $update_name_tr' f) 276 (Abs (x, dummyT, t) :: ts) 277 | assign_tr' _ = raise Match; 278 in 279 [("Collect", assert_tr'), ("Basic", assign_tr'), 280 ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")] 281 end 282 *} 285 subsection {* Rules for single-step proof \label{sec:hoare-isar} *} 287 text {* 288 We are now ready to introduce a set of Hoare rules to be used in 289 single-step structured proofs in Isabelle/Isar. We refer to the 290 concrete syntax introduce above. 292 \medskip Assertions of Hoare Logic may be manipulated in 293 calculational proofs, with the inclusion expressed in terms of sets 294 or predicates. Reversed order is supported as well. 295 *} 297 lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q" 298 by (unfold Valid_def) blast 299 lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q" 300 by (unfold Valid_def) blast 302 lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'" 303 by (unfold Valid_def) blast 304 lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'" 305 by (unfold Valid_def) blast 307 lemma [trans]: 308 "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q" 309 by (simp add: Valid_def) 310 lemma [trans]: 311 "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q" 312 by (simp add: Valid_def) 314 lemma [trans]: 315 "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}." 316 by (simp add: Valid_def) 317 lemma [trans]: 318 "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}." 319 by (simp add: Valid_def) 322 text {* 323 Identity and basic assignments.\footnote{The$\idt{hoare}$method 324 introduced in \S\ref{sec:hoare-vcg} is able to provide proper 325 instances for any number of basic assignments, without producing 326 additional verification conditions.} 327 *} 329 lemma skip [intro?]: "|- P SKIP P" 330 proof - 331 have "|- {s. id s : P} SKIP P" by (rule basic) 332 thus ?thesis by simp 333 qed 335 lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P" 336 by (rule basic) 338 text {* 339 Note that above formulation of assignment corresponds to our 340 preferred way to model state spaces, using (extensible) record types 341 in HOL \cite{Naraschewski-Wenzel:1998:HOOL}. For any record field 342$x$, Isabelle/HOL provides a functions$x$(selector) and 343$\idt{x{\dsh}update}\$ (update).  Above, there is only a place-holder
344  appearing for the latter kind of function: due to concrete syntax
345  \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due
346  to the external nature of HOL record fields, we could not even state
347  a general theorem relating selector and update functions (if this
348  were required here); this would only work for any particular instance
349  of record fields introduced so far.}
350 *}
352 text {*
353  Sequential composition --- normalizing with associativity achieves
354  proper of chunks of code verified separately.
355 *}
357 lemmas [trans, intro?] = seq
359 lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
360   by (auto simp add: Valid_def)
362 text {*
363  Conditional statements.
364 *}
366 lemmas [trans, intro?] = cond
368 lemma [trans, intro?]:
369   "|- .{\<acute>P & \<acute>b}. c1 Q
370       ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
371       ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
372     by (rule cond) (simp_all add: Valid_def)
374 text {*
375  While statements --- with optional invariant.
376 *}
378 lemma [intro?]:
379     "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
380   by (rule while)
382 lemma [intro?]:
383     "|- (P Int b) c P ==> |- P (While b arbitrary c) (P Int -b)"
384   by (rule while)
387 lemma [intro?]:
388   "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
389     ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
390   by (simp add: while Collect_conj_eq Collect_neg_eq)
392 lemma [intro?]:
393   "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
394     ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
395   by (simp add: while Collect_conj_eq Collect_neg_eq)
398 subsection {* Verification conditions \label{sec:hoare-vcg} *}
400 text {*
401  We now load the \emph{original} ML file for proof scripts and tactic
402  definition for the Hoare Verification Condition Generator (see
403  \url{http://isabelle.in.tum.de/library/Hoare/}).  As far as we are
404  concerned here, the result is a proof method \name{hoare}, which may
405  be applied to a Hoare Logic assertion to extract purely logical
406  verification conditions.  It is important to note that the method
407  requires \texttt{WHILE} loops to be fully annotated with invariants
408  beforehand.  Furthermore, only \emph{concrete} pieces of code are
409  handled --- the underlying tactic fails ungracefully if supplied with
410  meta-variables or parameters, for example.
411 *}
413 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
414 by (auto simp:Valid_def)
416 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
417 by (auto simp:Valid_def)
419 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
420 by (auto simp:Valid_def)
422 lemma CondRule:
423  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
424   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
425 by (auto simp:Valid_def)
427 lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
428        (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
429 apply(induct n)
430  apply clarsimp
431 apply(simp (no_asm_use))
432 apply blast
433 done
435 lemma WhileRule:
436  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
437 apply (clarsimp simp:Valid_def)
438 apply(drule iter_aux)
439   prefer 2 apply assumption
440  apply blast
441 apply blast
442 done
445 ML {* val Valid_def = thm "Valid_def" *}
446 use "~~/src/HOL/Hoare/hoare.ML"
448 method_setup hoare = {*
449   Method.no_args
450     (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
451   "verification condition generator for Hoare logic"
453 end