|
1 (* Title: ZF/UNITY/SubstAx.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 LeadsTo relation, restricted to the set of reachable states. |
|
7 |
|
8 *) |
|
9 |
|
10 |
|
11 (*Resembles the previous definition of LeadsTo*) |
|
12 |
|
13 Goalw [LeadsTo_def] |
|
14 "A LeadsTo B = \ |
|
15 \ {F:program. F : (reachable(F) Int A) leadsTo (reachable(F) Int B) & \ |
|
16 \ A:condition & B:condition}"; |
|
17 by (blast_tac (claset() addDs [psp_stable2, leadsToD, constrainsD2] |
|
18 addIs [leadsTo_weaken]) 1); |
|
19 qed "LeadsTo_eq_leadsTo"; |
|
20 |
|
21 Goalw [LeadsTo_def] |
|
22 "F: A LeadsTo B ==> F:program & A:condition & B:condition"; |
|
23 by (Blast_tac 1); |
|
24 qed "LeadsToD"; |
|
25 |
|
26 (*** Specialized laws for handling invariants ***) |
|
27 |
|
28 (** Conjoining an Always property **) |
|
29 Goal "[| F : Always(INV); A:condition |] ==> \ |
|
30 \ (F : (INV Int A) LeadsTo A') <-> (F : A LeadsTo A')"; |
|
31 by (asm_full_simp_tac |
|
32 (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable, |
|
33 Int_absorb2, Int_assoc RS sym, leadsToD]) 1); |
|
34 qed "Always_LeadsTo_pre"; |
|
35 |
|
36 Goal "[| F : Always(INV); A':condition |] \ |
|
37 \ ==> (F : A LeadsTo (INV Int A')) <-> (F : A LeadsTo A')"; |
|
38 by (asm_full_simp_tac |
|
39 (simpset() addsimps [LeadsTo_eq_leadsTo, Always_eq_includes_reachable, |
|
40 Int_absorb2, Int_assoc RS sym,leadsToD]) 1); |
|
41 qed "Always_LeadsTo_post"; |
|
42 |
|
43 (* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *) |
|
44 Goal "[| F:Always(C); F : (C Int A) LeadsTo A'; A:condition |] \ |
|
45 \ ==> F: A LeadsTo A'"; |
|
46 by (blast_tac (claset() addIs [Always_LeadsTo_pre RS iffD1]) 1); |
|
47 qed "Always_LeadsToI"; |
|
48 |
|
49 (* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *) |
|
50 Goal |
|
51 "[| F : Always(C); F : A LeadsTo A'; A':condition |] \ |
|
52 \ ==> F : A LeadsTo (C Int A')"; |
|
53 by (blast_tac (claset() addIs [Always_LeadsTo_post RS iffD2]) 1); |
|
54 qed "Always_LeadsToD"; |
|
55 |
|
56 (*** Introduction rules: Basis, Trans, Union ***) |
|
57 |
|
58 Goal "F : A leadsTo B ==> F : A LeadsTo B"; |
|
59 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
|
60 by (blast_tac (claset() addIs [leadsTo_weaken_L] |
|
61 addDs [leadsToD]) 1); |
|
62 qed "leadsTo_imp_LeadsTo"; |
|
63 |
|
64 Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C"; |
|
65 by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1); |
|
66 by (blast_tac (claset() addIs [leadsTo_Trans]) 1); |
|
67 qed "LeadsTo_Trans"; |
|
68 |
|
69 Goalw [LeadsTo_def] |
|
70 "[| ALL A:S. F : A LeadsTo B; F:program; B:condition |] \ |
|
71 \ ==> F : Union(S) LeadsTo B"; |
|
72 by Auto_tac; |
|
73 by (stac Int_Union_Union2 1); |
|
74 by (blast_tac (claset() addIs [leadsTo_UN]) 1); |
|
75 bind_thm("LeadsTo_Union", ballI RS result()); |
|
76 |
|
77 |
|
78 (*** Derived rules ***) |
|
79 |
|
80 Goalw [LeadsTo_def] |
|
81 "[| F:program; A:condition |] ==>F : A LeadsTo state"; |
|
82 by (blast_tac (claset() addIs [leadsTo_state]) 1); |
|
83 qed "LeadsTo_state"; |
|
84 Addsimps [LeadsTo_state]; |
|
85 |
|
86 (*Useful with cancellation, disjunction*) |
|
87 Goal "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"; |
|
88 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
|
89 qed "LeadsTo_Un_duplicate"; |
|
90 |
|
91 Goal "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)"; |
|
92 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
|
93 qed "LeadsTo_Un_duplicate2"; |
|
94 |
|
95 Goal "[| ALL i:I. F : A(i) LeadsTo B; F:program; B:condition |] \ |
|
96 \ ==> F : (UN i:I. A(i)) LeadsTo B"; |
|
97 by (simp_tac (simpset() addsimps [Int_Union_Union]) 1); |
|
98 by (blast_tac (claset() addIs [LeadsTo_Union]) 1); |
|
99 bind_thm("LeadsTo_UN", ballI RS result()); |
|
100 |
|
101 (*Binary union introduction rule*) |
|
102 Goal "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"; |
|
103 by (stac Un_eq_Union 1); |
|
104 by (blast_tac (claset() addIs [LeadsTo_Union] |
|
105 addDs [LeadsToD]) 1); |
|
106 qed "LeadsTo_Un"; |
|
107 |
|
108 (*Lets us look at the starting state*) |
|
109 Goal "[| ALL s:A. F : {s} LeadsTo B; F:program; B:condition |]\ |
|
110 \ ==> F : A LeadsTo B"; |
|
111 by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1); |
|
112 by (REPEAT(Blast_tac 1)); |
|
113 bind_thm("single_LeadsTo_I", ballI RS result()); |
|
114 |
|
115 Goal "[| A <= B; B:condition; F:program |] ==> F : A LeadsTo B"; |
|
116 by (subgoal_tac "A:condition" 1); |
|
117 by (force_tac (claset(), |
|
118 simpset() addsimps [condition_def]) 2); |
|
119 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
|
120 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
121 qed "subset_imp_LeadsTo"; |
|
122 |
|
123 bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); |
|
124 Addsimps [empty_LeadsTo]; |
|
125 |
|
126 Goal "[| F : A LeadsTo A'; A' <= B'; B':condition |] ==> F : A LeadsTo B'"; |
|
127 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
|
128 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1); |
|
129 qed_spec_mp "LeadsTo_weaken_R"; |
|
130 |
|
131 |
|
132 Goal "[| F : A LeadsTo A'; B <= A |] \ |
|
133 \ ==> F : B LeadsTo A'"; |
|
134 by (subgoal_tac "B:condition" 1); |
|
135 by (force_tac (claset() addSDs [LeadsToD], |
|
136 simpset() addsimps [condition_def]) 2); |
|
137 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
|
138 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); |
|
139 qed_spec_mp "LeadsTo_weaken_L"; |
|
140 |
|
141 Goal "[| F : A LeadsTo A'; \ |
|
142 \ B <= A; A' <= B'; B':condition |] \ |
|
143 \ ==> F : B LeadsTo B'"; |
|
144 by (blast_tac (claset() addIs [LeadsTo_weaken_R, |
|
145 LeadsTo_weaken_L, LeadsTo_Trans]) 1); |
|
146 qed "LeadsTo_weaken"; |
|
147 |
|
148 Goal "[| F : Always(C); F : A LeadsTo A'; \ |
|
149 \ C Int B <= A; C Int A' <= B'; B:condition; B':condition |] \ |
|
150 \ ==> F : B LeadsTo B'"; |
|
151 by (blast_tac (claset() |
|
152 addDs [AlwaysD2, LeadsToD, Always_LeadsToI] |
|
153 addIs [LeadsTo_weaken, Always_LeadsToD]) 1); |
|
154 qed "Always_LeadsTo_weaken"; |
|
155 |
|
156 (** Two theorems for "proof lattices" **) |
|
157 |
|
158 Goal "F : A LeadsTo B ==> F:(A Un B) LeadsTo B"; |
|
159 by (blast_tac (claset() |
|
160 addIs [LeadsTo_Un, subset_imp_LeadsTo] |
|
161 addDs [LeadsToD]) 1); |
|
162 qed "LeadsTo_Un_post"; |
|
163 |
|
164 Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \ |
|
165 \ ==> F : (A Un B) LeadsTo C"; |
|
166 by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, |
|
167 LeadsTo_weaken_L, LeadsTo_Trans] |
|
168 addDs [LeadsToD]) 1); |
|
169 qed "LeadsTo_Trans_Un"; |
|
170 |
|
171 |
|
172 (** Distributive laws **) |
|
173 |
|
174 Goal "(F : (A Un B) LeadsTo C) <-> (F : A LeadsTo C & F : B LeadsTo C)"; |
|
175 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); |
|
176 qed "LeadsTo_Un_distrib"; |
|
177 |
|
178 Goal "[| F:program; B:condition |] ==> \ |
|
179 \ (F : (UN i:I. A(i)) LeadsTo B) <-> (ALL i : I. F : A(i) LeadsTo B)"; |
|
180 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); |
|
181 qed "LeadsTo_UN_distrib"; |
|
182 |
|
183 Goal "[| F:program; B:condition |] ==> \ |
|
184 \ (F : Union(S) LeadsTo B) <-> (ALL A : S. F : A LeadsTo B)"; |
|
185 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); |
|
186 qed "LeadsTo_Union_distrib"; |
|
187 |
|
188 (** More rules using the premise "Always INV" **) |
|
189 |
|
190 Goal "F : A Ensures B ==> F : A LeadsTo B"; |
|
191 by (asm_full_simp_tac |
|
192 (simpset() addsimps [Ensures_def, LeadsTo_def, leadsTo_Basis]) 1); |
|
193 qed "LeadsTo_Basis"; |
|
194 |
|
195 Goal "[| F : (A-B) Co (A Un B); F : transient (A-B) |] \ |
|
196 \ ==> F : A Ensures B"; |
|
197 by (asm_full_simp_tac |
|
198 (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1); |
|
199 by (blast_tac (claset() addIs [ensuresI, constrains_weaken, |
|
200 transient_strengthen] |
|
201 addDs [constrainsD2]) 1); |
|
202 qed "EnsuresI"; |
|
203 |
|
204 Goal "[| F : Always(INV); \ |
|
205 \ F : (INV Int (A-A')) Co (A Un A'); \ |
|
206 \ F : transient (INV Int (A-A')) |] \ |
|
207 \ ==> F : A LeadsTo A'"; |
|
208 by (rtac Always_LeadsToI 1); |
|
209 by (assume_tac 1); |
|
210 by (blast_tac (claset() addDs [ConstrainsD]) 2); |
|
211 by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis, |
|
212 Always_ConstrainsD RS Constrains_weaken, |
|
213 transient_strengthen] |
|
214 addDs [AlwaysD2, ConstrainsD]) 1); |
|
215 qed "Always_LeadsTo_Basis"; |
|
216 |
|
217 (*Set difference: maybe combine with leadsTo_weaken_L?? |
|
218 This is the most useful form of the "disjunction" rule*) |
|
219 Goal "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C; \ |
|
220 \ A:condition; B:condition |] \ |
|
221 \ ==> F : A LeadsTo C"; |
|
222 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken] |
|
223 addDs [LeadsToD]) 1); |
|
224 qed "LeadsTo_Diff"; |
|
225 |
|
226 |
|
227 Goal "[| ALL i:I. F: A(i) LeadsTo A'(i); F:program |] \ |
|
228 \ ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))"; |
|
229 by (rtac LeadsTo_Union 1); |
|
230 by (ALLGOALS(Clarify_tac)); |
|
231 by (blast_tac (claset() addDs [LeadsToD]) 2); |
|
232 by (blast_tac (claset() addIs [LeadsTo_weaken_R] |
|
233 addDs [LeadsToD]) 1); |
|
234 bind_thm ("LeadsTo_UN_UN", ballI RS result()); |
|
235 |
|
236 |
|
237 (*Version with no index set*) |
|
238 Goal "[| ALL i. F: A(i) LeadsTo A'(i); F:program |] \ |
|
239 \ ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))"; |
|
240 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1); |
|
241 qed "all_LeadsTo_UN_UN"; |
|
242 |
|
243 bind_thm ("LeadsTo_UN_UN_noindex", allI RS all_LeadsTo_UN_UN); |
|
244 |
|
245 (*Binary union version*) |
|
246 Goal "[| F : A LeadsTo A'; F : B LeadsTo B' |] \ |
|
247 \ ==> F : (A Un B) LeadsTo (A' Un B')"; |
|
248 by (blast_tac (claset() |
|
249 addIs [LeadsTo_Un, LeadsTo_weaken_R] |
|
250 addDs [LeadsToD]) 1); |
|
251 qed "LeadsTo_Un_Un"; |
|
252 |
|
253 (** The cancellation law **) |
|
254 |
|
255 Goal "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |] \ |
|
256 \ ==> F : A LeadsTo (A' Un B')"; |
|
257 by (blast_tac (claset() addIs [LeadsTo_Un_Un, |
|
258 subset_imp_LeadsTo, LeadsTo_Trans] |
|
259 addDs [LeadsToD]) 1); |
|
260 qed "LeadsTo_cancel2"; |
|
261 |
|
262 Goal "A Un (B - A) = A Un B"; |
|
263 by Auto_tac; |
|
264 qed "Un_Diff"; |
|
265 |
|
266 Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] \ |
|
267 \ ==> F : A LeadsTo (A' Un B')"; |
|
268 by (rtac LeadsTo_cancel2 1); |
|
269 by (assume_tac 2); |
|
270 by (asm_simp_tac (simpset() addsimps [Un_Diff]) 1); |
|
271 qed "LeadsTo_cancel_Diff2"; |
|
272 |
|
273 Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] \ |
|
274 \ ==> F : A LeadsTo (B' Un A')"; |
|
275 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
|
276 by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1); |
|
277 qed "LeadsTo_cancel1"; |
|
278 |
|
279 |
|
280 Goal "(B - A) Un A = B Un A"; |
|
281 by Auto_tac; |
|
282 qed "Diff_Un2"; |
|
283 |
|
284 Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] \ |
|
285 \ ==> F : A LeadsTo (B' Un A')"; |
|
286 by (rtac LeadsTo_cancel1 1); |
|
287 by (assume_tac 2); |
|
288 by (asm_simp_tac (simpset() addsimps [Diff_Un2]) 1); |
|
289 qed "LeadsTo_cancel_Diff1"; |
|
290 |
|
291 |
|
292 (** The impossibility law **) |
|
293 |
|
294 (*The set "A" may be non-empty, but it contains no reachable states*) |
|
295 Goal "F : A LeadsTo 0 ==> F : Always (state -A)"; |
|
296 by (full_simp_tac (simpset() |
|
297 addsimps [LeadsTo_def,Always_eq_includes_reachable]) 1); |
|
298 by (Clarify_tac 1); |
|
299 by (forward_tac [reachableD] 1); |
|
300 by (auto_tac (claset() addSDs [leadsTo_empty], |
|
301 simpset() addsimps [condition_def])); |
|
302 qed "LeadsTo_empty"; |
|
303 |
|
304 (** PSP: Progress-Safety-Progress **) |
|
305 |
|
306 (*Special case of PSP: Misra's "stable conjunction"*) |
|
307 Goal "[| F : A LeadsTo A'; F : Stable(B) |] \ |
|
308 \ ==> F : (A Int B) LeadsTo (A' Int B)"; |
|
309 by (forward_tac [StableD2] 1); |
|
310 by (rotate_tac ~1 1); |
|
311 by (asm_full_simp_tac |
|
312 (simpset() addsimps [LeadsTo_eq_leadsTo, Stable_eq_stable]) 1); |
|
313 by (Clarify_tac 1); |
|
314 by (dtac psp_stable 1); |
|
315 by (assume_tac 1); |
|
316 by (asm_full_simp_tac (simpset() addsimps (Int_absorb::Int_ac)) 1); |
|
317 qed "PSP_Stable"; |
|
318 |
|
319 Goal "[| F : A LeadsTo A'; F : Stable(B) |] \ |
|
320 \ ==> F : (B Int A) LeadsTo (B Int A')"; |
|
321 by (asm_simp_tac (simpset() addsimps PSP_Stable::Int_ac) 1); |
|
322 qed "PSP_Stable2"; |
|
323 |
|
324 Goal "[| F : A LeadsTo A'; F : B Co B' |] \ |
|
325 \ ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"; |
|
326 by (full_simp_tac |
|
327 (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1); |
|
328 by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1); |
|
329 qed "PSP"; |
|
330 |
|
331 Goal "[| F : A LeadsTo A'; F : B Co B' |] \ |
|
332 \ ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))"; |
|
333 by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1); |
|
334 qed "PSP2"; |
|
335 |
|
336 |
|
337 Goal |
|
338 "[| F : A LeadsTo A'; F : B Unless B' |] \ |
|
339 \ ==> F : (A Int B) LeadsTo ((A' Int B) Un B')"; |
|
340 by (forward_tac [LeadsToD] 1); |
|
341 by (forward_tac [UnlessD] 1); |
|
342 by (rewrite_goals_tac [Unless_def]); |
|
343 by (dtac PSP 1); |
|
344 by (assume_tac 1); |
|
345 by (blast_tac (claset() |
|
346 addIs [LeadsTo_Diff, |
|
347 LeadsTo_weaken, subset_imp_LeadsTo]) 1); |
|
348 qed "PSP_Unless"; |
|
349 |
|
350 (*** Induction rules ***) |
|
351 |
|
352 (** Meta or object quantifier ????? **) |
|
353 Goal "[| wf(r); \ |
|
354 \ ALL m:I. F : (A Int f-``{m}) LeadsTo \ |
|
355 \ ((A Int f-``(converse(r) `` {m})) Un B); \ |
|
356 \ field(r)<=I; A<=f-``I; F:program; A:condition; B:condition |] \ |
|
357 \ ==> F : A LeadsTo B"; |
|
358 by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1); |
|
359 by Safe_tac; |
|
360 by (eres_inst_tac [("I", "I"), ("f", "f")] leadsTo_wf_induct 1); |
|
361 by (ALLGOALS(Clarify_tac)); |
|
362 by (dres_inst_tac [("x", "m")] bspec 4); |
|
363 by Safe_tac; |
|
364 by (res_inst_tac [("A'", |
|
365 "reachable(F) Int (A Int f -``(converse(r)``{m}) Un B)")] |
|
366 leadsTo_weaken_R 4); |
|
367 by (asm_simp_tac (simpset() addsimps [Int_assoc]) 4); |
|
368 by (asm_simp_tac (simpset() addsimps [Int_assoc]) 5); |
|
369 by (REPEAT(Blast_tac 1)); |
|
370 qed "LeadsTo_wf_induct"; |
|
371 |
|
372 |
|
373 |
|
374 Goal "[| ALL m:nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``lessThan(m,nat)) Un B); \ |
|
375 \ A<=f-``nat; F:program; A:condition; B:condition |] \ |
|
376 \ ==> F : A LeadsTo B"; |
|
377 by (res_inst_tac [("A1", "nat"), ("I", "nat")] (wf_less_than RS LeadsTo_wf_induct) 1); |
|
378 by (ALLGOALS(asm_full_simp_tac |
|
379 (simpset() addsimps [nat_less_than_field]))); |
|
380 by (Clarify_tac 1); |
|
381 by (ALLGOALS(asm_full_simp_tac |
|
382 (simpset() addsimps [rewrite_rule [vimage_def] Image_inverse_less_than]))); |
|
383 qed "LessThan_induct"; |
|
384 |
|
385 |
|
386 (****** |
|
387 To be ported ??? I am not sure. |
|
388 |
|
389 integ_0_le_induct |
|
390 LessThan_bounded_induct |
|
391 GreaterThan_bounded_induct |
|
392 |
|
393 *****) |
|
394 |
|
395 (*** Completion: Binary and General Finite versions ***) |
|
396 |
|
397 Goal "[| F : A LeadsTo (A' Un C); F : A' Co (A' Un C); \ |
|
398 \ F : B LeadsTo (B' Un C); F : B' Co (B' Un C) |] \ |
|
399 \ ==> F : (A Int B) LeadsTo ((A' Int B') Un C)"; |
|
400 by (full_simp_tac |
|
401 (simpset() addsimps [LeadsTo_eq_leadsTo, Constrains_eq_constrains, |
|
402 Int_Un_distrib2 RS sym]) 1); |
|
403 by Safe_tac; |
|
404 by (REPEAT(Blast_tac 2)); |
|
405 by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1); |
|
406 qed "Completion"; |
|
407 |
|
408 |
|
409 Goal "[| I:Fin(X);F:program; C:condition |] \ |
|
410 \ ==> (ALL i:I. F : (A(i)) LeadsTo (A'(i) Un C)) --> \ |
|
411 \ (ALL i:I. F : (A'(i)) Co (A'(i) Un C)) --> \ |
|
412 \ F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)"; |
|
413 by (etac Fin_induct 1); |
|
414 by Auto_tac; |
|
415 by (case_tac "y=0" 1); |
|
416 by Auto_tac; |
|
417 by (etac not_emptyE 1); |
|
418 by (subgoal_tac "Inter(cons(A(x), RepFun(y, A)))= A(x) Int Inter(RepFun(y,A)) &\ |
|
419 \ Inter(cons(A'(x), RepFun(y, A')))= A'(x) Int Inter(RepFun(y,A'))" 1); |
|
420 by (Blast_tac 2); |
|
421 by (Asm_simp_tac 1); |
|
422 by (rtac Completion 1); |
|
423 by (subgoal_tac "Inter(RepFun(y, A')) Un C = (INT x:RepFun(y, A'). x Un C)" 4); |
|
424 by (Blast_tac 5); |
|
425 by (Asm_simp_tac 4); |
|
426 by (rtac Constrains_INT 4); |
|
427 by (REPEAT(Blast_tac 1)); |
|
428 val lemma = result(); |
|
429 |
|
430 |
|
431 val prems = Goal |
|
432 "[| I:Fin(X); !!i. i:I ==> F : A(i) LeadsTo (A'(i) Un C); \ |
|
433 \ !!i. i:I ==> F : A'(i) Co (A'(i) Un C); \ |
|
434 \ F:program; C:condition |] \ |
|
435 \ ==> F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)"; |
|
436 by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1); |
|
437 qed "Finite_completion"; |
|
438 |
|
439 Goalw [Stable_def] |
|
440 "[| F : A LeadsTo A'; F : Stable(A'); \ |
|
441 \ F : B LeadsTo B'; F : Stable(B') |] \ |
|
442 \ ==> F : (A Int B) LeadsTo (A' Int B')"; |
|
443 by (res_inst_tac [("C1", "0")] (Completion RS LeadsTo_weaken_R) 1); |
|
444 by (REPEAT(blast_tac (claset() addDs [LeadsToD,ConstrainsD]) 5)); |
|
445 by (ALLGOALS(Asm_full_simp_tac)); |
|
446 qed "Stable_completion"; |
|
447 |
|
448 |
|
449 val prems = Goalw [Stable_def] |
|
450 "[| I:Fin(X); \ |
|
451 \ ALL i:I. F : A(i) LeadsTo A'(i); \ |
|
452 \ ALL i:I. F: Stable(A'(i)); F:program |] \ |
|
453 \ ==> F : (INT i:I. A(i)) LeadsTo (INT i:I. A'(i))"; |
|
454 by (subgoal_tac "(INT i:I. A'(i)):condition" 1); |
|
455 by (blast_tac (claset() addDs [LeadsToD,ConstrainsD]) 2); |
|
456 by (res_inst_tac [("C1", "0")] (Finite_completion RS LeadsTo_weaken_R) 1); |
|
457 by (assume_tac 7); |
|
458 by (ALLGOALS(Asm_full_simp_tac)); |
|
459 by (ALLGOALS (Blast_tac)); |
|
460 qed "Finite_stable_completion"; |
|
461 |
|
462 |
|
463 (*proves "ensures/leadsTo" properties when the program is specified*) |
|
464 fun ensures_tac sact = |
|
465 SELECT_GOAL |
|
466 (EVERY [REPEAT (Always_Int_tac 1), |
|
467 etac Always_LeadsTo_Basis 1 |
|
468 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
|
469 REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis, |
|
470 EnsuresI, ensuresI] 1), |
|
471 (*now there are two subgoals: co & transient*) |
|
472 simp_tac (simpset() addsimps !program_defs_ref) 2, |
|
473 res_inst_tac [("act", sact)] transientI 2, |
|
474 (*simplify the command's domain*) |
|
475 simp_tac (simpset() addsimps [domain_def]) 3, |
|
476 (* proving the domain part *) |
|
477 Clarify_tac 3, dtac swap 3, Force_tac 4, |
|
478 rtac ReplaceI 3, Force_tac 3, Force_tac 4, |
|
479 Asm_full_simp_tac 3, rtac conjI 3, Simp_tac 4, |
|
480 REPEAT (rtac update_type2 3), |
|
481 constrains_tac 1, |
|
482 ALLGOALS Clarify_tac, |
|
483 ALLGOALS (asm_full_simp_tac |
|
484 (simpset() addsimps [condition_def])), |
|
485 ALLGOALS Clarify_tac]); |
|
486 |