|
1 (* Title: ZF/UNITY/Guar.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Guarantees, etc. |
|
7 |
|
8 From Chandy and Sanders, "Reasoning About Program Composition" |
|
9 Revised by Sidi Ehmety on January 2001 |
|
10 |
|
11 Proofs ported from HOL. |
|
12 *) |
|
13 |
|
14 |
|
15 Goal |
|
16 "F~:program ==> F Join G = programify(G)"; |
|
17 by (rtac program_equalityI 1); |
|
18 by Auto_tac; |
|
19 by (auto_tac (claset(), |
|
20 simpset() addsimps [Join_def, programify_def, SKIP_def, |
|
21 Acts_def, Init_def, AllowedActs_def, |
|
22 RawInit_eq, RawActs_eq, RawAllowedActs_eq, |
|
23 Int_absorb, Int_assoc, Un_absorb])); |
|
24 by (forward_tac [Id_in_RawActs] 2); |
|
25 by (forward_tac [Id_in_RawAllowedActs] 3); |
|
26 by (dtac RawInit_type 1); |
|
27 by (dtac RawActs_type 2); |
|
28 by (dtac RawAllowedActs_type 3); |
|
29 by (auto_tac (claset(), simpset() |
|
30 addsimps [condition_def, actionSet_def, cons_absorb])); |
|
31 qed "not_program_Join1"; |
|
32 |
|
33 Goal |
|
34 "G~:program ==> F Join G = programify(F)"; |
|
35 by (stac Join_commute 1); |
|
36 by (blast_tac (claset() addIs [not_program_Join1]) 1); |
|
37 qed "not_program_Join2"; |
|
38 |
|
39 Goal "F~:program ==> F ok G"; |
|
40 by (auto_tac (claset(), |
|
41 simpset() addsimps [ok_def, programify_def, SKIP_def, mk_program_def, |
|
42 Acts_def, Init_def, AllowedActs_def, |
|
43 RawInit_def, RawActs_def, RawAllowedActs_def, |
|
44 Int_absorb, Int_assoc, Un_absorb])); |
|
45 by (auto_tac (claset(), simpset() |
|
46 addsimps [condition_def, actionSet_def, program_def, cons_absorb])); |
|
47 qed "not_program_ok1"; |
|
48 |
|
49 Goal "G~:program ==> F ok G"; |
|
50 by (rtac ok_sym 1); |
|
51 by (blast_tac (claset() addIs [not_program_ok1]) 1); |
|
52 qed "not_program_ok2"; |
|
53 |
|
54 |
|
55 Goal "OK(cons(i, I), F) <-> \ |
|
56 \ (i:I & OK(I, F)) | (i~:I & OK(I, F) & F(i) ok JOIN(I,F))"; |
|
57 by (asm_full_simp_tac (simpset() addsimps [OK_iff_ok]) 1); |
|
58 (** Auto_tac proves the goal in one step, but take more time **) |
|
59 by Safe_tac; |
|
60 by (ALLGOALS(Clarify_tac)); |
|
61 by (REPEAT(blast_tac (claset() addIs [ok_sym]) 10)); |
|
62 by (REPEAT(Blast_tac 1)); |
|
63 qed "OK_cons_iff"; |
|
64 |
|
65 (*** existential properties ***) |
|
66 |
|
67 Goalw [ex_prop_def] |
|
68 "GG:Fin(program) ==> (ex_prop(X) \ |
|
69 \ --> GG Int X~=0 --> OK(GG, (%G. G)) -->(JN G:GG. G):X)"; |
|
70 by (etac Fin_induct 1); |
|
71 by (ALLGOALS(asm_full_simp_tac |
|
72 (simpset() addsimps [OK_cons_iff]))); |
|
73 (* Auto_tac proves the goal in one step *) |
|
74 by Safe_tac; |
|
75 by (ALLGOALS(Asm_full_simp_tac)); |
|
76 by (Fast_tac 1); |
|
77 qed_spec_mp "ex1"; |
|
78 |
|
79 Goalw [ex_prop_def] |
|
80 "X<=program ==> (ALL GG. GG:Fin(program) & GG Int X ~= 0\ |
|
81 \ --> OK(GG,(%G. G)) -->(JN G:GG. G):X) --> ex_prop(X)"; |
|
82 by (Clarify_tac 1); |
|
83 by (dres_inst_tac [("x", "{F,G}")] spec 1); |
|
84 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [OK_iff_ok]))); |
|
85 by Safe_tac; |
|
86 by (auto_tac (claset() addIs [ok_sym], simpset())); |
|
87 qed "ex2"; |
|
88 |
|
89 (*Chandy & Sanders take this as a definition*) |
|
90 |
|
91 Goal "X<=program ==> ex_prop(X) <-> \ |
|
92 \ (ALL GG. GG:Fin(program) & GG Int X ~= 0 &\ |
|
93 \ OK(GG,( %G. G)) --> (JN G:GG. G):X)"; |
|
94 by (blast_tac (claset() addIs [ex1, ex2 RS mp]) 1); |
|
95 qed "ex_prop_finite"; |
|
96 |
|
97 |
|
98 (*Their "equivalent definition" given at the end of section 3*) |
|
99 Goalw [ex_prop2_def] |
|
100 "ex_prop(X) <-> ex_prop2(X)"; |
|
101 by (Asm_full_simp_tac 1); |
|
102 by (rewrite_goals_tac |
|
103 [ex_prop_def, component_of_def]); |
|
104 by Safe_tac; |
|
105 by (stac Join_commute 4); |
|
106 by (dtac ok_sym 4); |
|
107 by (case_tac "G:program" 1); |
|
108 by (dres_inst_tac [("x", "G")] bspec 5); |
|
109 by (dres_inst_tac [("x", "F")] bspec 4); |
|
110 by Safe_tac; |
|
111 by (force_tac (claset(), |
|
112 simpset() addsimps [not_program_Join1]) 2); |
|
113 by (REPEAT(Force_tac 1)); |
|
114 qed "ex_prop_equiv"; |
|
115 |
|
116 (*** universal properties ***) |
|
117 |
|
118 Goalw [uv_prop_def] |
|
119 "GG:Fin(program) ==> \ |
|
120 \ (uv_prop(X)--> \ |
|
121 \ GG <= X & OK(GG, (%G. G)) --> (JN G:GG. G):X)"; |
|
122 by (etac Fin_induct 1); |
|
123 by (auto_tac (claset(), simpset() addsimps |
|
124 [OK_cons_iff])); |
|
125 qed_spec_mp "uv1"; |
|
126 |
|
127 Goalw [uv_prop_def] |
|
128 "X<=program ==> (ALL GG. GG:Fin(program) & GG <= X & OK(GG,(%G. G)) \ |
|
129 \ --> (JN G:GG. G):X) --> uv_prop(X)"; |
|
130 by Auto_tac; |
|
131 by (Clarify_tac 2); |
|
132 by (dres_inst_tac [("x", "{x,xa}")] spec 2); |
|
133 by (dres_inst_tac [("x", "0")] spec 1); |
|
134 by (auto_tac (claset() addDs [ok_sym], |
|
135 simpset() addsimps [OK_iff_ok])); |
|
136 qed "uv2"; |
|
137 |
|
138 (*Chandy & Sanders take this as a definition*) |
|
139 Goal |
|
140 "X<=program ==> \ |
|
141 \ uv_prop(X) <-> (ALL GG. GG:Fin(program) & GG <= X &\ |
|
142 \ OK(GG, %G. G) --> (JN G:GG. G): X)"; |
|
143 by (REPEAT(blast_tac (claset() addIs [uv1,uv2 RS mp]) 1)); |
|
144 qed "uv_prop_finite"; |
|
145 |
|
146 (*** guarantees ***) |
|
147 (* The premise G:program is needed later *) |
|
148 val major::prems = Goal |
|
149 "[| (!!G. [| F ok G; F Join G:X; G:program |] ==> F Join G : Y); F:program |] \ |
|
150 \ ==> F : X guarantees Y"; |
|
151 by (cut_facts_tac prems 1); |
|
152 by (simp_tac (simpset() addsimps [guar_def, component_def]) 1); |
|
153 by (blast_tac (claset() addIs [major]) 1); |
|
154 qed "guaranteesI"; |
|
155 |
|
156 Goalw [guar_def, component_def] |
|
157 "[| F : X guarantees Y; F ok G; F Join G:X; G:program |] \ |
|
158 \ ==> F Join G : Y"; |
|
159 by (Asm_full_simp_tac 1); |
|
160 qed "guaranteesD"; |
|
161 |
|
162 (*This version of guaranteesD matches more easily in the conclusion |
|
163 The major premise can no longer be F<=H since we need to reason about G*) |
|
164 |
|
165 Goalw [guar_def] |
|
166 "[| F : X guarantees Y; F Join G = H; H : X; F ok G; G:program |] \ |
|
167 \ ==> H : Y"; |
|
168 by (Blast_tac 1); |
|
169 qed "component_guaranteesD"; |
|
170 |
|
171 Goalw [guar_def] |
|
172 "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"; |
|
173 by Auto_tac; |
|
174 qed "guarantees_weaken"; |
|
175 |
|
176 Goalw [guar_def] "X <= Y \ |
|
177 \ ==> X guarantees Y = program"; |
|
178 by (Blast_tac 1); |
|
179 qed "subset_imp_guarantees_program"; |
|
180 |
|
181 (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) |
|
182 Goalw [guar_def] "[| X <= Y; F:program |] \ |
|
183 \ ==> F : X guarantees Y"; |
|
184 by (Blast_tac 1); |
|
185 qed "subset_imp_guarantees"; |
|
186 |
|
187 (*Remark at end of section 4.1 *) |
|
188 Goalw [guar_def, component_of_def] |
|
189 "Y<=program ==>ex_prop(Y) --> (Y = (program guarantees Y))"; |
|
190 by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
|
191 (* Simplification tactics with ex_prop2_def loops *) |
|
192 by (rewrite_goals_tac [ex_prop2_def]); |
|
193 by (Clarify_tac 1); |
|
194 by (rtac equalityI 1); |
|
195 by Safe_tac; |
|
196 by (Blast_tac 1); |
|
197 by (dres_inst_tac [("x", "x")] bspec 1); |
|
198 by (dres_inst_tac [("x", "x")] bspec 3); |
|
199 by (dtac iff_sym 4); |
|
200 by (Blast_tac 1); |
|
201 by (ALLGOALS(Asm_full_simp_tac)); |
|
202 by (etac iffE 2); |
|
203 by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def]))); |
|
204 by Safe_tac; |
|
205 by (REPEAT(Force_tac 1)); |
|
206 qed "ex_prop_imp"; |
|
207 |
|
208 Goalw [guar_def] |
|
209 "(Y = program guarantees Y) ==> ex_prop(Y)"; |
|
210 by (asm_simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
|
211 by (rewrite_goals_tac [ex_prop2_def]); |
|
212 by Safe_tac; |
|
213 by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def]))); |
|
214 by (dtac sym 2); |
|
215 by (ALLGOALS(etac equalityE)); |
|
216 by (REPEAT(Force_tac 1)); |
|
217 qed "guarantees_imp"; |
|
218 |
|
219 Goal "Y<=program ==>(ex_prop(Y)) <-> (Y = program guarantees Y)"; |
|
220 by (rtac iffI 1); |
|
221 by (rtac (ex_prop_imp RS mp) 1); |
|
222 by (rtac guarantees_imp 3); |
|
223 by (ALLGOALS(Asm_simp_tac)); |
|
224 qed "ex_prop_equiv2"; |
|
225 |
|
226 (** Distributive laws. Re-orient to perform miniscoping **) |
|
227 |
|
228 Goalw [guar_def] |
|
229 "i:I ==>(UN i:I. X(i)) guarantees Y = (INT i:I. X(i) guarantees Y)"; |
|
230 by (rtac equalityI 1); |
|
231 by Safe_tac; |
|
232 by (Force_tac 2); |
|
233 by (REPEAT(Blast_tac 1)); |
|
234 qed "guarantees_UN_left"; |
|
235 |
|
236 Goalw [guar_def] |
|
237 "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"; |
|
238 by (rtac equalityI 1); |
|
239 by Safe_tac; |
|
240 by (REPEAT(Blast_tac 1)); |
|
241 qed "guarantees_Un_left"; |
|
242 |
|
243 Goalw [guar_def] |
|
244 "i:I ==> X guarantees (INT i:I. Y(i)) = (INT i:I. X guarantees Y(i))"; |
|
245 by (rtac equalityI 1); |
|
246 by Safe_tac; |
|
247 by (REPEAT(Blast_tac 1)); |
|
248 qed "guarantees_INT_right"; |
|
249 |
|
250 Goalw [guar_def] |
|
251 "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"; |
|
252 by (Blast_tac 1); |
|
253 qed "guarantees_Int_right"; |
|
254 |
|
255 Goal "[| F : Z guarantees X; F : Z guarantees Y |] \ |
|
256 \ ==> F : Z guarantees (X Int Y)"; |
|
257 by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
258 qed "guarantees_Int_right_I"; |
|
259 |
|
260 Goal "i:I==> (F : X guarantees (INT i:I. Y(i))) <-> \ |
|
261 \ (ALL i:I. F : X guarantees Y(i))"; |
|
262 by (asm_simp_tac (simpset() addsimps [guarantees_INT_right, INT_iff]) 1); |
|
263 by (Blast_tac 1); |
|
264 qed "guarantees_INT_right_iff"; |
|
265 |
|
266 |
|
267 Goalw [guar_def] "(X guarantees Y) = (program guarantees ((program-X) Un Y))"; |
|
268 by Auto_tac; |
|
269 qed "shunting"; |
|
270 |
|
271 Goalw [guar_def] "(X guarantees Y) = (program - Y) guarantees (program -X)"; |
|
272 by (Blast_tac 1); |
|
273 qed "contrapositive"; |
|
274 |
|
275 (** The following two can be expressed using intersection and subset, which |
|
276 is more faithful to the text but looks cryptic. |
|
277 **) |
|
278 |
|
279 Goalw [guar_def] |
|
280 "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\ |
|
281 \ ==> F : (V Int Y) guarantees Z"; |
|
282 by (Blast_tac 1); |
|
283 qed "combining1"; |
|
284 |
|
285 Goalw [guar_def] |
|
286 "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\ |
|
287 \ ==> F : V guarantees (X Un Z)"; |
|
288 by (Blast_tac 1); |
|
289 qed "combining2"; |
|
290 |
|
291 |
|
292 (** The following two follow Chandy-Sanders, but the use of object-quantifiers |
|
293 does not suit Isabelle... **) |
|
294 |
|
295 (*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) |
|
296 Goalw [guar_def] |
|
297 "[| ALL i:I. F : X guarantees Y(i); i:I |] \ |
|
298 \ ==> F : X guarantees (INT i:I. Y(i))"; |
|
299 by (Blast_tac 1); |
|
300 qed "all_guarantees"; |
|
301 |
|
302 (*Premises should be [| F: X guarantees Y i; i: I |] *) |
|
303 Goalw [guar_def] |
|
304 "EX i:I. F : X guarantees Y(i) ==> F : X guarantees (UN i:I. Y(i))"; |
|
305 by (Blast_tac 1); |
|
306 qed "ex_guarantees"; |
|
307 |
|
308 |
|
309 (*** Additional guarantees laws, by lcp ***) |
|
310 |
|
311 Goalw [guar_def] |
|
312 "[| F: U guarantees V; G: X guarantees Y; F ok G |] \ |
|
313 \ ==> F Join G: (U Int X) guarantees (V Int Y)"; |
|
314 by (Simp_tac 1); |
|
315 by Safe_tac; |
|
316 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
|
317 by (subgoal_tac "F Join G Join x = G Join (F Join x)" 1); |
|
318 by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); |
|
319 by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
|
320 qed "guarantees_Join_Int"; |
|
321 |
|
322 Goalw [guar_def] |
|
323 "[| F: U guarantees V; G: X guarantees Y; F ok G |] \ |
|
324 \ ==> F Join G: (U Un X) guarantees (V Un Y)"; |
|
325 by (Simp_tac 1); |
|
326 by Safe_tac; |
|
327 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
|
328 by (subgoal_tac "F Join G Join x = G Join (F Join x)" 1); |
|
329 by (rotate_tac 4 1); |
|
330 by (dres_inst_tac [("x", "F Join x")] bspec 1); |
|
331 by (Simp_tac 1); |
|
332 by (force_tac (claset(), simpset() addsimps [ok_commute]) 1); |
|
333 by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
|
334 qed "guarantees_Join_Un"; |
|
335 |
|
336 Goalw [guar_def] |
|
337 "[| ALL i:I. F(i) : X(i) guarantees Y(i); OK(I,F); i:I |] \ |
|
338 \ ==> (JN i:I. F(i)) : (INT i:I. X(i)) guarantees (INT i:I. Y(i))"; |
|
339 by Safe_tac; |
|
340 by (Blast_tac 2); |
|
341 by (dres_inst_tac [("x", "xa")] bspec 1); |
|
342 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [INT_iff]))); |
|
343 by Safe_tac; |
|
344 by (rotate_tac ~1 1); |
|
345 by (dres_inst_tac [("x", "(JN x:(I-{xa}). F(x)) Join G")] bspec 1); |
|
346 by (auto_tac |
|
347 (claset() addIs [OK_imp_ok], |
|
348 simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); |
|
349 qed "guarantees_JN_INT"; |
|
350 |
|
351 Goalw [guar_def] |
|
352 "[| ALL i:I. F(i) : X(i) guarantees Y(i); OK(I,F) |] \ |
|
353 \ ==> JOIN(I,F) : (UN i:I. X(i)) guarantees (UN i:I. Y(i))"; |
|
354 by Auto_tac; |
|
355 by (dres_inst_tac [("x", "xa")] bspec 1); |
|
356 by (ALLGOALS(Asm_full_simp_tac)); |
|
357 by Safe_tac; |
|
358 by (rotate_tac ~1 1); |
|
359 by (dres_inst_tac [("x", "JOIN(I-{xa}, F) Join x")] bspec 1); |
|
360 by (auto_tac |
|
361 (claset() addIs [OK_imp_ok], |
|
362 simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); |
|
363 qed "guarantees_JN_UN"; |
|
364 |
|
365 (*** guarantees laws for breaking down the program, by lcp ***) |
|
366 |
|
367 Goalw [guar_def] |
|
368 "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"; |
|
369 by (Simp_tac 1); |
|
370 by Safe_tac; |
|
371 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
|
372 qed "guarantees_Join_I1"; |
|
373 |
|
374 Goal "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"; |
|
375 by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute, |
|
376 inst "G" "G" ok_commute]) 1); |
|
377 by (blast_tac (claset() addIs [guarantees_Join_I1]) 1); |
|
378 qed "guarantees_Join_I2"; |
|
379 |
|
380 Goalw [guar_def] |
|
381 "[| i:I; F(i): X guarantees Y; OK(I,F) |] \ |
|
382 \ ==> (JN i:I. F(i)) : X guarantees Y"; |
|
383 by Safe_tac; |
|
384 by (dres_inst_tac [("x", "JOIN(I-{i},F) Join G")] bspec 1); |
|
385 by (Simp_tac 1); |
|
386 by (auto_tac (claset() addIs [OK_imp_ok], |
|
387 simpset() addsimps [JN_Join_diff, Join_assoc RS sym])); |
|
388 qed "guarantees_JN_I"; |
|
389 |
|
390 (*** well-definedness ***) |
|
391 |
|
392 Goalw [welldef_def] "F Join G: welldef ==> programify(F): welldef"; |
|
393 by Auto_tac; |
|
394 qed "Join_welldef_D1"; |
|
395 |
|
396 Goalw [welldef_def] "F Join G: welldef ==> programify(G): welldef"; |
|
397 by Auto_tac; |
|
398 qed "Join_welldef_D2"; |
|
399 |
|
400 (*** refinement ***) |
|
401 |
|
402 Goalw [refines_def] "F refines F wrt X"; |
|
403 by (Blast_tac 1); |
|
404 qed "refines_refl"; |
|
405 |
|
406 (* Added by Sidi Ehmety from Chandy & Sander, section 6 *) |
|
407 |
|
408 Goalw [guar_def, component_of_def] |
|
409 "(F:X guarantees Y) <-> \ |
|
410 \ F:program & (ALL H:program. H:X --> (F component_of H --> H:Y))"; |
|
411 by Safe_tac; |
|
412 by (REPEAT(Force_tac 1)); |
|
413 qed "guarantees_equiv"; |
|
414 |
|
415 Goalw [wg_def] "!!X. [| F:(X guarantees Y); X <= program |] ==> X <= wg(F,Y)"; |
|
416 by Auto_tac; |
|
417 qed "wg_weakest"; |
|
418 |
|
419 Goalw [wg_def, guar_def] |
|
420 "F:program ==> F:wg(F,Y) guarantees Y"; |
|
421 by (Blast_tac 1); |
|
422 qed "wg_guarantees"; |
|
423 |
|
424 Goalw [wg_def] |
|
425 "[| F:program; H:program |] ==> \ |
|
426 \ (H: wg(F,X)) <-> H:program & (F component_of H --> H:X)"; |
|
427 by (simp_tac (simpset() addsimps [guarantees_equiv]) 1); |
|
428 by (rtac iffI 1); |
|
429 by Safe_tac; |
|
430 by (res_inst_tac [("x", "{H}")] bexI 3); |
|
431 by (res_inst_tac [("x", "{H}")] bexI 2); |
|
432 by (REPEAT(Blast_tac 1)); |
|
433 qed "wg_equiv"; |
|
434 |
|
435 Goal |
|
436 "[| F component_of H; F:program; H:program |] ==> \ |
|
437 \ H:wg(F,X) <-> H:X"; |
|
438 by (asm_full_simp_tac (simpset() addsimps [wg_equiv]) 1); |
|
439 qed "component_of_wg"; |
|
440 |
|
441 Goal |
|
442 "ALL FF:Fin(program). FF Int X ~= 0 --> OK(FF, %F. F) \ |
|
443 \ --> (ALL F:FF. ((JN F:FF. F): wg(F,X)) <-> ((JN F:FF. F):X))"; |
|
444 by (Clarify_tac 1); |
|
445 by (subgoal_tac "F component_of (JN F:FF. F)" 1); |
|
446 by (dres_inst_tac [("X", "X")] component_of_wg 1); |
|
447 by (force_tac (claset() addSDs [Fin.dom_subset RS subsetD RS PowD], |
|
448 simpset()) 1); |
|
449 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_def]))); |
|
450 by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1); |
|
451 by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym], |
|
452 simpset() addsimps [OK_iff_ok])); |
|
453 qed "wg_finite"; |
|
454 |
|
455 |
|
456 (* "!!FF. [| FF:Fin(program); FF Int X ~=0; OK(FF, %F. F); G:FF |] |
|
457 ==> JOIN(FF, %F. F):wg(G, X) <-> JOIN(FF, %F. F):X" *) |
|
458 val wg_finite2 = wg_finite RS bspec RS mp RS mp RS bspec; |
|
459 |
|
460 |
|
461 Goal "[| ex_prop(X); F:program |] ==> (F:X) <-> (ALL H:program. H : wg(F,X))"; |
|
462 by (asm_full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1); |
|
463 by (rewrite_goals_tac [ex_prop2_def]); |
|
464 by (Blast_tac 1); |
|
465 qed "wg_ex_prop"; |
|
466 |
|
467 (** From Charpentier and Chandy "Theorems About Composition" **) |
|
468 (* Proposition 2 *) |
|
469 Goalw [wx_def] "wx(X)<=X"; |
|
470 by Auto_tac; |
|
471 qed "wx_subset"; |
|
472 |
|
473 Goalw [wx_def] "wx(X)<=program"; |
|
474 by Auto_tac; |
|
475 qed "wx_into_program"; |
|
476 |
|
477 Goal |
|
478 "ex_prop(wx(X))"; |
|
479 by (full_simp_tac (simpset() |
|
480 addsimps [ex_prop_def, wx_def]) 1); |
|
481 by Safe_tac; |
|
482 by (ALLGOALS(res_inst_tac [("x", "xb")] bexI)); |
|
483 by (REPEAT(Force_tac 1)); |
|
484 qed "wx_ex_prop"; |
|
485 |
|
486 Goalw [wx_def] |
|
487 "ALL Z. Z<=program --> Z<= X --> ex_prop(Z) --> Z <= wx(X)"; |
|
488 by Auto_tac; |
|
489 qed "wx_weakest"; |
|
490 |
|
491 (* Proposition 6 *) |
|
492 Goalw [ex_prop_def] |
|
493 "ex_prop({F:program. ALL G:program. F ok G --> F Join G:X})"; |
|
494 by Safe_tac; |
|
495 by (dres_inst_tac [("x", "G Join Ga")] bspec 1); |
|
496 by (Simp_tac 1); |
|
497 by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1); |
|
498 by (dres_inst_tac [("x", "F Join Ga")] bspec 1); |
|
499 by (Simp_tac 1); |
|
500 by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1); |
|
501 by Safe_tac; |
|
502 by (asm_simp_tac (simpset() addsimps [ok_commute]) 1); |
|
503 by (subgoal_tac "F Join G = G Join F" 1); |
|
504 by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1); |
|
505 by (simp_tac (simpset() addsimps [Join_commute]) 1); |
|
506 qed "wx'_ex_prop"; |
|
507 |
|
508 (* Equivalence with the other definition of wx *) |
|
509 |
|
510 Goalw [wx_def] |
|
511 "wx(X) = {F:program. ALL G:program. F ok G --> (F Join G):X}"; |
|
512 by (rtac equalityI 1); |
|
513 by Safe_tac; |
|
514 by (Blast_tac 1); |
|
515 by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1); |
|
516 by (dres_inst_tac [("x", "x")] bspec 1); |
|
517 by (dres_inst_tac [("x", "G")] bspec 2); |
|
518 by (forw_inst_tac [("c", "x Join G")] subsetD 3); |
|
519 by Safe_tac; |
|
520 by (Blast_tac 1); |
|
521 by (Blast_tac 1); |
|
522 by (res_inst_tac [("B", "{F:program. ALL G:program. F ok G --> F Join G:X}")] |
|
523 UnionI 1); |
|
524 by Safe_tac; |
|
525 by (rtac wx'_ex_prop 2); |
|
526 by (rotate_tac 2 1); |
|
527 by (dres_inst_tac [("x", "SKIP")] bspec 1); |
|
528 by Auto_tac; |
|
529 qed "wx_equiv"; |
|
530 |
|
531 (* Propositions 7 to 11 are all about this second definition of wx. And |
|
532 by equivalence between the two definition, they are the same as the ones proved *) |
|
533 |
|
534 |
|
535 (* Proposition 12 *) |
|
536 (* Main result of the paper *) |
|
537 Goalw [guar_def] |
|
538 "(X guarantees Y) = wx((program-X) Un Y)"; |
|
539 by (simp_tac (simpset() addsimps [wx_equiv]) 1); |
|
540 by Auto_tac; |
|
541 qed "guarantees_wx_eq"; |
|
542 |
|
543 (* {* Corollary, but this result has already been proved elsewhere *} |
|
544 "ex_prop(X guarantees Y)"; |
|
545 by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1); |
|
546 qed "guarantees_ex_prop"; |
|
547 *) |
|
548 |
|
549 (* Rules given in section 7 of Chandy and Sander's |
|
550 Reasoning About Program composition paper *) |
|
551 |
|
552 Goal "[| Init(F) <= A; F:program |] \ |
|
553 \ ==> F:(stable(A)) guarantees (Always(A))"; |
|
554 by (rtac guaranteesI 1); |
|
555 by (assume_tac 2); |
|
556 by (simp_tac (simpset() addsimps [Join_commute]) 1); |
|
557 by (rtac stable_Join_Always1 1); |
|
558 by (ALLGOALS(asm_full_simp_tac (simpset() |
|
559 addsimps [invariant_def, Join_stable]))); |
|
560 by (auto_tac (claset(), simpset() addsimps [programify_def])); |
|
561 qed "stable_guarantees_Always"; |
|
562 |
|
563 (* To be moved to WFair.ML *) |
|
564 Goal "[| F:A co A Un B; F:transient(A) |] ==> F:A leadsTo B"; |
|
565 by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); |
|
566 by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); |
|
567 by (rtac (ensuresI RS leadsTo_Basis) 3); |
|
568 by (ALLGOALS(Blast_tac)); |
|
569 qed "leadsTo_Basis'"; |
|
570 |
|
571 Goal "[| F:transient(A); B:condition |] \ |
|
572 \ ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"; |
|
573 by (rtac guaranteesI 1); |
|
574 by (rtac leadsTo_Basis' 1); |
|
575 by (dtac constrains_weaken_R 1); |
|
576 by (assume_tac 3); |
|
577 by (blast_tac (claset() addIs [Join_transient_I1]) 3); |
|
578 by (REPEAT(blast_tac (claset() addDs [transientD]) 1)); |
|
579 qed "constrains_guarantees_leadsTo"; |
|
580 |
|
581 |