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 by (rtac 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 by (etac 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 by (etac 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 by (dtac hoare_derivs.Body 1); |
|
71 by (etac 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 by (rtac Body1 1); |
|
78 by (rtac 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 by (rtac 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 by (rtac 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 by (rtac (hoare_derivs.Loop RS conseq2) 1); |
|
94 by (ALLGOALS Simp_tac); |
|
95 by (rtac hoare_derivs.conseq 1); |
|
96 by (Fast_tac 1); |
|
97 qed "LoopF"; |
|
98 |
|
99 (* |
|
100 Goal "[| G'||-ts; G' <= G |] ==> G||-ts"; |
|
101 by (etac hoare_derivs.cut 1); |
|
102 by (etac 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 by (rtac 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.intros) |
|
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 by (rtac BodyN 1); |
|
122 by (etac 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 by (etac finite_induct 1); |
|
134 by (ALLGOALS Clarsimp_tac); |
|
135 by (dtac derivs_insertD 1); |
|
136 by (rtac 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 by (rtac 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 by (rtac 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 by (dtac 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 by (etac 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 Simp_tac, Clarify_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 by (etac 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 by (etac 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 by (dtac 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 by (etac 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 AddSEs WTs_elim_cases; |
|
223 AddIffs [not_None_eq]; |
|
224 (* requires com_det, escape (i.e. hoare_derivs.conseq) *) |
|
225 Goal "state_not_singleton ==> \ |
|
226 \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"; |
|
227 by (induct_tac "c" 1); |
|
228 by (ALLGOALS Clarsimp_tac); |
|
229 by (fast_tac (claset() addIs [(thm"domI")]) 7); |
|
230 by (etac MGT_alternD 6); |
|
231 by (rewtac MGT_def); |
|
232 by (EVERY'[dtac bspec, etac (thm"domI")] 7); |
|
233 by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac |
|
234 [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")] |
|
235 (hoare_derivs.Call RS conseq1), etac conseq12] 7); |
|
236 by (ALLGOALS (etac thin_rl)); |
|
237 by (rtac (hoare_derivs.Skip RS conseq2) 1); |
|
238 by (rtac (hoare_derivs.Ass RS conseq1) 2); |
|
239 by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac |
|
240 [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")] |
|
241 (hoare_derivs.Local RS conseq1), etac conseq12] 3); |
|
242 by (EVERY'[etac hoare_derivs.Comp, etac conseq12] 5); |
|
243 by ((rtac hoare_derivs.If THEN_ALL_NEW etac conseq12) 6); |
|
244 by (EVERY'[rtac (hoare_derivs.Loop RS conseq2), etac conseq12] 8); |
|
245 by Auto_tac; |
|
246 qed_spec_mp "MGF_lemma1"; |
|
247 |
|
248 (* Version: nested single recursion *) |
|
249 |
|
250 Goal "[| !!G ts. ts <= G ==> P G ts;\ |
|
251 \ !!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn};\ |
|
252 \ !!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}; \ |
|
253 \ !!pn. pn : U ==> wt (the (body pn)); \ |
|
254 \ finite U; uG = mgt_call`U |] ==> \ |
|
255 \ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"; |
|
256 by (cut_facts_tac (premises()) 1); |
|
257 by (induct_tac "n" 1); |
|
258 by (ALLGOALS Clarsimp_tac); |
|
259 by (subgoal_tac "G = mgt_call ` U" 1); |
|
260 by (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2); |
|
261 by (Asm_full_simp_tac 1); |
|
262 by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1); |
|
263 by (rtac ballI 1); |
|
264 by (resolve_tac (premises()(*hoare_derivs.asm*)) 1); |
|
265 by (Fast_tac 1); |
|
266 by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1); |
|
267 by (rtac ballI 1); |
|
268 by (case_tac "mgt_call pn : G" 1); |
|
269 by (resolve_tac (premises()(*hoare_derivs.asm*)) 1); |
|
270 by (Fast_tac 1); |
|
271 by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1); |
|
272 by (EVERY [dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]); |
|
273 by (eresolve_tac (tl(tl(tl(premises())))) 3); |
|
274 by (Fast_tac 1); |
|
275 by (dtac finite_subset 1); |
|
276 by (etac finite_imageI 1); |
|
277 by (Asm_simp_tac 1); |
|
278 by (arith_tac 1); |
|
279 qed_spec_mp "nesting_lemma"; |
|
280 |
|
281 Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> \ |
|
282 \ G|-{=}.BODY pn.{->}"; |
|
283 by (rtac BodyN 1); |
|
284 by (etac conseq2 1); |
|
285 by (Force_tac 1); |
|
286 qed "MGT_BodyN"; |
|
287 |
|
288 (* requires BodyN, com_det *) |
|
289 Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c"; |
|
290 by (res_inst_tac [("P","%G ts. G||-ts"),("U","dom body")] nesting_lemma 1); |
|
291 by (etac hoare_derivs.asm 1); |
|
292 by (etac MGT_BodyN 1); |
|
293 by (rtac finite_dom_body 3); |
|
294 by (etac MGF_lemma1 1); |
|
295 by (assume_tac 2); |
|
296 by (Blast_tac 1); |
|
297 by (Clarsimp_tac 1); |
|
298 by (eatac WT_bodiesD 1 1); |
|
299 by (rtac le_refl 3); |
|
300 by Auto_tac; |
|
301 qed "MGF"; |
|
302 |
|
303 |
|
304 (* Version: simultaneous recursion in call rule *) |
|
305 |
|
306 (* finiteness not really necessary here *) |
|
307 Goalw [MGT_def] "[| G Un (%pn. {=}. BODY pn .{->})`Procs \ |
|
308 \ ||-(%pn. {=}. the (body pn) .{->})`Procs; \ |
|
309 \ finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})`Procs"; |
|
310 by (rtac hoare_derivs.Body 1); |
|
311 by (etac finite_pointwise 1); |
|
312 by (assume_tac 2); |
|
313 by (Clarify_tac 1); |
|
314 by (etac conseq2 1); |
|
315 by Auto_tac; |
|
316 qed "MGT_Body"; |
|
317 |
|
318 (* requires empty, insert, com_det *) |
|
319 Goal "[| state_not_singleton; WT_bodies; \ |
|
320 \ F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> \ |
|
321 \ (%pn. {=}. BODY pn .{->})`dom body||-F"; |
|
322 by (ftac finite_subset 1); |
|
323 by (rtac (finite_dom_body RS finite_imageI) 1); |
|
324 by (rotate_tac 2 1); |
|
325 by (make_imp_tac 1); |
|
326 by (etac finite_induct 1); |
|
327 by (ALLGOALS (clarsimp_tac ( |
|
328 claset() addSIs [hoare_derivs.empty,hoare_derivs.insert], |
|
329 simpset() delsimps [range_composition]))); |
|
330 by (etac MGF_lemma1 1); |
|
331 by (fast_tac (claset() addDs [WT_bodiesD]) 2); |
|
332 by (Clarsimp_tac 1); |
|
333 by (rtac hoare_derivs.asm 1); |
|
334 by (fast_tac (claset() addIs [(thm"domI")]) 1); |
|
335 qed_spec_mp "MGF_lemma2_simult"; |
|
336 |
|
337 (* requires Body, empty, insert, com_det *) |
|
338 Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c"; |
|
339 by (rtac MGF_lemma1 1); |
|
340 by (assume_tac 1); |
|
341 by (assume_tac 2); |
|
342 by (Clarsimp_tac 1); |
|
343 by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})`dom body" 1); |
|
344 by (etac hoare_derivs.weaken 1); |
|
345 by (fast_tac (claset() addIs [(thm"domI")]) 1); |
|
346 by (rtac (finite_dom_body RSN (2,MGT_Body)) 1); |
|
347 by (Simp_tac 1); |
|
348 by (eatac MGF_lemma2_simult 1 1); |
|
349 by (rtac subset_refl 1); |
|
350 qed "MGF'"; |
|
351 |
|
352 (* requires Body+empty+insert / BodyN, com_det *) |
|
353 bind_thm ("hoare_complete", MGF' RS MGF_complete); |
|
354 |
|
355 section "unused derived rules"; |
|
356 |
|
357 Goal "G|-{%Z s. False}.c.{Q}"; |
|
358 by (rtac hoare_derivs.conseq 1); |
|
359 by (Fast_tac 1); |
|
360 qed "falseE"; |
|
361 |
|
362 Goal "G|-{P}.c.{%Z s. True}"; |
|
363 by (rtac hoare_derivs.conseq 1); |
|
364 by (fast_tac (claset() addSIs [falseE]) 1); |
|
365 qed "trueI"; |
|
366 |
|
367 Goal "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] \ |
|
368 \ ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}"; |
|
369 by (rtac hoare_derivs.conseq 1); |
|
370 by (fast_tac (claset() addEs [conseq12]) 1); |
|
371 qed "disj"; (* analogue conj non-derivable *) |
|
372 |
|
373 Goal "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}"; |
|
374 by (rtac conseq12 1); |
|
375 by (rtac hoare_derivs.Skip 1); |
|
376 by (Fast_tac 1); |
|
377 qed "hoare_SkipI"; |
|
378 |
|
379 |
|
380 section "useful derived rules"; |
|
381 |
|
382 Goal "{t}|-t"; |
|
383 by (rtac hoare_derivs.asm 1); |
|
384 by (rtac subset_refl 1); |
|
385 qed "single_asm"; |
|
386 |
|
387 Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}"; |
|
388 by (rtac hoare_derivs.conseq 1); |
|
389 by (Clarsimp_tac 1); |
|
390 by (cut_facts_tac (premises()) 1); |
|
391 by (Fast_tac 1); |
|
392 qed "export_s"; |
|
393 |
|
394 |
|
395 Goal "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> \ |
|
396 \ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}"; |
|
397 by (rtac export_s 1); |
|
398 by (rtac hoare_derivs.Local 1); |
|
399 by (etac conseq2 1); |
|
400 by (etac spec 1); |
|
401 qed "weak_Local"; |
|
402 |
|
403 (* |
|
404 Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}"; |
|
405 by (induct_tac "c" 1); |
|
406 by Auto_tac; |
|
407 by (rtac conseq1 1); |
|
408 by (rtac hoare_derivs.Skip 1); |
|
409 force 1; |
|
410 by (rtac conseq1 1); |
|
411 by (rtac hoare_derivs.Ass 1); |
|
412 force 1; |
|
413 by (defer_tac 1); |
|
414 ### |
|
415 by (rtac hoare_derivs.Comp 1); |
|
416 by (dtac spec 2); |
|
417 by (dtac spec 2); |
|
418 by (assume_tac 2); |
|
419 by (etac conseq1 2); |
|
420 by (Clarsimp_tac 2); |
|
421 force 1; |
|
422 *) |
|