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