author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46582  dcc312f22ee8 
child 48891  c0eafbd55de3 
permissions  rwrr 
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 

37671  16 
text {* The following abstract syntax and semantics of Hoare Logic 
17 
over \texttt{WHILE} programs closely follows the existing tradition 

18 
in Isabelle/HOL of formalizing the presentation given in 

40880  19 
\cite[\S6]{Winskel:1993}. See also @{file "~~/src/HOL/Hoare"} and 
37671  20 
\cite{Nipkow:1998:Winskel}. *} 
10148  21 

41818  22 
type_synonym 'a bexp = "'a set" 
23 
type_synonym 'a assn = "'a set" 

10148  24 

25 
datatype 'a com = 

26 
Basic "'a => 'a" 

27 
 Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60) 

28 
 Cond "'a bexp" "'a com" "'a com" 

29 
 While "'a bexp" "'a assn" "'a com" 

30 

37671  31 
abbreviation Skip ("SKIP") 
32 
where "SKIP == Basic id" 

10148  33 

41818  34 
type_synonym 'a sem = "'a => 'a => bool" 
10148  35 

37671  36 
primrec iter :: "nat => 'a bexp => 'a sem => 'a sem" 
37 
where 

10148  38 
"iter 0 b S s s' = (s ~: b & s = s')" 
37671  39 
 "iter (Suc n) b S s s' = (s : b & (EX s''. S s s'' & iter n b S s'' s'))" 
10148  40 

37671  41 
primrec Sem :: "'a com => 'a sem" 
42 
where 

10148  43 
"Sem (Basic f) s s' = (s' = f s)" 
37671  44 
 "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')" 
45 
 "Sem (Cond b c1 c2) s s' = 

10148  46 
(if s : b then Sem c1 s s' else Sem c2 s s')" 
37671  47 
 "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')" 
10148  48 

46582  49 
definition Valid :: "'a bexp => 'a com => 'a bexp => bool" 
37671  50 
("(3 _/ (2_)/ _)" [100, 55, 100] 50) 
51 
where " P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' > s : P > s' : Q)" 

10148  52 

37671  53 
notation (xsymbols) Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50) 
10148  54 

55 
lemma ValidI [intro?]: 

56 
"(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==>  P c Q" 

57 
by (simp add: Valid_def) 

58 

59 
lemma ValidD [dest?]: 

60 
" P c Q ==> Sem c s s' ==> s : P ==> s' : Q" 

61 
by (simp add: Valid_def) 

62 

63 

64 
subsection {* Primitive Hoare rules *} 

65 

37671  66 
text {* From the semantics defined above, we derive the standard set 
67 
of primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}. 

68 
Usually, variant forms of these rules are applied in actual proof, 

69 
see also \S\ref{sec:hoareisar} and \S\ref{sec:hoarevcg}. 

10148  70 

37671  71 
\medskip The \name{basic} rule represents any kind of atomic access 
72 
to the state space. This subsumes the common rules of \name{skip} 

73 
and \name{assign}, as formulated in \S\ref{sec:hoareisar}. *} 

10148  74 

75 
theorem basic: " {s. f s : P} (Basic f) P" 

76 
proof 

77 
fix s s' assume s: "s : {s. f s : P}" 

78 
assume "Sem (Basic f) s s'" 

37671  79 
then have "s' = f s" by simp 
10148  80 
with s show "s' : P" by simp 
81 
qed 

82 

83 
text {* 

84 
The rules for sequential commands and semantic consequences are 

85 
established in a straight forward manner as follows. 

86 
*} 

87 

88 
theorem seq: " P c1 Q ==>  Q c2 R ==>  P (c1; c2) R" 

89 
proof 

90 
assume cmd1: " P c1 Q" and cmd2: " Q c2 R" 

91 
fix s s' assume s: "s : P" 

92 
assume "Sem (c1; c2) s s'" 

93 
then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'" 

94 
by auto 

95 
from cmd1 sem1 s have "s'' : Q" .. 

96 
with cmd2 sem2 show "s' : R" .. 

97 
qed 

98 

99 
theorem conseq: "P' <= P ==>  P c Q ==> Q <= Q' ==>  P' c Q'" 

100 
proof 

101 
assume P'P: "P' <= P" and QQ': "Q <= Q'" 

102 
assume cmd: " P c Q" 

103 
fix s s' :: 'a 

104 
assume sem: "Sem c s s'" 

105 
assume "s : P'" with P'P have "s : P" .. 

106 
with cmd sem have "s' : Q" .. 

107 
with QQ' show "s' : Q'" .. 

108 
qed 

109 

37671  110 
text {* The rule for conditional commands is directly reflected by the 
111 
corresponding semantics; in the proof we just have to look closely 

112 
which cases apply. *} 

10148  113 

114 
theorem cond: 

46582  115 
assumes case_b: " (P Int b) c1 Q" 
116 
and case_nb: " (P Int b) c2 Q" 

117 
shows " P (Cond b c1 c2) Q" 

10148  118 
proof 
119 
fix s s' assume s: "s : P" 

120 
assume sem: "Sem (Cond b c1 c2) s s'" 

121 
show "s' : Q" 

122 
proof cases 

123 
assume b: "s : b" 

124 
from case_b show ?thesis 

125 
proof 

126 
from sem b show "Sem c1 s s'" by simp 

127 
from s b show "s : P Int b" by simp 

128 
qed 

129 
next 

130 
assume nb: "s ~: b" 

131 
from case_nb show ?thesis 

132 
proof 

133 
from sem nb show "Sem c2 s s'" by simp 

134 
from s nb show "s : P Int b" by simp 

135 
qed 

136 
qed 

137 
qed 

138 

37671  139 
text {* The @{text while} rule is slightly less trivial  it is the 
140 
only one based on recursion, which is expressed in the semantics by 

141 
a Kleenestyle least fixedpoint construction. The auxiliary 

142 
statement below, which is by induction on the number of iterations 

143 
is the main point to be proven; the rest is by routine application 

144 
of the semantics of \texttt{WHILE}. *} 

10148  145 

18241  146 
theorem while: 
147 
assumes body: " (P Int b) c P" 

148 
shows " P (While b X c) (P Int b)" 

10148  149 
proof 
150 
fix s s' assume s: "s : P" 

151 
assume "Sem (While b X c) s s'" 

18241  152 
then obtain n where "iter n b (Sem c) s s'" by auto 
153 
from this and s show "s' : P Int b" 

20503  154 
proof (induct n arbitrary: s) 
19122  155 
case 0 
37671  156 
then show ?case by auto 
11987  157 
next 
19122  158 
case (Suc n) 
11987  159 
then obtain s'' where b: "s : b" and sem: "Sem c s s''" 
37671  160 
and iter: "iter n b (Sem c) s'' s'" by auto 
11987  161 
from Suc and b have "s : P Int b" by simp 
162 
with body sem have "s'' : P" .. 

163 
with iter show ?case by (rule Suc) 

10148  164 
qed 
165 
qed 

166 

167 

168 
subsection {* Concrete syntax for assertions *} 

169 

37671  170 
text {* We now introduce concrete syntax for describing commands (with 
171 
embedded expressions) and assertions. The basic technique is that of 

172 
semantic ``quoteantiquote''. A \emph{quotation} is a syntactic 

173 
entity delimited by an implicit abstraction, say over the state 

174 
space. An \emph{antiquotation} is a marked expression within a 

175 
quotation that refers the implicit argument; a typical antiquotation 

176 
would select (or even update) components from the state. 

10148  177 

37671  178 
We will see some examples later in the concrete rules and 
179 
applications. *} 

10148  180 

37671  181 
text {* The following specification of syntax and translations is for 
182 
Isabelle experts only; feel free to ignore it. 

10148  183 

37671  184 
While the first part is still a somewhat intelligible specification 
185 
of the concrete syntactic representation of our Hoare language, the 

186 
actual ``ML drivers'' is quite involved. Just note that the we 

187 
reuse the basic quote/antiquote translations as already defined in 

42284  188 
Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and 
189 
@{ML Syntax_Trans.quote_tr'},). *} 

10148  190 

191 
syntax 

10874  192 
"_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000) 
193 
"_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000) 

194 
"_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp" 

195 
("_[_'/\<acute>_]" [1000] 999) 

196 
"_Assert" :: "'a => 'a set" ("(.{_}.)" [0] 1000) 

197 
"_Assign" :: "idt => 'b => 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) 

10148  198 
"_Cond" :: "'a bexp => 'a com => 'a com => 'a com" 
199 
("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) 

200 
"_While_inv" :: "'a bexp => 'a assn => 'a com => 'a com" 

201 
("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) 

202 
"_While" :: "'a bexp => 'a com => 'a com" 

203 
("(0WHILE _ //DO _ /OD)" [0, 0] 61) 

204 

205 
syntax (xsymbols) 

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

207 

208 
translations 

35054  209 
".{b}." => "CONST Collect .(b)." 
25706  210 
"B [a/\<acute>x]" => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}." 
35054  211 
"\<acute>x := a" => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))." 
212 
"IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2" 

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

28524  214 
"WHILE b DO c OD" == "WHILE b INV CONST undefined DO c OD" 
10148  215 

216 
parse_translation {* 

217 
let 

42284  218 
fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t 
10148  219 
 quote_tr ts = raise TERM ("quote_tr", ts); 
35113  220 
in [(@{syntax_const "_quote"}, quote_tr)] end 
10148  221 
*} 
222 

37671  223 
text {* As usual in Isabelle syntax translations, the part for 
224 
printing is more complicated  we cannot express parts as macro 

225 
rules as above. Don't look here, unless you have to do similar 

226 
things for yourself. *} 

10148  227 

228 
print_translation {* 

229 
let 

230 
fun quote_tr' f (t :: ts) = 

42284  231 
Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) 
10148  232 
 quote_tr' _ _ = raise Match; 
233 

35113  234 
val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); 
10148  235 

35113  236 
fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = 
10148  237 
quote_tr' (Syntax.const name) (t :: ts) 
238 
 bexp_tr' _ _ = raise Match; 

239 

25706  240 
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = 
42284  241 
quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) 
242 
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) 

10148  243 
 assign_tr' _ = raise Match; 
244 
in 

35113  245 
[(@{const_syntax Collect}, assert_tr'), 
246 
(@{const_syntax Basic}, assign_tr'), 

247 
(@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}), 

248 
(@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})] 

10148  249 
end 
250 
*} 

251 

252 

253 
subsection {* Rules for singlestep proof \label{sec:hoareisar} *} 

254 

37671  255 
text {* We are now ready to introduce a set of Hoare rules to be used 
256 
in singlestep structured proofs in Isabelle/Isar. We refer to the 

257 
concrete syntax introduce above. 

10148  258 

37671  259 
\medskip Assertions of Hoare Logic may be manipulated in 
260 
calculational proofs, with the inclusion expressed in terms of sets 

261 
or predicates. Reversed order is supported as well. *} 

10148  262 

263 
lemma [trans]: " P c Q ==> P' <= P ==>  P' c Q" 

264 
by (unfold Valid_def) blast 

265 
lemma [trans] : "P' <= P ==>  P c Q ==>  P' c Q" 

266 
by (unfold Valid_def) blast 

267 

268 
lemma [trans]: "Q <= Q' ==>  P c Q ==>  P c Q'" 

269 
by (unfold Valid_def) blast 

270 
lemma [trans]: " P c Q ==> Q <= Q' ==>  P c Q'" 

271 
by (unfold Valid_def) blast 

272 

273 
lemma [trans]: 

10838  274 
" .{\<acute>P}. c Q ==> (!!s. P' s > P s) ==>  .{\<acute>P'}. c Q" 
10148  275 
by (simp add: Valid_def) 
276 
lemma [trans]: 

10838  277 
"(!!s. P' s > P s) ==>  .{\<acute>P}. c Q ==>  .{\<acute>P'}. c Q" 
10148  278 
by (simp add: Valid_def) 
279 

280 
lemma [trans]: 

10838  281 
" P c .{\<acute>Q}. ==> (!!s. Q s > Q' s) ==>  P c .{\<acute>Q'}." 
10148  282 
by (simp add: Valid_def) 
283 
lemma [trans]: 

10838  284 
"(!!s. Q s > Q' s) ==>  P c .{\<acute>Q}. ==>  P c .{\<acute>Q'}." 
10148  285 
by (simp add: Valid_def) 
286 

287 

37671  288 
text {* Identity and basic assignments.\footnote{The $\idt{hoare}$ 
289 
method introduced in \S\ref{sec:hoarevcg} is able to provide proper 

290 
instances for any number of basic assignments, without producing 

291 
additional verification conditions.} *} 

10148  292 

293 
lemma skip [intro?]: " P SKIP P" 

294 
proof  

295 
have " {s. id s : P} SKIP P" by (rule basic) 

37671  296 
then show ?thesis by simp 
10148  297 
qed 
298 

42053
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
41818
diff
changeset

299 
lemma assign: " P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P" 
10148  300 
by (rule basic) 
301 

37671  302 
text {* Note that above formulation of assignment corresponds to our 
303 
preferred way to model state spaces, using (extensible) record types 

304 
in HOL \cite{NaraschewskiWenzel:1998:HOOL}. For any record field 

305 
$x$, Isabelle/HOL provides a functions $x$ (selector) and 

306 
$\idt{x{\dsh}update}$ (update). Above, there is only a placeholder 

307 
appearing for the latter kind of function: due to concrete syntax 

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

309 
due to the external nature of HOL record fields, we could not even 

310 
state a general theorem relating selector and update functions (if 

311 
this were required here); this would only work for any particular 

312 
instance of record fields introduced so far.} *} 

10148  313 

37671  314 
text {* Sequential composition  normalizing with associativity 
315 
achieves proper of chunks of code verified separately. *} 

10148  316 

317 
lemmas [trans, intro?] = seq 

318 

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

320 
by (auto simp add: Valid_def) 

321 

37671  322 
text {* Conditional statements. *} 
10148  323 

324 
lemmas [trans, intro?] = cond 

325 

326 
lemma [trans, intro?]: 

10838  327 
" .{\<acute>P & \<acute>b}. c1 Q 
328 
==>  .{\<acute>P & ~ \<acute>b}. c2 Q 

329 
==>  .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q" 

10148  330 
by (rule cond) (simp_all add: Valid_def) 
331 

37671  332 
text {* While statements  with optional invariant. *} 
10148  333 

334 
lemma [intro?]: 

335 
" (P Int b) c P ==>  P (While b P c) (P Int b)" 

336 
by (rule while) 

337 

338 
lemma [intro?]: 

28524  339 
" (P Int b) c P ==>  P (While b undefined c) (P Int b)" 
10148  340 
by (rule while) 
341 

342 

343 
lemma [intro?]: 

10838  344 
" .{\<acute>P & \<acute>b}. c .{\<acute>P}. 
345 
==>  .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}." 

10148  346 
by (simp add: while Collect_conj_eq Collect_neg_eq) 
347 

348 
lemma [intro?]: 

10838  349 
" .{\<acute>P & \<acute>b}. c .{\<acute>P}. 
350 
==>  .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}." 

10148  351 
by (simp add: while Collect_conj_eq Collect_neg_eq) 
352 

353 

354 
subsection {* Verification conditions \label{sec:hoarevcg} *} 

355 

37671  356 
text {* We now load the \emph{original} ML file for proof scripts and 
357 
tactic definition for the Hoare Verification Condition Generator 

40880  358 
(see @{file "~~/src/HOL/Hoare/"}). As far as we 
37671  359 
are concerned here, the result is a proof method \name{hoare}, which 
360 
may be applied to a Hoare Logic assertion to extract purely logical 

361 
verification conditions. It is important to note that the method 

362 
requires \texttt{WHILE} loops to be fully annotated with invariants 

363 
beforehand. Furthermore, only \emph{concrete} pieces of code are 

364 
handled  the underlying tactic fails ungracefully if supplied 

365 
with metavariables or parameters, for example. *} 

10148  366 

13862  367 
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" 
18193  368 
by (auto simp add: Valid_def) 
13862  369 

370 
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q" 

18193  371 
by (auto simp: Valid_def) 
13862  372 

373 
lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R" 

18193  374 
by (auto simp: Valid_def) 
13862  375 

376 
lemma CondRule: 

18193  377 
"p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')} 
378 
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q" 

379 
by (auto simp: Valid_def) 

13862  380 

18241  381 
lemma iter_aux: 
382 
"\<forall>s s'. Sem c s s' > s : I & s : b > s' : I ==> 

18193  383 
(\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)" 
384 
apply(induct n) 

385 
apply clarsimp 

386 
apply (simp (no_asm_use)) 

387 
apply blast 

388 
done 

13862  389 

390 
lemma WhileRule: 

18193  391 
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q" 
392 
apply (clarsimp simp: Valid_def) 

393 
apply (drule iter_aux) 

394 
prefer 2 

395 
apply assumption 

396 
apply blast 

397 
apply blast 

398 
done 

13862  399 

26303  400 
lemma Compl_Collect: " Collect b = {x. \<not> b x}" 
401 
by blast 

402 

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

403 
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

404 

24472
943ef707396c
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
22759
diff
changeset

405 
use "~~/src/HOL/Hoare/hoare_tac.ML" 
10148  406 

407 
method_setup hoare = {* 

30549  408 
Scan.succeed (fn ctxt => 
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
28524
diff
changeset

409 
(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

410 
(hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *} 
10148  411 
"verification condition generator for Hoare logic" 
412 

13703  413 
end 