summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/Hoare.thy

author | oheimb |

Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) | |

changeset 11008 | f7333f055ef6 |

parent 10874 | ad7113530c32 |

child 11987 | bf31b35949ce |

permissions | -rw-r--r-- |

improved theory reference in comment

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 = Main

11 files ("~~/src/HOL/Hoare/Hoare.ML"):

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

19 \cite[\S6]{Winskel:1993}. See also

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 (symbols)

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

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 }

187 qed

188 from this iter s show "s' : P Int -b" .

189 qed

192 subsection {* Concrete syntax for assertions *}

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.

203 We will see some examples later in the concrete rules and

204 applications.

205 *}

207 text {*

208 The following specification of syntax and translations is for

209 Isabelle experts only; feel free to ignore it.

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 *}

219 syntax

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)

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)

233 syntax (xsymbols)

234 "_Assert" :: "'a => 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)

236 translations

237 ".{b}." => "Collect .(b)."

238 "B [a/\<acute>x]" => ".{\<acute>(_update_name x a) \<in> B}."

239 "\<acute>x := a" => "Basic .(\<acute>(_update_name x a))."

240 "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"

241 "WHILE b INV i DO c OD" => "While .{b}. i c"

242 "WHILE b DO c OD" == "WHILE b INV arbitrary DO c OD"

244 parse_translation {*

245 let

246 fun quote_tr [t] = Syntax.quote_tr "_antiquote" t

247 | quote_tr ts = raise TERM ("quote_tr", ts);

248 in [("_quote", quote_tr)] end

249 *}

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 *}

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;

263 val assert_tr' = quote_tr' (Syntax.const "_Assert");

265 fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =

266 quote_tr' (Syntax.const name) (t :: ts)

267 | bexp_tr' _ _ = raise Match;

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);

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;

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 *}

291 subsection {* Rules for single-step proof \label{sec:hoare-isar} *}

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.

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 *}

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

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

313 lemma [trans]:

314 "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"

315 by (simp add: Valid_def)

316 lemma [trans]:

317 "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"

318 by (simp add: Valid_def)

320 lemma [trans]:

321 "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."

322 by (simp add: Valid_def)

323 lemma [trans]:

324 "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."

325 by (simp add: Valid_def)

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 *}

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

341 lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"

342 by (rule basic)

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

351 \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due

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 *}

358 text {*

359 Sequential composition --- normalizing with associativity achieves

360 proper of chunks of code verified separately.

361 *}

363 lemmas [trans, intro?] = seq

365 lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"

366 by (auto simp add: Valid_def)

368 text {*

369 Conditional statements.

370 *}

372 lemmas [trans, intro?] = cond

374 lemma [trans, intro?]:

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"

378 by (rule cond) (simp_all add: Valid_def)

380 text {*

381 While statements --- with optional invariant.

382 *}

384 lemma [intro?]:

385 "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"

386 by (rule while)

388 lemma [intro?]:

389 "|- (P Int b) c P ==> |- P (While b arbitrary c) (P Int -b)"

390 by (rule while)

393 lemma [intro?]:

394 "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.

395 ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."

396 by (simp add: while Collect_conj_eq Collect_neg_eq)

398 lemma [intro?]:

399 "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.

400 ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."

401 by (simp add: while Collect_conj_eq Collect_neg_eq)

404 subsection {* Verification conditions \label{sec:hoare-vcg} *}

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 *}

419 ML {* val Valid_def = thm "Valid_def" *}

420 use "~~/src/HOL/Hoare/Hoare.ML"

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"

427 end