|
1 (* Title: HOL/IMPP/Hoare.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 TUM |
|
5 |
|
6 Soundness and relative completeness of Hoare rules wrt operational semantics |
|
7 *) |
|
8 |
|
9 Goalw [state_not_singleton_def] |
|
10 "state_not_singleton ==> !t. (!s::state. s = t) --> False"; |
|
11 by (Clarify_tac 1); |
|
12 by (case_tac "ta = t" 1); |
|
13 by (ALLGOALS (blast_tac (HOL_cs addDs [not_sym]))); |
|
14 qed "single_stateE"; |
|
15 |
|
16 Addsimps[peek_and_def]; |
|
17 |
|
18 |
|
19 section "validity"; |
|
20 |
|
21 Goalw [triple_valid_def] |
|
22 "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))"; |
|
23 by Auto_tac; |
|
24 qed "triple_valid_def2"; |
|
25 |
|
26 Goal "|=0:{P}. BODY pn .{Q}"; |
|
27 by (simp_tac (simpset() addsimps [triple_valid_def2]) 1); |
|
28 by (Clarsimp_tac 1); |
|
29 qed "Body_triple_valid_0"; |
|
30 |
|
31 (* only ==> direction required *) |
|
32 Goal "|=n:{P}. the (body pn) .{Q} = |=Suc n:{P}. BODY pn .{Q}"; |
|
33 by (simp_tac (simpset() addsimps [triple_valid_def2]) 1); |
|
34 by (Force_tac 1); |
|
35 qed "Body_triple_valid_Suc"; |
|
36 |
|
37 Goalw [triple_valid_def] "|=Suc n:t --> |=n:t"; |
|
38 by (induct_tac "t" 1); |
|
39 by (Simp_tac 1); |
|
40 by (fast_tac (claset() addIs [evaln_Suc]) 1); |
|
41 qed_spec_mp "triple_valid_Suc"; |
|
42 |
|
43 Goal "||=Suc n:ts ==> ||=n:ts"; |
|
44 by (fast_tac (claset() addIs [triple_valid_Suc]) 1); |
|
45 qed "triples_valid_Suc"; |
|
46 |
|
47 |
|
48 section "derived rules"; |
|
49 |
|
50 Goal "[| G|-{P'}.c.{Q'}; !Z s. P Z s --> \ |
|
51 \ (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |] \ |
|
52 \ ==> G|-{P}.c.{Q}"; |
|
53 br hoare_derivs.conseq 1; |
|
54 by (Blast_tac 1); |
|
55 qed "conseq12"; |
|
56 |
|
57 Goal "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}"; |
|
58 be conseq12 1; |
|
59 by (Fast_tac 1); |
|
60 qed "conseq1"; |
|
61 |
|
62 Goal "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}"; |
|
63 be conseq12 1; |
|
64 by (Fast_tac 1); |
|
65 qed "conseq2"; |
|
66 |
|
67 Goal "[| G Un (%p. {P p}. BODY p .{Q p})``Procs \ |
|
68 \ ||- (%p. {P p}. the (body p) .{Q p})``Procs; \ |
|
69 \ pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}"; |
|
70 bd hoare_derivs.Body 1; |
|
71 be hoare_derivs.weaken 1; |
|
72 by (Fast_tac 1); |
|
73 qed "Body1"; |
|
74 |
|
75 Goal "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==> \ |
|
76 \ G|-{P}. BODY pn .{Q}"; |
|
77 br Body1 1; |
|
78 br singletonI 2; |
|
79 by (Clarsimp_tac 1); |
|
80 qed "BodyN"; |
|
81 |
|
82 Goal "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}"; |
|
83 br hoare_derivs.conseq 1; |
|
84 by (Fast_tac 1); |
|
85 qed "escape"; |
|
86 |
|
87 Goal "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}"; |
|
88 br hoare_derivs.conseq 1; |
|
89 by (fast_tac (claset() addDs (premises())) 1); |
|
90 qed "constant"; |
|
91 |
|
92 Goal "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}"; |
|
93 br (hoare_derivs.Loop RS conseq2) 1; |
|
94 by (ALLGOALS Simp_tac); |
|
95 br hoare_derivs.conseq 1; |
|
96 by (Fast_tac 1); |
|
97 qed "LoopF"; |
|
98 |
|
99 (* |
|
100 Goal "[| G'||-ts; G' <= G |] ==> G||-ts"; |
|
101 be hoare_derivs.cut 1; |
|
102 be hoare_derivs.asm 1; |
|
103 qed "thin"; |
|
104 *) |
|
105 Goal "G'||-ts ==> !G. G' <= G --> G||-ts"; |
|
106 by (etac hoare_derivs.induct 1); |
|
107 by (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1])); |
|
108 br hoare_derivs.empty 1; |
|
109 by (eatac hoare_derivs.insert 1 1); |
|
110 by (fast_tac (claset() addIs [hoare_derivs.asm]) 1); |
|
111 by (fast_tac (claset() addIs [hoare_derivs.cut]) 1); |
|
112 by (fast_tac (claset() addIs [hoare_derivs.weaken]) 1); |
|
113 by (EVERY'[rtac hoare_derivs.conseq, strip_tac, smp_tac 2,Clarify_tac, |
|
114 smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1); |
|
115 by (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac] 7); |
|
116 by (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intrs) |
|
117 THEN_ALL_NEW Fast_tac)); |
|
118 qed_spec_mp "thin"; |
|
119 |
|
120 Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"; |
|
121 br BodyN 1; |
|
122 be thin 1; |
|
123 by Auto_tac; |
|
124 qed "weak_Body"; |
|
125 |
|
126 Goal "G||-insert t ts ==> G|-t & G||-ts"; |
|
127 by (fast_tac (claset() addIs [hoare_derivs.weaken]) 1); |
|
128 qed "derivs_insertD"; |
|
129 |
|
130 Goal "[| finite U; \ |
|
131 \ !p. G |- {P' p}.c0 p.{Q' p} --> G |- {P p}.c0 p.{Q p} |] ==> \ |
|
132 \ G||-(%p. {P' p}.c0 p.{Q' p}) `` U --> G||-(%p. {P p}.c0 p.{Q p}) `` U"; |
|
133 be finite_induct 1; |
|
134 by (ALLGOALS Clarsimp_tac); |
|
135 bd derivs_insertD 1; |
|
136 br hoare_derivs.insert 1; |
|
137 by Auto_tac; |
|
138 qed_spec_mp "finite_pointwise"; |
|
139 |
|
140 |
|
141 section "soundness"; |
|
142 |
|
143 Goalw [hoare_valids_def] |
|
144 "G|={P &> b}. c .{P} ==> \ |
|
145 \ G|={P}. WHILE b DO c .{P &> (Not o b)}"; |
|
146 by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1); |
|
147 br allI 1; |
|
148 by (subgoal_tac "!d s s'. <d,s> -n-> s' --> \ |
|
149 \ d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s')" 1); |
|
150 by (EVERY'[etac thin_rl, Fast_tac] 1); |
|
151 by (EVERY'[REPEAT o rtac allI, rtac impI] 1); |
|
152 by ((etac evaln.induct THEN_ALL_NEW Simp_tac) 1); |
|
153 by (ALLGOALS Fast_tac); |
|
154 qed "Loop_sound_lemma"; |
|
155 |
|
156 Goalw [hoare_valids_def] |
|
157 "[| G Un (%pn. {P pn}. BODY pn .{Q pn})``Procs \ |
|
158 \ ||=(%pn. {P pn}. the (body pn) .{Q pn})``Procs |] ==> \ |
|
159 \ G||=(%pn. {P pn}. BODY pn .{Q pn})``Procs"; |
|
160 br allI 1; |
|
161 by (induct_tac "n" 1); |
|
162 by (fast_tac (claset() addIs [Body_triple_valid_0]) 1); |
|
163 by (Clarsimp_tac 1); |
|
164 bd triples_valid_Suc 1; |
|
165 by (mp_tac 1); |
|
166 by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1); |
|
167 by (EVERY'[dtac spec, etac impE, etac conjI, atac] 1); |
|
168 by (fast_tac (claset() addSIs [Body_triple_valid_Suc RS iffD1]) 1); |
|
169 qed "Body_sound_lemma"; |
|
170 |
|
171 Goal "G||-ts ==> G||=ts"; |
|
172 be hoare_derivs.induct 1; |
|
173 by (TRYALL (eresolve_tac [Loop_sound_lemma, Body_sound_lemma] |
|
174 THEN_ALL_NEW atac)); |
|
175 by (rewtac hoare_valids_def); |
|
176 by (Blast_tac 1); |
|
177 by (Blast_tac 1); |
|
178 by (Blast_tac 1); (* asm *) |
|
179 by (Blast_tac 1); (* cut *) |
|
180 by (Blast_tac 1); (* weaken *) |
|
181 by (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", |
|
182 Clarsimp_tac, REPEAT o smp_tac 1])); |
|
183 by (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2]))); |
|
184 by (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *) |
|
185 by (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *) |
|
186 by (Force_tac 3); (* Call *) |
|
187 by (eresolve_tac evaln_elim_cases 2); (* If *) |
|
188 by (TRYALL Blast_tac); |
|
189 qed "hoare_sound"; |
|
190 |
|
191 |
|
192 section "completeness"; |
|
193 |
|
194 (* Both versions *) |
|
195 |
|
196 (*unused*) |
|
197 Goalw [MGT_def] "G|-MGT c ==> \ |
|
198 \ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}"; |
|
199 be conseq12 1; |
|
200 by Auto_tac; |
|
201 qed "MGT_alternI"; |
|
202 |
|
203 (* requires com_det *) |
|
204 Goalw [MGT_def] "state_not_singleton ==> \ |
|
205 \ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c"; |
|
206 be conseq12 1; |
|
207 by Auto_tac; |
|
208 by (case_tac "? t. <c,?s> -c-> t" 1); |
|
209 by (fast_tac (claset() addEs [com_det]) 1); |
|
210 by (Clarsimp_tac 1); |
|
211 bd single_stateE 1; |
|
212 by (Blast_tac 1); |
|
213 qed "MGT_alternD"; |
|
214 |
|
215 Goalw [MGT_def] |
|
216 "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}"; |
|
217 be conseq12 1; |
|
218 by (clarsimp_tac (claset(), simpset() addsimps |
|
219 [hoare_valids_def,eval_eq,triple_valid_def2]) 1); |
|
220 qed "MGF_complete"; |
|
221 |
|
222 val WTs_elim_cases = map WTs.mk_cases |
|
223 ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", |
|
224 "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)", |
|
225 "WT (BODY P)", "WT (X:=CALL P(a))"]; |
|
226 |
|
227 AddSEs WTs_elim_cases; |
|
228 (* requires com_det, escape (i.e. hoare_derivs.conseq) *) |
|
229 Goal "state_not_singleton ==> \ |
|
230 \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"; |
|
231 by (induct_tac "c" 1); |
|
232 by (ALLGOALS Clarsimp_tac); |
|
233 by (fast_tac (claset() addIs [domI]) 7); |
|
234 be MGT_alternD 6; |
|
235 by (rewtac MGT_def); |
|
236 by (EVERY'[dtac bspec, etac domI] 7); |
|
237 by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac |
|
238 [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")] |
|
239 (hoare_derivs.Call RS conseq1), etac conseq12] 7); |
|
240 by (ALLGOALS (etac thin_rl)); |
|
241 br (hoare_derivs.Skip RS conseq2) 1; |
|
242 br (hoare_derivs.Ass RS conseq1) 2; |
|
243 by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac |
|
244 [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")] |
|
245 (hoare_derivs.Local RS conseq1), etac conseq12] 3); |
|
246 by (EVERY'[etac hoare_derivs.Comp, etac conseq12] 5); |
|
247 by ((rtac hoare_derivs.If THEN_ALL_NEW etac conseq12) 6); |
|
248 by (EVERY'[rtac (hoare_derivs.Loop RS conseq2), etac conseq12] 8); |
|
249 by Auto_tac; |
|
250 qed_spec_mp "MGF_lemma1"; |
|
251 |
|
252 (* Version: nested single recursion *) |
|
253 |
|
254 Goal "[| !!G ts. ts <= G ==> P G ts;\ |
|
255 \ !!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn};\ |
|
256 \ !!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}; \ |
|
257 \ !!pn. pn : U ==> wt (the (body pn)); \ |
|
258 \ finite U; uG = mgt_call``U |] ==> \ |
|
259 \ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"; |
|
260 by (cut_facts_tac (premises()) 1); |
|
261 by (induct_tac "n" 1); |
|
262 by (ALLGOALS Clarsimp_tac); |
|
263 bd card_seteq 1; |
|
264 by (Asm_simp_tac 1); |
|
265 be finite_imageI 1; |
|
266 by (Asm_full_simp_tac 1); |
|
267 by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1); |
|
268 br ballI 1; |
|
269 by (resolve_tac (premises()(*hoare_derivs.asm*)) 1); |
|
270 by (Fast_tac 1); |
|
271 by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1); |
|
272 br ballI 1; |
|
273 by (case_tac "mgt_call pn : G" 1); |
|
274 by (resolve_tac (premises()(*hoare_derivs.asm*)) 1); |
|
275 by (Fast_tac 1); |
|
276 by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1); |
|
277 byev[dtac spec 1, etac impE 1, etac impE 2, etac impE 3, dtac spec 4,etac mp 4]; |
|
278 by (eresolve_tac (tl(tl(tl(premises())))) 4); |
|
279 by (Fast_tac 1); |
|
280 be Suc_leD 1; |
|
281 bd finite_subset 1; |
|
282 be finite_imageI 1; |
|
283 by (force_tac (claset() addEs [Suc_diff_Suc], simpset()) 1); |
|
284 qed_spec_mp "nesting_lemma"; |
|
285 |
|
286 Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> \ |
|
287 \ G|-{=}.BODY pn.{->}"; |
|
288 br BodyN 1; |
|
289 be conseq2 1; |
|
290 by (Force_tac 1); |
|
291 qed "MGT_BodyN"; |
|
292 |
|
293 (* requires BodyN, com_det *) |
|
294 Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c"; |
|
295 by (res_inst_tac [("P","%G ts. G||-ts"),("U","dom body")] nesting_lemma 1); |
|
296 be hoare_derivs.asm 1; |
|
297 be MGT_BodyN 1; |
|
298 br finite_dom_body 3; |
|
299 be MGF_lemma1 1; |
|
300 ba 2; |
|
301 by (Blast_tac 1); |
|
302 by (Clarsimp_tac 1); |
|
303 by (eatac WT_bodiesD 1 1); |
|
304 br le_refl 3; |
|
305 by Auto_tac; |
|
306 qed "MGF"; |
|
307 |
|
308 |
|
309 (* Version: simultaneous recursion in call rule *) |
|
310 |
|
311 (* finiteness not really necessary here *) |
|
312 Goalw [MGT_def] "[| G Un (%pn. {=}. BODY pn .{->})``Procs \ |
|
313 \ ||-(%pn. {=}. the (body pn) .{->})``Procs; \ |
|
314 \ finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})``Procs"; |
|
315 br hoare_derivs.Body 1; |
|
316 be finite_pointwise 1; |
|
317 ba 2; |
|
318 by (Clarify_tac 1); |
|
319 be conseq2 1; |
|
320 by Auto_tac; |
|
321 qed "MGT_Body"; |
|
322 |
|
323 (* requires empty, insert, com_det *) |
|
324 Goal "[| state_not_singleton; WT_bodies; \ |
|
325 \ F<=(%pn. {=}.the (body pn).{->})``dom body |] ==> \ |
|
326 \ (%pn. {=}. BODY pn .{->})``dom body||-F"; |
|
327 by (ftac finite_subset 1); |
|
328 br (finite_dom_body RS finite_imageI) 1; |
|
329 by (rotate_tac 2 1); |
|
330 by (make_imp_tac 1); |
|
331 be finite_induct 1; |
|
332 by (ALLGOALS (clarsimp_tac ( |
|
333 claset() addSIs [hoare_derivs.empty,hoare_derivs.insert], |
|
334 simpset() delsimps [range_composition]))); |
|
335 be MGF_lemma1 1; |
|
336 by (fast_tac (claset() addDs [WT_bodiesD]) 2); |
|
337 by (Clarsimp_tac 1); |
|
338 br hoare_derivs.asm 1; |
|
339 by (fast_tac (claset() addIs [domI]) 1); |
|
340 qed_spec_mp "MGF_lemma2_simult"; |
|
341 |
|
342 (* requires Body, empty, insert, com_det *) |
|
343 Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c"; |
|
344 br MGF_lemma1 1; |
|
345 ba 1; |
|
346 ba 2; |
|
347 by (Clarsimp_tac 1); |
|
348 by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})``dom body" 1); |
|
349 be hoare_derivs.weaken 1; |
|
350 by (fast_tac (claset() addIs [domI]) 1); |
|
351 br (finite_dom_body RSN (2,MGT_Body)) 1; |
|
352 by (Simp_tac 1); |
|
353 by (eatac MGF_lemma2_simult 1 1); |
|
354 br subset_refl 1; |
|
355 qed "MGF"; |
|
356 |
|
357 (* requires Body+empty+insert / BodyN, com_det *) |
|
358 bind_thm ("hoare_complete", MGF RS MGF_complete); |
|
359 |
|
360 section "unused derived rules"; |
|
361 |
|
362 Goal "G|-{%Z s. False}.c.{Q}"; |
|
363 br hoare_derivs.conseq 1; |
|
364 by (Fast_tac 1); |
|
365 qed "falseE"; |
|
366 |
|
367 Goal "G|-{P}.c.{%Z s. True}"; |
|
368 br hoare_derivs.conseq 1; |
|
369 by (fast_tac (claset() addSIs [falseE]) 1); |
|
370 qed "trueI"; |
|
371 |
|
372 Goal "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] \ |
|
373 \ ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}"; |
|
374 br hoare_derivs.conseq 1; |
|
375 by (fast_tac (claset() addEs [conseq12]) 1); |
|
376 qed "disj"; (* analogue conj non-derivable *) |
|
377 |
|
378 Goal "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}"; |
|
379 br conseq12 1; |
|
380 br hoare_derivs.Skip 1; |
|
381 by (Fast_tac 1); |
|
382 qed "hoare_SkipI"; |
|
383 |
|
384 |
|
385 section "useful derived rules"; |
|
386 |
|
387 Goal "{t}|-t"; |
|
388 br hoare_derivs.asm 1; |
|
389 br subset_refl 1; |
|
390 qed "single_asm"; |
|
391 |
|
392 Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}"; |
|
393 br hoare_derivs.conseq 1; |
|
394 by (Clarsimp_tac 1); |
|
395 by (cut_facts_tac (premises()) 1); |
|
396 by (Fast_tac 1); |
|
397 qed "export_s"; |
|
398 |
|
399 |
|
400 Goal "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> \ |
|
401 \ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}"; |
|
402 br export_s 1; |
|
403 br hoare_derivs.Local 1; |
|
404 be conseq2 1; |
|
405 be spec 1; |
|
406 qed "weak_Local"; |
|
407 |