8177
|
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 |
|
17477
|
9 |
Goalw [state_not_singleton_def]
|
|
10 |
"state_not_singleton ==> !t. (!s::state. s = t) --> False";
|
8177
|
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 |
|
17477
|
21 |
Goalw [triple_valid_def]
|
8177
|
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}";
|
10962
|
53 |
by (rtac hoare_derivs.conseq 1);
|
8177
|
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}";
|
10962
|
58 |
by (etac conseq12 1);
|
8177
|
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}";
|
10962
|
63 |
by (etac conseq12 1);
|
8177
|
64 |
by (Fast_tac 1);
|
|
65 |
qed "conseq2";
|
|
66 |
|
10834
|
67 |
Goal "[| G Un (%p. {P p}. BODY p .{Q p})`Procs \
|
|
68 |
\ ||- (%p. {P p}. the (body p) .{Q p})`Procs; \
|
8177
|
69 |
\ pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}";
|
10962
|
70 |
by (dtac hoare_derivs.Body 1);
|
|
71 |
by (etac hoare_derivs.weaken 1);
|
8177
|
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}";
|
10962
|
77 |
by (rtac Body1 1);
|
|
78 |
by (rtac singletonI 2);
|
8177
|
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}";
|
10962
|
83 |
by (rtac hoare_derivs.conseq 1);
|
8177
|
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}";
|
10962
|
88 |
by (rtac hoare_derivs.conseq 1);
|
8177
|
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}";
|
10962
|
93 |
by (rtac (hoare_derivs.Loop RS conseq2) 1);
|
8177
|
94 |
by (ALLGOALS Simp_tac);
|
10962
|
95 |
by (rtac hoare_derivs.conseq 1);
|
8177
|
96 |
by (Fast_tac 1);
|
|
97 |
qed "LoopF";
|
|
98 |
|
|
99 |
(*
|
|
100 |
Goal "[| G'||-ts; G' <= G |] ==> G||-ts";
|
10962
|
101 |
by (etac hoare_derivs.cut 1);
|
|
102 |
by (etac hoare_derivs.asm 1);
|
8177
|
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]));
|
17477
|
108 |
by (rtac hoare_derivs.empty 1);
|
8177
|
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,
|
17477
|
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));
|
8177
|
118 |
qed_spec_mp "thin";
|
|
119 |
|
|
120 |
Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}";
|
10962
|
121 |
by (rtac BodyN 1);
|
|
122 |
by (etac thin 1);
|
8177
|
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} |] ==> \
|
10834
|
132 |
\ G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U";
|
10962
|
133 |
by (etac finite_induct 1);
|
8177
|
134 |
by (ALLGOALS Clarsimp_tac);
|
10962
|
135 |
by (dtac derivs_insertD 1);
|
|
136 |
by (rtac hoare_derivs.insert 1);
|
8177
|
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);
|
10962
|
147 |
by (rtac allI 1);
|
8177
|
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]
|
10834
|
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";
|
10962
|
160 |
by (rtac allI 1);
|
8177
|
161 |
by (induct_tac "n" 1);
|
|
162 |
by (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
|
|
163 |
by (Clarsimp_tac 1);
|
10962
|
164 |
by (dtac triples_valid_Suc 1);
|
8177
|
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";
|
10962
|
172 |
by (etac hoare_derivs.induct 1);
|
8177
|
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 *)
|
17477
|
181 |
by (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs",
|
|
182 |
Simp_tac, Clarify_tac, REPEAT o smp_tac 1]));
|
8177
|
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}";
|
10962
|
199 |
by (etac conseq12 1);
|
8177
|
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";
|
10962
|
206 |
by (etac conseq12 1);
|
8177
|
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);
|
10962
|
211 |
by (dtac single_stateE 1);
|
8177
|
212 |
by (Blast_tac 1);
|
|
213 |
qed "MGT_alternD";
|
|
214 |
|
17477
|
215 |
Goalw [MGT_def]
|
8177
|
216 |
"{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}";
|
10962
|
217 |
by (etac conseq12 1);
|
17477
|
218 |
by (clarsimp_tac (claset(), simpset() addsimps
|
8177
|
219 |
[hoare_valids_def,eval_eq,triple_valid_def2]) 1);
|
|
220 |
qed "MGF_complete";
|
|
221 |
|
|
222 |
AddSEs WTs_elim_cases;
|
18447
|
223 |
AddIffs [not_None_eq];
|
8177
|
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);
|
13911
|
229 |
by (fast_tac (claset() addIs [(thm"domI")]) 7);
|
10962
|
230 |
by (etac MGT_alternD 6);
|
8177
|
231 |
by (rewtac MGT_def);
|
13911
|
232 |
by (EVERY'[dtac bspec, etac (thm"domI")] 7);
|
17477
|
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);
|
8177
|
236 |
by (ALLGOALS (etac thin_rl));
|
10962
|
237 |
by (rtac (hoare_derivs.Skip RS conseq2) 1);
|
|
238 |
by (rtac (hoare_derivs.Ass RS conseq1) 2);
|
17477
|
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);
|
8177
|
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)); \
|
10834
|
254 |
\ finite U; uG = mgt_call`U |] ==> \
|
8177
|
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);
|
10834
|
259 |
by (subgoal_tac "G = mgt_call ` U" 1);
|
9078
|
260 |
by (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2);
|
8177
|
261 |
by (Asm_full_simp_tac 1);
|
|
262 |
by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
|
10962
|
263 |
by (rtac ballI 1);
|
8177
|
264 |
by (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
|
|
265 |
by (Fast_tac 1);
|
|
266 |
by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
|
10962
|
267 |
by (rtac ballI 1);
|
8177
|
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);
|
17956
|
272 |
by (EVERY [dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]);
|
13612
|
273 |
by (eresolve_tac (tl(tl(tl(premises())))) 3);
|
8177
|
274 |
by (Fast_tac 1);
|
10962
|
275 |
by (dtac finite_subset 1);
|
|
276 |
by (etac finite_imageI 1);
|
17477
|
277 |
by (Asm_simp_tac 1);
|
10962
|
278 |
by (arith_tac 1);
|
8177
|
279 |
qed_spec_mp "nesting_lemma";
|
|
280 |
|
|
281 |
Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> \
|
|
282 |
\ G|-{=}.BODY pn.{->}";
|
10962
|
283 |
by (rtac BodyN 1);
|
|
284 |
by (etac conseq2 1);
|
8177
|
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);
|
10962
|
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);
|
8177
|
296 |
by (Blast_tac 1);
|
|
297 |
by (Clarsimp_tac 1);
|
|
298 |
by (eatac WT_bodiesD 1 1);
|
10962
|
299 |
by (rtac le_refl 3);
|
8177
|
300 |
by Auto_tac;
|
|
301 |
qed "MGF";
|
|
302 |
|
|
303 |
|
|
304 |
(* Version: simultaneous recursion in call rule *)
|
|
305 |
|
|
306 |
(* finiteness not really necessary here *)
|
10834
|
307 |
Goalw [MGT_def] "[| G Un (%pn. {=}. BODY pn .{->})`Procs \
|
|
308 |
\ ||-(%pn. {=}. the (body pn) .{->})`Procs; \
|
|
309 |
\ finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})`Procs";
|
10962
|
310 |
by (rtac hoare_derivs.Body 1);
|
|
311 |
by (etac finite_pointwise 1);
|
|
312 |
by (assume_tac 2);
|
8177
|
313 |
by (Clarify_tac 1);
|
10962
|
314 |
by (etac conseq2 1);
|
8177
|
315 |
by Auto_tac;
|
|
316 |
qed "MGT_Body";
|
|
317 |
|
|
318 |
(* requires empty, insert, com_det *)
|
|
319 |
Goal "[| state_not_singleton; WT_bodies; \
|
10834
|
320 |
\ F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> \
|
|
321 |
\ (%pn. {=}. BODY pn .{->})`dom body||-F";
|
8177
|
322 |
by (ftac finite_subset 1);
|
10962
|
323 |
by (rtac (finite_dom_body RS finite_imageI) 1);
|
8177
|
324 |
by (rotate_tac 2 1);
|
|
325 |
by (make_imp_tac 1);
|
10962
|
326 |
by (etac finite_induct 1);
|
8177
|
327 |
by (ALLGOALS (clarsimp_tac (
|
17477
|
328 |
claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
|
|
329 |
simpset() delsimps [range_composition])));
|
10962
|
330 |
by (etac MGF_lemma1 1);
|
8177
|
331 |
by (fast_tac (claset() addDs [WT_bodiesD]) 2);
|
|
332 |
by (Clarsimp_tac 1);
|
10962
|
333 |
by (rtac hoare_derivs.asm 1);
|
13911
|
334 |
by (fast_tac (claset() addIs [(thm"domI")]) 1);
|
8177
|
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";
|
10962
|
339 |
by (rtac MGF_lemma1 1);
|
|
340 |
by (assume_tac 1);
|
|
341 |
by (assume_tac 2);
|
8177
|
342 |
by (Clarsimp_tac 1);
|
10834
|
343 |
by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})`dom body" 1);
|
10962
|
344 |
by (etac hoare_derivs.weaken 1);
|
13911
|
345 |
by (fast_tac (claset() addIs [(thm"domI")]) 1);
|
10962
|
346 |
by (rtac (finite_dom_body RSN (2,MGT_Body)) 1);
|
8177
|
347 |
by (Simp_tac 1);
|
|
348 |
by (eatac MGF_lemma2_simult 1 1);
|
10962
|
349 |
by (rtac subset_refl 1);
|
13524
|
350 |
qed "MGF'";
|
8177
|
351 |
|
|
352 |
(* requires Body+empty+insert / BodyN, com_det *)
|
17477
|
353 |
bind_thm ("hoare_complete", MGF' RS MGF_complete);
|
8177
|
354 |
|
|
355 |
section "unused derived rules";
|
|
356 |
|
|
357 |
Goal "G|-{%Z s. False}.c.{Q}";
|
10962
|
358 |
by (rtac hoare_derivs.conseq 1);
|
8177
|
359 |
by (Fast_tac 1);
|
|
360 |
qed "falseE";
|
|
361 |
|
|
362 |
Goal "G|-{P}.c.{%Z s. True}";
|
10962
|
363 |
by (rtac hoare_derivs.conseq 1);
|
8177
|
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}";
|
10962
|
369 |
by (rtac hoare_derivs.conseq 1);
|
8177
|
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}";
|
10962
|
374 |
by (rtac conseq12 1);
|
|
375 |
by (rtac hoare_derivs.Skip 1);
|
8177
|
376 |
by (Fast_tac 1);
|
|
377 |
qed "hoare_SkipI";
|
|
378 |
|
|
379 |
|
|
380 |
section "useful derived rules";
|
|
381 |
|
|
382 |
Goal "{t}|-t";
|
10962
|
383 |
by (rtac hoare_derivs.asm 1);
|
|
384 |
by (rtac subset_refl 1);
|
8177
|
385 |
qed "single_asm";
|
|
386 |
|
|
387 |
Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}";
|
10962
|
388 |
by (rtac hoare_derivs.conseq 1);
|
8177
|
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}";
|
10962
|
397 |
by (rtac export_s 1);
|
|
398 |
by (rtac hoare_derivs.Local 1);
|
|
399 |
by (etac conseq2 1);
|
|
400 |
by (etac spec 1);
|
8177
|
401 |
qed "weak_Local";
|
|
402 |
|
11132
|
403 |
(*
|
|
404 |
Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}";
|
|
405 |
by (induct_tac "c" 1);
|
12486
|
406 |
by Auto_tac;
|
|
407 |
by (rtac conseq1 1);
|
|
408 |
by (rtac hoare_derivs.Skip 1);
|
11132
|
409 |
force 1;
|
12486
|
410 |
by (rtac conseq1 1);
|
|
411 |
by (rtac hoare_derivs.Ass 1);
|
11132
|
412 |
force 1;
|
|
413 |
by (defer_tac 1);
|
|
414 |
###
|
12486
|
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);
|
11132
|
420 |
by (Clarsimp_tac 2);
|
|
421 |
force 1;
|
|
422 |
*)
|