author | wenzelm |
Wed, 12 Dec 2001 20:37:31 +0100 | |
changeset 12484 | 7ad150f5fc10 |
parent 12220 | 9dc4e8fec63d |
child 13535 | 007559e981c7 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: HOL/UNITY/WFair.ML |
2 |
ID: $Id$ |
|
3 |
Author: Sidi O Ehmety, Computer Laboratory |
|
4 |
Copyright 2001 University of Cambridge |
|
5 |
||
6 |
Weak Fairness versions of transient, ensures, leadsTo. |
|
7 |
||
8 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 |
*) |
|
10 |
||
11 |
(*** transient ***) |
|
12 |
||
12195 | 13 |
Goalw [transient_def] "transient(A)<=program"; |
11479 | 14 |
by Auto_tac; |
12195 | 15 |
qed "transient_type"; |
16 |
||
17 |
Goalw [transient_def] |
|
18 |
"F:transient(A) ==> F:program & st_set(A)"; |
|
19 |
by Auto_tac; |
|
20 |
qed "transientD2"; |
|
11479 | 21 |
|
22 |
Goalw [stable_def, constrains_def, transient_def] |
|
23 |
"[| F : stable(A); F : transient(A) |] ==> A = 0"; |
|
24 |
by Auto_tac; |
|
25 |
by (Blast_tac 1); |
|
26 |
qed "stable_transient_empty"; |
|
27 |
||
12195 | 28 |
Goalw [transient_def, st_set_def] |
29 |
"[|F:transient(A); B<=A|] ==> F:transient(B)"; |
|
11479 | 30 |
by Safe_tac; |
31 |
by (res_inst_tac [("x", "act")] bexI 1); |
|
32 |
by (ALLGOALS(Asm_full_simp_tac)); |
|
33 |
by (Blast_tac 1); |
|
12195 | 34 |
by Auto_tac; |
11479 | 35 |
qed "transient_strengthen"; |
36 |
||
12195 | 37 |
Goalw [transient_def] |
38 |
"[|act:Acts(F); A <= domain(act); act``A <= state-A; \ |
|
39 |
\ F:program; st_set(A)|] ==> F:transient(A)"; |
|
11479 | 40 |
by (Blast_tac 1); |
41 |
qed "transientI"; |
|
42 |
||
43 |
val major::prems = |
|
12195 | 44 |
Goalw [transient_def] "[| F:transient(A); \ |
45 |
\ !!act. [| act:Acts(F); A <= domain(act); act``A <= state-A|]==>P|]==>P"; |
|
11479 | 46 |
by (rtac (major RS CollectE) 1); |
47 |
by (blast_tac (claset() addIs prems) 1); |
|
48 |
qed "transientE"; |
|
49 |
||
50 |
Goalw [transient_def] "transient(state) = 0"; |
|
51 |
by (rtac equalityI 1); |
|
52 |
by (ALLGOALS(Clarify_tac)); |
|
12195 | 53 |
by (cut_inst_tac [("F", "x")] Acts_type 1); |
11479 | 54 |
by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1); |
12195 | 55 |
by Auto_tac; |
11479 | 56 |
qed "transient_state"; |
57 |
||
12195 | 58 |
Goalw [transient_def,st_set_def] "state<=B ==> transient(B) = 0"; |
59 |
by (rtac equalityI 1); |
|
60 |
by (ALLGOALS(Clarify_tac)); |
|
61 |
by (cut_inst_tac [("F", "x")] Acts_type 1); |
|
62 |
by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1); |
|
63 |
by (subgoal_tac "B=state" 1); |
|
64 |
by Auto_tac; |
|
65 |
qed "transient_state2"; |
|
66 |
||
11479 | 67 |
Goalw [transient_def] "transient(0) = program"; |
68 |
by (rtac equalityI 1); |
|
12195 | 69 |
by Auto_tac; |
11479 | 70 |
qed "transient_empty"; |
71 |
||
12195 | 72 |
Addsimps [transient_empty, transient_state, transient_state2]; |
11479 | 73 |
|
74 |
(*** ensures ***) |
|
75 |
||
12195 | 76 |
Goalw [ensures_def, constrains_def] "A ensures B <=program"; |
77 |
by Auto_tac; |
|
78 |
qed "ensures_type"; |
|
79 |
||
11479 | 80 |
Goalw [ensures_def] |
12195 | 81 |
"[|F:(A-B) co (A Un B); F:transient(A-B)|]==>F:A ensures B"; |
82 |
by (auto_tac (claset(), simpset() addsimps [transient_type RS subsetD])); |
|
11479 | 83 |
qed "ensuresI"; |
84 |
||
12195 | 85 |
(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *) |
11479 | 86 |
Goal "[| F:A co A Un B; F: transient(A) |] ==> F: A ensures B"; |
87 |
by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); |
|
88 |
by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); |
|
12195 | 89 |
by (auto_tac (claset(), simpset() addsimps [ensures_def, transient_type RS subsetD])); |
11479 | 90 |
qed "ensuresI2"; |
91 |
||
12195 | 92 |
Goalw [ensures_def] "F:A ensures B ==> F:(A-B) co (A Un B) & F:transient (A-B)"; |
93 |
by Auto_tac; |
|
11479 | 94 |
qed "ensuresD"; |
95 |
||
12195 | 96 |
Goalw [ensures_def] "[|F:A ensures A'; A'<=B' |] ==> F:A ensures B'"; |
11479 | 97 |
by (blast_tac (claset() |
12195 | 98 |
addIs [transient_strengthen, constrains_weaken]) 1); |
11479 | 99 |
qed "ensures_weaken_R"; |
100 |
||
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
101 |
(*The L-version (precondition strengthening) fails, but we have this*) |
12220 | 102 |
Goalw [ensures_def] |
103 |
"[| F:stable(C); F:A ensures B |] ==> F:(C Int A) ensures (C Int B)"; |
|
104 |
by (simp_tac (simpset() addsimps [Int_Un_distrib RS sym, |
|
105 |
Diff_Int_distrib RS sym]) 1); |
|
11479 | 106 |
by (blast_tac (claset() |
107 |
addIs [transient_strengthen, |
|
12195 | 108 |
stable_constrains_Int, constrains_weaken]) 1); |
11479 | 109 |
qed "stable_ensures_Int"; |
110 |
||
12195 | 111 |
Goal "[|F:stable(A); F:transient(C); A<=B Un C|] ==> F : A ensures B"; |
112 |
by (forward_tac [stable_type RS subsetD] 1); |
|
113 |
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); |
|
11479 | 114 |
by (Clarify_tac 1); |
115 |
by (blast_tac (claset() addIs [transient_strengthen, |
|
12195 | 116 |
constrains_weaken]) 1); |
11479 | 117 |
qed "stable_transient_ensures"; |
118 |
||
119 |
Goal "(A ensures B) = (A unless B) Int transient (A-B)"; |
|
12195 | 120 |
by (auto_tac (claset(), simpset() addsimps [ensures_def, unless_def])); |
11479 | 121 |
qed "ensures_eq"; |
122 |
||
12195 | 123 |
Goal "[| F:program; A<=B |] ==> F : A ensures B"; |
124 |
by (rewrite_goal_tac [ensures_def,constrains_def,transient_def, st_set_def] 1); |
|
125 |
by Auto_tac; |
|
126 |
qed "subset_imp_ensures"; |
|
127 |
||
11479 | 128 |
(*** leadsTo ***) |
12195 | 129 |
val leads_left = leads.dom_subset RS subsetD RS SigmaD1; |
130 |
val leads_right = leads.dom_subset RS subsetD RS SigmaD2; |
|
11479 | 131 |
|
12195 | 132 |
Goalw [leadsTo_def] "A leadsTo B <= program"; |
133 |
by Auto_tac; |
|
134 |
qed "leadsTo_type"; |
|
135 |
||
136 |
Goalw [leadsTo_def, st_set_def] |
|
137 |
"F: A leadsTo B ==> F:program & st_set(A) & st_set(B)"; |
|
138 |
by (blast_tac (claset() addDs [leads_left, leads_right]) 1); |
|
139 |
qed "leadsToD2"; |
|
11479 | 140 |
|
12195 | 141 |
Goalw [leadsTo_def, st_set_def] |
142 |
"[|F:A ensures B; st_set(A); st_set(B)|] ==> F:A leadsTo B"; |
|
143 |
by (cut_facts_tac [ensures_type] 1); |
|
144 |
by (auto_tac (claset() addIs [leads.Basis], simpset())); |
|
11479 | 145 |
qed "leadsTo_Basis"; |
12195 | 146 |
AddIs [leadsTo_Basis]; |
11479 | 147 |
|
12195 | 148 |
(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *) |
149 |
(* [| F:program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *) |
|
150 |
bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); |
|
11479 | 151 |
|
12195 | 152 |
Goalw [leadsTo_def] "[|F: A leadsTo B; F: B leadsTo C |]==>F: A leadsTo C"; |
153 |
by (auto_tac (claset() addIs [leads.Trans], simpset())); |
|
11479 | 154 |
qed "leadsTo_Trans"; |
155 |
||
12195 | 156 |
(* Better when used in association with leadsTo_weaken_R *) |
157 |
Goalw [transient_def] "F:transient(A) ==> F : A leadsTo (state-A )"; |
|
11479 | 158 |
by (rtac (ensuresI RS leadsTo_Basis) 1); |
159 |
by (ALLGOALS(Clarify_tac)); |
|
160 |
by (blast_tac (claset() addIs [transientI]) 2); |
|
161 |
by (rtac constrains_weaken 1); |
|
162 |
by Auto_tac; |
|
163 |
qed "transient_imp_leadsTo"; |
|
164 |
||
165 |
(*Useful with cancellation, disjunction*) |
|
166 |
Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; |
|
12220 | 167 |
by (Asm_full_simp_tac 1); |
11479 | 168 |
qed "leadsTo_Un_duplicate"; |
169 |
||
170 |
Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"; |
|
171 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
|
172 |
qed "leadsTo_Un_duplicate2"; |
|
173 |
||
12220 | 174 |
(*The Union introduction rule as we should have liked to state it*) |
12195 | 175 |
val [major, program,B]= Goalw [leadsTo_def, st_set_def] |
176 |
"[|(!!A. A:S ==> F:A leadsTo B); F:program; st_set(B)|]==>F:Union(S) leadsTo B"; |
|
177 |
by (cut_facts_tac [program, B] 1); |
|
178 |
by Auto_tac; |
|
179 |
by (rtac leads.Union 1); |
|
180 |
by Auto_tac; |
|
181 |
by (ALLGOALS(dtac major)); |
|
182 |
by (auto_tac (claset() addDs [leads_left], simpset())); |
|
183 |
qed "leadsTo_Union"; |
|
11479 | 184 |
|
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
185 |
val [major,program,B] = Goalw [leadsTo_def, st_set_def] |
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
186 |
"[|(!!A. A:S ==>F:(A Int C) leadsTo B); F:program; st_set(B)|] \ |
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
187 |
\ ==>F:(Union(S)Int C)leadsTo B"; |
12195 | 188 |
by (cut_facts_tac [program, B] 1); |
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
189 |
by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_Union_Union]) 1); |
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
190 |
by (resolve_tac [leads.Union] 1); |
12195 | 191 |
by Auto_tac; |
192 |
by (ALLGOALS(dtac major)); |
|
193 |
by (auto_tac (claset() addDs [leads_left], simpset())); |
|
194 |
qed "leadsTo_Union_Int"; |
|
11479 | 195 |
|
12195 | 196 |
val [major,program,B] = Goalw [leadsTo_def, st_set_def] |
197 |
"[|(!!i. i:I ==> F : A(i) leadsTo B); F:program; st_set(B)|]==>F:(UN i:I. A(i)) leadsTo B"; |
|
198 |
by (cut_facts_tac [program, B] 1); |
|
199 |
by (asm_simp_tac (simpset() addsimps [Int_Union_Union]) 1); |
|
200 |
by (rtac leads.Union 1); |
|
201 |
by Auto_tac; |
|
202 |
by (ALLGOALS(dtac major)); |
|
203 |
by (auto_tac (claset() addDs [leads_left], simpset())); |
|
204 |
qed "leadsTo_UN"; |
|
11479 | 205 |
|
12195 | 206 |
(* Binary union introduction rule *) |
11479 | 207 |
Goal "[| F: A leadsTo C; F: B leadsTo C |] ==> F : (A Un B) leadsTo C"; |
208 |
by (stac Un_eq_Union 1); |
|
12195 | 209 |
by (blast_tac (claset() addIs [leadsTo_Union] addDs [leadsToD2]) 1); |
11479 | 210 |
qed "leadsTo_Un"; |
211 |
||
12195 | 212 |
val [major, program, B] = Goal |
213 |
"[|(!!x. x:A==> F:{x} leadsTo B); F:program; st_set(B) |] ==> F:A leadsTo B"; |
|
214 |
by (res_inst_tac [("b", "A")] (UN_singleton RS subst) 1); |
|
215 |
by (rtac leadsTo_UN 1); |
|
216 |
by (auto_tac (claset() addDs prems, simpset() addsimps [major, program, B])); |
|
217 |
qed "single_leadsTo_I"; |
|
218 |
||
219 |
Goal "[| F:program; st_set(A) |] ==> F: A leadsTo A"; |
|
220 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
221 |
qed "leadsTo_refl"; |
|
222 |
||
223 |
Goal "F: A leadsTo A <-> F:program & st_set(A)"; |
|
224 |
by (auto_tac (claset() addIs [leadsTo_refl] |
|
225 |
addDs [leadsToD2], simpset())); |
|
226 |
qed "leadsTo_refl_iff"; |
|
227 |
||
228 |
Goal "F: 0 leadsTo B <-> (F:program & st_set(B))"; |
|
229 |
by (auto_tac (claset() addIs [subset_imp_leadsTo] |
|
230 |
addDs [leadsToD2], simpset())); |
|
231 |
qed "empty_leadsTo"; |
|
232 |
AddIffs [empty_leadsTo]; |
|
233 |
||
234 |
Goal "F: A leadsTo state <-> (F:program & st_set(A))"; |
|
235 |
by (auto_tac (claset() addIs [subset_imp_leadsTo] |
|
236 |
addDs [leadsToD2, st_setD], simpset())); |
|
237 |
qed "leadsTo_state"; |
|
238 |
AddIffs [leadsTo_state]; |
|
239 |
||
240 |
Goal "[| F:A leadsTo A'; A'<=B'; st_set(B') |] ==> F : A leadsTo B'"; |
|
241 |
by (blast_tac (claset() addDs [leadsToD2] |
|
242 |
addIs [subset_imp_leadsTo,leadsTo_Trans]) 1); |
|
243 |
qed "leadsTo_weaken_R"; |
|
244 |
||
245 |
Goal "[| F:A leadsTo A'; B<=A |] ==> F : B leadsTo A'"; |
|
12484 | 246 |
by (ftac leadsToD2 1); |
12195 | 247 |
by (blast_tac (claset() addIs [leadsTo_Trans,subset_imp_leadsTo, st_set_subset]) 1); |
248 |
qed_spec_mp "leadsTo_weaken_L"; |
|
249 |
||
250 |
Goal "[| F:A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F:B leadsTo B'"; |
|
12484 | 251 |
by (ftac leadsToD2 1); |
12195 | 252 |
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, |
253 |
leadsTo_Trans, leadsTo_refl]) 1); |
|
254 |
qed "leadsTo_weaken"; |
|
255 |
||
256 |
(* This rule has a nicer conclusion *) |
|
257 |
Goal "[| F:transient(A); state-A<=B; st_set(B)|] ==> F:A leadsTo B"; |
|
12484 | 258 |
by (ftac transientD2 1); |
12195 | 259 |
by (rtac leadsTo_weaken_R 1); |
260 |
by (auto_tac (claset(), simpset() addsimps [transient_imp_leadsTo])); |
|
261 |
qed "transient_imp_leadsTo2"; |
|
262 |
||
263 |
(*Distributes over binary unions*) |
|
264 |
Goal "F:(A Un B) leadsTo C <-> (F:A leadsTo C & F : B leadsTo C)"; |
|
265 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); |
|
266 |
qed "leadsTo_Un_distrib"; |
|
267 |
||
268 |
Goal |
|
269 |
"(F:(UN i:I. A(i)) leadsTo B)<-> ((ALL i : I. F: A(i) leadsTo B) & F:program & st_set(B))"; |
|
270 |
by (blast_tac (claset() addDs [leadsToD2] |
|
271 |
addIs [leadsTo_UN, leadsTo_weaken_L]) 1); |
|
272 |
qed "leadsTo_UN_distrib"; |
|
273 |
||
274 |
Goal "(F: Union(S) leadsTo B) <-> (ALL A:S. F : A leadsTo B) & F:program & st_set(B)"; |
|
275 |
by (blast_tac (claset() addDs [leadsToD2] |
|
276 |
addIs [leadsTo_Union, leadsTo_weaken_L]) 1); |
|
277 |
qed "leadsTo_Union_distrib"; |
|
278 |
||
279 |
(*Set difference: maybe combine with leadsTo_weaken_L?*) |
|
280 |
Goal "[| F: (A-B) leadsTo C; F: B leadsTo C; st_set(C) |] ==> F: A leadsTo C"; |
|
281 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken] |
|
282 |
addDs [leadsToD2]) 1); |
|
283 |
qed "leadsTo_Diff"; |
|
284 |
||
285 |
val [major,minor] = Goal |
|
286 |
"[|(!!i. i:I ==> F: A(i) leadsTo A'(i)); F:program |] \ |
|
287 |
\ ==> F: (UN i:I. A(i)) leadsTo (UN i:I. A'(i))"; |
|
288 |
by (rtac leadsTo_Union 1); |
|
289 |
by (ALLGOALS(Asm_simp_tac)); |
|
290 |
by Safe_tac; |
|
291 |
by (simp_tac (simpset() addsimps [minor]) 2); |
|
292 |
by (blast_tac (claset() addDs [leadsToD2, major])2); |
|
293 |
by (blast_tac (claset() addIs [leadsTo_weaken_R] addDs [major, leadsToD2]) 1); |
|
294 |
qed "leadsTo_UN_UN"; |
|
295 |
||
296 |
(*Binary union version*) |
|
297 |
Goal "[| F: A leadsTo A'; F:B leadsTo B' |] ==> F : (A Un B) leadsTo (A' Un B')"; |
|
298 |
by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B')" 1); |
|
299 |
by (blast_tac (claset() addDs [leadsToD2]) 2); |
|
300 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R]) 1); |
|
301 |
qed "leadsTo_Un_Un"; |
|
302 |
||
303 |
(** The cancellation law **) |
|
304 |
Goal "[|F: A leadsTo (A' Un B); F: B leadsTo B'|] ==> F: A leadsTo (A' Un B')"; |
|
305 |
by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B') &F:program" 1); |
|
306 |
by (blast_tac (claset() addDs [leadsToD2]) 2); |
|
307 |
by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_Un_Un, leadsTo_refl]) 1); |
|
308 |
qed "leadsTo_cancel2"; |
|
309 |
||
310 |
Goal "[|F: A leadsTo (A' Un B); F : (B-A') leadsTo B'|]==> F: A leadsTo (A' Un B')"; |
|
311 |
by (rtac leadsTo_cancel2 1); |
|
312 |
by (assume_tac 2); |
|
313 |
by (blast_tac (claset() addDs [leadsToD2] addIs [leadsTo_weaken_R]) 1); |
|
314 |
qed "leadsTo_cancel_Diff2"; |
|
315 |
||
11479 | 316 |
|
12195 | 317 |
Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] ==> F:A leadsTo (B' Un A')"; |
318 |
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
|
319 |
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); |
|
320 |
qed "leadsTo_cancel1"; |
|
11479 | 321 |
|
12195 | 322 |
Goal "[|F: A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F : A leadsTo (B' Un A')"; |
323 |
by (rtac leadsTo_cancel1 1); |
|
324 |
by (assume_tac 2); |
|
325 |
by (blast_tac (claset() addIs [leadsTo_weaken_R] addDs [leadsToD2]) 1); |
|
326 |
qed "leadsTo_cancel_Diff1"; |
|
11479 | 327 |
|
328 |
(*The INDUCTION rule as we should have liked to state it*) |
|
12195 | 329 |
val [major, basis_prem, trans_prem, union_prem] = Goalw [leadsTo_def, st_set_def] |
11479 | 330 |
"[| F: za leadsTo zb; \ |
12195 | 331 |
\ !!A B. [| F: A ensures B; st_set(A); st_set(B) |] ==> P(A, B); \ |
11479 | 332 |
\ !!A B C. [| F: A leadsTo B; P(A, B); \ |
333 |
\ F: B leadsTo C; P(B, C) |] \ |
|
334 |
\ ==> P(A, C); \ |
|
12195 | 335 |
\ !!B S. [| ALL A:S. F:A leadsTo B; ALL A:S. P(A, B); st_set(B); ALL A:S. st_set(A)|] \ |
11479 | 336 |
\ ==> P(Union(S), B) \ |
337 |
\ |] ==> P(za, zb)"; |
|
338 |
by (cut_facts_tac [major] 1); |
|
339 |
by (rtac (major RS CollectD2 RS leads.induct) 1); |
|
12195 | 340 |
by (rtac union_prem 3); |
341 |
by (rtac trans_prem 2); |
|
342 |
by (rtac basis_prem 1); |
|
343 |
by Auto_tac; |
|
11479 | 344 |
qed "leadsTo_induct"; |
345 |
||
12195 | 346 |
(* Added by Sidi, an induction rule without ensures *) |
347 |
val [major,imp_prem,basis_prem,trans_prem,union_prem] = Goal |
|
11479 | 348 |
"[| F: za leadsTo zb; \ |
12195 | 349 |
\ !!A B. [| A<=B; st_set(B) |] ==> P(A, B); \ |
350 |
\ !!A B. [| F:A co A Un B; F:transient(A); st_set(B) |] ==> P(A, B); \ |
|
11479 | 351 |
\ !!A B C. [| F: A leadsTo B; P(A, B); \ |
352 |
\ F: B leadsTo C; P(B, C) |] \ |
|
353 |
\ ==> P(A, C); \ |
|
12195 | 354 |
\ !!B S. [| ALL A:S. F:A leadsTo B; ALL A:S. P(A, B); st_set(B); ALL A:S. st_set(A) |] \ |
11479 | 355 |
\ ==> P(Union(S), B) \ |
356 |
\ |] ==> P(za, zb)"; |
|
357 |
by (cut_facts_tac [major] 1); |
|
358 |
by (etac leadsTo_induct 1); |
|
12195 | 359 |
by (auto_tac (claset() addIs [trans_prem,union_prem], simpset())); |
11479 | 360 |
by (rewrite_goal_tac [ensures_def] 1); |
12195 | 361 |
by (Clarify_tac 1); |
12484 | 362 |
by (ftac constrainsD2 1); |
11479 | 363 |
by (dres_inst_tac [("B'", "(A-B) Un B")] constrains_weaken_R 1); |
12195 | 364 |
by (Blast_tac 1); |
11479 | 365 |
by (forward_tac [ensuresI2 RS leadsTo_Basis] 1); |
12195 | 366 |
by (dtac basis_prem 4); |
367 |
by (ALLGOALS(Asm_full_simp_tac)); |
|
368 |
by (forw_inst_tac [("A1", "A"), ("B", "B")] (Int_lower2 RS imp_prem) 1); |
|
369 |
by (subgoal_tac "A=Union({A - B, A Int B})" 1); |
|
370 |
by (Blast_tac 2); |
|
371 |
by (etac ssubst 1); |
|
372 |
by (rtac union_prem 1); |
|
11479 | 373 |
by (auto_tac (claset() addIs [subset_imp_leadsTo], simpset())); |
374 |
qed "leadsTo_induct2"; |
|
375 |
||
376 |
(** Variant induction rule: on the preconditions for B **) |
|
377 |
(*Lemma is the weak version: can't see how to do it in one step*) |
|
378 |
val major::prems = Goal |
|
379 |
"[| F : za leadsTo zb; \ |
|
380 |
\ P(zb); \ |
|
12195 | 381 |
\ !!A B. [| F : A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A); \ |
382 |
\ !!S. [| ALL A:S. P(A); ALL A:S. st_set(A) |] ==> P(Union(S)) \ |
|
11479 | 383 |
\ |] ==> P(za)"; |
384 |
(*by induction on this formula*) |
|
385 |
by (subgoal_tac "P(zb) --> P(za)" 1); |
|
386 |
(*now solve first subgoal: this formula is sufficient*) |
|
387 |
by (blast_tac (claset() addIs leadsTo_refl::prems) 1); |
|
388 |
by (rtac (major RS leadsTo_induct) 1); |
|
389 |
by (REPEAT (blast_tac (claset() addIs prems) 1)); |
|
390 |
qed "lemma"; |
|
391 |
||
392 |
||
12195 | 393 |
val [major, zb_prem, basis_prem, union_prem] = Goal |
11479 | 394 |
"[| F : za leadsTo zb; \ |
395 |
\ P(zb); \ |
|
12195 | 396 |
\ !!A B. [| F : A ensures B; F : B leadsTo zb; P(B); st_set(A) |] ==> P(A); \ |
397 |
\ !!S. ALL A:S. F : A leadsTo zb & P(A) & st_set(A) ==> P(Union(S)) \ |
|
11479 | 398 |
\ |] ==> P(za)"; |
399 |
by (cut_facts_tac [major] 1); |
|
400 |
by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1); |
|
401 |
by (etac conjunct2 1); |
|
402 |
by (rtac (major RS lemma) 1); |
|
12195 | 403 |
by (blast_tac (claset() addDs [leadsToD2] |
404 |
addIs [leadsTo_Union,union_prem]) 3); |
|
405 |
by (blast_tac (claset() addIs [leadsTo_Trans,basis_prem, leadsTo_Basis]) 2); |
|
406 |
by (blast_tac (claset() addIs [leadsTo_refl,zb_prem] |
|
407 |
addDs [leadsToD2]) 1); |
|
11479 | 408 |
qed "leadsTo_induct_pre"; |
409 |
||
410 |
(** The impossibility law **) |
|
411 |
Goal |
|
412 |
"F : A leadsTo 0 ==> A=0"; |
|
413 |
by (etac leadsTo_induct_pre 1); |
|
12195 | 414 |
by (auto_tac (claset(), simpset() addsimps |
415 |
[ensures_def, constrains_def, transient_def, st_set_def])); |
|
416 |
by (dtac bspec 1); |
|
417 |
by (REPEAT(Blast_tac 1)); |
|
11479 | 418 |
qed "leadsTo_empty"; |
12195 | 419 |
Addsimps [leadsTo_empty]; |
11479 | 420 |
|
421 |
(** PSP: Progress-Safety-Progress **) |
|
422 |
||
423 |
(*Special case of PSP: Misra's "stable conjunction"*) |
|
424 |
Goalw [stable_def] |
|
12195 | 425 |
"[| F : A leadsTo A'; F : stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)"; |
11479 | 426 |
by (etac leadsTo_induct 1); |
427 |
by (rtac leadsTo_Union_Int 3); |
|
12195 | 428 |
by (ALLGOALS(Asm_simp_tac)); |
429 |
by (REPEAT(blast_tac (claset() addDs [constrainsD2]) 3)); |
|
11479 | 430 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
431 |
by (rtac leadsTo_Basis 1); |
|
432 |
by (asm_full_simp_tac (simpset() |
|
12220 | 433 |
addsimps [ensures_def, Diff_Int_distrib RS sym, |
434 |
Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1); |
|
11479 | 435 |
by (REPEAT(blast_tac (claset() |
436 |
addIs [transient_strengthen,constrains_Int] |
|
437 |
addDs [constrainsD2]) 1)); |
|
438 |
qed "psp_stable"; |
|
439 |
||
440 |
||
12195 | 441 |
Goal "[|F: A leadsTo A'; F : stable(B) |]==>F: (B Int A) leadsTo (B Int A')"; |
11479 | 442 |
by (asm_simp_tac (simpset() |
443 |
addsimps psp_stable::Int_ac) 1); |
|
444 |
qed "psp_stable2"; |
|
445 |
||
12195 | 446 |
Goalw [ensures_def, constrains_def, st_set_def] |
447 |
"[| F: A ensures A'; F: B co B' |]==> F: (A Int B') ensures ((A' Int B) Un (B' - B))"; |
|
11479 | 448 |
(*speeds up the proof*) |
449 |
by (Clarify_tac 1); |
|
450 |
by (blast_tac (claset() addIs [transient_strengthen]) 1); |
|
451 |
qed "psp_ensures"; |
|
452 |
||
12195 | 453 |
Goal |
454 |
"[|F:A leadsTo A'; F: B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (B' - B))"; |
|
455 |
by (subgoal_tac "F:program & st_set(A) & st_set(A')& st_set(B)" 1); |
|
456 |
by (blast_tac (claset() addSDs [constrainsD2, leadsToD2]) 2); |
|
11479 | 457 |
by (etac leadsTo_induct 1); |
458 |
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); |
|
459 |
(*Transitivity case has a delicate argument involving "cancellation"*) |
|
460 |
by (rtac leadsTo_Un_duplicate2 2); |
|
461 |
by (etac leadsTo_cancel_Diff1 2); |
|
462 |
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2); |
|
463 |
by (blast_tac (claset() addIs [leadsTo_weaken_L] |
|
464 |
addDs [constrains_imp_subset]) 2); |
|
465 |
(*Basis case*) |
|
12195 | 466 |
by (blast_tac (claset() addIs [psp_ensures, leadsTo_Basis]) 1); |
11479 | 467 |
qed "psp"; |
468 |
||
469 |
||
12195 | 470 |
Goal "[| F : A leadsTo A'; F : B co B'; st_set(B') |] \ |
11479 | 471 |
\ ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"; |
472 |
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); |
|
473 |
qed "psp2"; |
|
474 |
||
475 |
Goalw [unless_def] |
|
12195 | 476 |
"[| F : A leadsTo A'; F : B unless B'; st_set(B); st_set(B') |] \ |
11479 | 477 |
\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')"; |
12195 | 478 |
by (subgoal_tac "st_set(A)&st_set(A')" 1); |
479 |
by (blast_tac (claset() addDs [leadsToD2]) 2); |
|
11479 | 480 |
by (dtac psp 1); |
481 |
by (assume_tac 1); |
|
12195 | 482 |
by (Blast_tac 1); |
483 |
by (REPEAT(blast_tac (claset() addIs [leadsTo_weaken]) 1)); |
|
11479 | 484 |
qed "psp_unless"; |
485 |
||
12195 | 486 |
(*** Proving the wf induction rules ***) |
11479 | 487 |
(** The most general rule: r is any wf relation; f is any variant function **) |
488 |
Goal "[| wf(r); \ |
|
489 |
\ m:I; \ |
|
490 |
\ field(r)<=I; \ |
|
12195 | 491 |
\ F:program; st_set(B);\ |
11479 | 492 |
\ ALL m:I. F : (A Int f-``{m}) leadsTo \ |
493 |
\ ((A Int f-``(converse(r)``{m})) Un B) |] \ |
|
494 |
\ ==> F : (A Int f-``{m}) leadsTo B"; |
|
495 |
by (eres_inst_tac [("a","m")] wf_induct2 1); |
|
496 |
by (ALLGOALS(Asm_simp_tac)); |
|
497 |
by (subgoal_tac "F : (A Int (f-``(converse(r)``{x}))) leadsTo B" 1); |
|
498 |
by (stac vimage_eq_UN 2); |
|
12220 | 499 |
by (asm_simp_tac (simpset() delsimps UN_simps |
500 |
addsimps [Int_UN_distrib]) 2); |
|
11479 | 501 |
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); |
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
502 |
by (auto_tac (claset() addIs [leadsTo_UN], |
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
503 |
simpset() delsimps UN_simps addsimps [Int_UN_distrib])); |
11479 | 504 |
qed "lemma1"; |
505 |
||
506 |
(** Meta or object quantifier ? **) |
|
507 |
Goal "[| wf(r); \ |
|
508 |
\ field(r)<=I; \ |
|
509 |
\ A<=f-``I;\ |
|
12195 | 510 |
\ F:program; st_set(A); st_set(B); \ |
11479 | 511 |
\ ALL m:I. F : (A Int f-``{m}) leadsTo \ |
512 |
\ ((A Int f-``(converse(r)``{m})) Un B) |] \ |
|
513 |
\ ==> F : A leadsTo B"; |
|
514 |
by (res_inst_tac [("b", "A")] subst 1); |
|
515 |
by (res_inst_tac [("I", "I")] leadsTo_UN 2); |
|
516 |
by (REPEAT (assume_tac 2)); |
|
517 |
by (Clarify_tac 2); |
|
518 |
by (eres_inst_tac [("I", "I")] lemma1 2); |
|
519 |
by (REPEAT (assume_tac 2)); |
|
520 |
by (rtac equalityI 1); |
|
521 |
by Safe_tac; |
|
522 |
by (thin_tac "field(r)<=I" 1); |
|
523 |
by (dres_inst_tac [("c", "x")] subsetD 1); |
|
524 |
by Safe_tac; |
|
525 |
by (res_inst_tac [("b", "x")] UN_I 1); |
|
526 |
by Auto_tac; |
|
527 |
qed "leadsTo_wf_induct"; |
|
528 |
||
529 |
Goalw [field_def] "field(less_than(nat)) = nat"; |
|
530 |
by (simp_tac (simpset() addsimps [less_than_equals]) 1); |
|
531 |
by (rtac equalityI 1); |
|
12195 | 532 |
by (force_tac (claset(), simpset()) 1); |
11479 | 533 |
by (Clarify_tac 1); |
534 |
by (thin_tac "x~:range(?y)" 1); |
|
535 |
by (etac nat_induct 1); |
|
536 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [domain_def]))); |
|
537 |
by (res_inst_tac [("x", "<succ(xa),succ(succ(xa))>")] ReplaceI 2); |
|
538 |
by (res_inst_tac [("x", "<0,1>")] ReplaceI 1); |
|
539 |
by (REPEAT(force_tac (claset() addIs [splitI], simpset()) 1)); |
|
540 |
qed "nat_less_than_field"; |
|
541 |
||
542 |
(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*) |
|
543 |
Goal |
|
544 |
"[| A<=f-``nat;\ |
|
12195 | 545 |
\ F:program; st_set(A); st_set(B); \ |
11479 | 546 |
\ ALL m:nat. F:(A Int f-``{m}) leadsTo ((A Int f-``lessThan(m,nat)) Un B) |] \ |
547 |
\ ==> F : A leadsTo B"; |
|
548 |
by (res_inst_tac [("A1", "nat")] |
|
549 |
(wf_less_than RS leadsTo_wf_induct) 1); |
|
550 |
by (Clarify_tac 6); |
|
551 |
by (ALLGOALS(asm_full_simp_tac |
|
552 |
(simpset() addsimps [nat_less_than_field]))); |
|
553 |
by (Clarify_tac 1); |
|
554 |
by (ALLGOALS(asm_full_simp_tac |
|
555 |
(simpset() addsimps [rewrite_rule [vimage_def] Image_inverse_less_than]))); |
|
556 |
qed "lessThan_induct"; |
|
557 |
||
558 |
(*** wlt ****) |
|
559 |
||
560 |
(*Misra's property W3*) |
|
12195 | 561 |
Goalw [wlt_def] "wlt(F,B) <=state"; |
562 |
by Auto_tac; |
|
563 |
qed "wlt_type"; |
|
564 |
||
565 |
Goalw [st_set_def] "st_set(wlt(F, B))"; |
|
12484 | 566 |
by (rtac wlt_type 1); |
12195 | 567 |
qed "wlt_st_set"; |
568 |
AddIffs [wlt_st_set]; |
|
569 |
||
570 |
Goalw [wlt_def] "F:wlt(F, B) leadsTo B <-> (F:program & st_set(B))"; |
|
571 |
by (blast_tac (claset() addDs [leadsToD2] addSIs [leadsTo_Union]) 1); |
|
572 |
qed "wlt_leadsTo_iff"; |
|
573 |
||
574 |
(* [| F:program; st_set(B) |] ==> F:wlt(F, B) leadsTo B *) |
|
575 |
bind_thm("wlt_leadsTo", conjI RS (wlt_leadsTo_iff RS iffD2)); |
|
11479 | 576 |
|
577 |
Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt(F, B)"; |
|
12484 | 578 |
by (ftac leadsToD2 1); |
12195 | 579 |
by (auto_tac (claset(), simpset() addsimps [st_set_def])); |
11479 | 580 |
qed "leadsTo_subset"; |
581 |
||
582 |
(*Misra's property W2*) |
|
12195 | 583 |
Goal "F : A leadsTo B <-> (A <= wlt(F,B) & F:program & st_set(B))"; |
584 |
by Auto_tac; |
|
585 |
by (REPEAT(blast_tac (claset() addDs [leadsToD2,leadsTo_subset] |
|
586 |
addIs [leadsTo_weaken_L, wlt_leadsTo]) 1)); |
|
11479 | 587 |
qed "leadsTo_eq_subset_wlt"; |
588 |
||
589 |
(*Misra's property W4*) |
|
12195 | 590 |
Goal "[| F:program; st_set(B) |] ==> B <= wlt(F,B)"; |
591 |
by (rtac leadsTo_subset 1); |
|
11479 | 592 |
by (asm_simp_tac (simpset() |
593 |
addsimps [leadsTo_eq_subset_wlt RS iff_sym, |
|
594 |
subset_imp_leadsTo]) 1); |
|
595 |
qed "wlt_increasing"; |
|
596 |
||
597 |
(*Used in the Trans case below*) |
|
12195 | 598 |
Goalw [constrains_def, st_set_def] |
11479 | 599 |
"[| B <= A2; \ |
600 |
\ F : (A1 - B) co (A1 Un B); \ |
|
601 |
\ F : (A2 - C) co (A2 Un C) |] \ |
|
602 |
\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"; |
|
603 |
by (Clarify_tac 1); |
|
604 |
by (Blast_tac 1); |
|
605 |
qed "lemma1"; |
|
606 |
||
607 |
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
|
608 |
(* slightly different from the HOL one: B here is bounded *) |
|
609 |
Goal "F : A leadsTo A' \ |
|
12195 | 610 |
\ ==> EX B:Pow(state). A<=B & F:B leadsTo A' & F : (B-A') co (B Un A')"; |
12484 | 611 |
by (ftac leadsToD2 1); |
11479 | 612 |
by (etac leadsTo_induct 1); |
613 |
(*Basis*) |
|
12195 | 614 |
by (blast_tac (claset() addDs [ensuresD, constrainsD2, st_setD]) 1); |
11479 | 615 |
(*Trans*) |
616 |
by (Clarify_tac 1); |
|
617 |
by (res_inst_tac [("x", "Ba Un Bb")] bexI 1); |
|
618 |
by (blast_tac (claset() addIs [lemma1,leadsTo_Un_Un, leadsTo_cancel1, |
|
619 |
leadsTo_Un_duplicate]) 1); |
|
620 |
by (Blast_tac 1); |
|
621 |
(*Union*) |
|
622 |
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1]) 1); |
|
12195 | 623 |
by (subgoal_tac "EX y. y:Pi(S, %A. {Ba:Pow(state). A<=Ba & \ |
11479 | 624 |
\ F:Ba leadsTo B & F:Ba - B co Ba Un B})" 1); |
625 |
by (rtac AC_ball_Pi 2); |
|
12195 | 626 |
by (ALLGOALS(Clarify_tac)); |
627 |
by (rotate_tac 1 2); |
|
628 |
by (dres_inst_tac [("x", "x")] bspec 2); |
|
629 |
by (REPEAT(Blast_tac 2)); |
|
11479 | 630 |
by (res_inst_tac [("x", "UN A:S. y`A")] bexI 1); |
631 |
by Safe_tac; |
|
632 |
by (res_inst_tac [("I1", "S")] (constrains_UN RS constrains_weaken) 3); |
|
633 |
by (rtac leadsTo_Union 2); |
|
12195 | 634 |
by (blast_tac (claset() addSDs [apply_type]) 5); |
635 |
by (ALLGOALS(Asm_full_simp_tac)); |
|
636 |
by (REPEAT(force_tac (claset() addSDs [apply_type], simpset()) 1)); |
|
11479 | 637 |
qed "leadsTo_123"; |
638 |
||
639 |
||
640 |
(*Misra's property W5*) |
|
12195 | 641 |
Goal "[| F:program; st_set(B) |] ==>F : (wlt(F, B) - B) co (wlt(F,B))"; |
11479 | 642 |
by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); |
643 |
by (assume_tac 1); |
|
12195 | 644 |
by (Blast_tac 1); |
11479 | 645 |
by (Clarify_tac 1); |
646 |
by (subgoal_tac "Ba = wlt(F,B)" 1); |
|
647 |
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2); |
|
648 |
by (Clarify_tac 1); |
|
649 |
by (asm_full_simp_tac (simpset() |
|
650 |
addsimps [wlt_increasing RS (subset_Un_iff2 RS iffD1)]) 1); |
|
651 |
qed "wlt_constrains_wlt"; |
|
652 |
||
653 |
(*** Completion: Binary and General Finite versions ***) |
|
654 |
||
655 |
Goal "[| W = wlt(F, (B' Un C)); \ |
|
656 |
\ F : A leadsTo (A' Un C); F : A' co (A' Un C); \ |
|
657 |
\ F : B leadsTo (B' Un C); F : B' co (B' Un C) |] \ |
|
658 |
\ ==> F : (A Int B) leadsTo ((A' Int B') Un C)"; |
|
12195 | 659 |
by (subgoal_tac "st_set(C)&st_set(W)&st_set(W-C)&st_set(A')&st_set(A)\ |
660 |
\ & st_set(B) & st_set(B') & F:program" 1); |
|
661 |
by (Asm_simp_tac 2); |
|
662 |
by (blast_tac (claset() addSDs [leadsToD2]) 2); |
|
11479 | 663 |
by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1); |
664 |
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] |
|
12195 | 665 |
MRS constrains_Un RS constrains_weaken]) 2); |
11479 | 666 |
by (subgoal_tac "F : (W-C) co W" 1); |
12195 | 667 |
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing RS |
668 |
(subset_Un_iff2 RS iffD1), Un_assoc]) 2); |
|
11479 | 669 |
by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1); |
12195 | 670 |
by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2); |
671 |
(** LEVEL 9 **) |
|
11479 | 672 |
by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); |
673 |
by (rtac leadsTo_Un_duplicate2 2); |
|
12195 | 674 |
by (rtac leadsTo_Un_Un 2); |
675 |
by (blast_tac (claset() addIs [leadsTo_refl]) 3); |
|
676 |
by (res_inst_tac [("A'1", "B' Un C")] (wlt_leadsTo RS psp2 RS leadsTo_weaken) 2); |
|
677 |
by (REPEAT(Blast_tac 2)); |
|
678 |
(** LEVEL 17 **) |
|
11479 | 679 |
by (dtac leadsTo_Diff 1); |
12195 | 680 |
by (blast_tac (claset() addIs [subset_imp_leadsTo] |
681 |
addDs [leadsToD2, constrainsD2]) 1); |
|
682 |
by (force_tac (claset(), simpset() addsimps [st_set_def]) 1); |
|
11479 | 683 |
by (subgoal_tac "A Int B <= A Int W" 1); |
684 |
by (blast_tac (claset() addSDs [leadsTo_subset] |
|
685 |
addSIs [subset_refl RS Int_mono]) 2); |
|
12195 | 686 |
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); |
687 |
qed "completion_aux"; |
|
688 |
bind_thm("completion", refl RS completion_aux); |
|
11479 | 689 |
|
12195 | 690 |
Goal "[| I:Fin(X); F:program; st_set(C) |] ==> \ |
11479 | 691 |
\(ALL i:I. F : (A(i)) leadsTo (A'(i) Un C)) --> \ |
692 |
\ (ALL i:I. F : (A'(i)) co (A'(i) Un C)) --> \ |
|
693 |
\ F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)"; |
|
12220 | 694 |
by (etac Fin_induct 1); |
12195 | 695 |
by (auto_tac (claset(), simpset() addsimps [Inter_0])); |
11479 | 696 |
by (rtac completion 1); |
12220 | 697 |
by (auto_tac (claset(), |
698 |
simpset() delsimps INT_simps addsimps INT_extend_simps)); |
|
699 |
by (rtac constrains_INT 1); |
|
11479 | 700 |
by (REPEAT(Blast_tac 1)); |
701 |
qed "lemma"; |
|
702 |
||
703 |
val prems = Goal |
|
704 |
"[| I:Fin(X); \ |
|
705 |
\ !!i. i:I ==> F : A(i) leadsTo (A'(i) Un C); \ |
|
12195 | 706 |
\ !!i. i:I ==> F : A'(i) co (A'(i) Un C); F:program; st_set(C)|] \ |
11479 | 707 |
\ ==> F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)"; |
12195 | 708 |
by (resolve_tac [lemma RS mp RS mp] 1); |
709 |
by (resolve_tac prems 3); |
|
710 |
by (REPEAT(blast_tac (claset() addIs prems) 1)); |
|
11479 | 711 |
qed "finite_completion"; |
712 |
||
713 |
Goalw [stable_def] |
|
714 |
"[| F : A leadsTo A'; F : stable(A'); \ |
|
715 |
\ F : B leadsTo B'; F : stable(B') |] \ |
|
716 |
\ ==> F : (A Int B) leadsTo (A' Int B')"; |
|
717 |
by (res_inst_tac [("C1", "0")] (completion RS leadsTo_weaken_R) 1); |
|
12195 | 718 |
by (REPEAT(blast_tac (claset() addDs [leadsToD2, constrainsD2]) 5)); |
11479 | 719 |
by (ALLGOALS(Asm_full_simp_tac)); |
720 |
qed "stable_completion"; |
|
721 |
||
722 |
||
12195 | 723 |
val major::prems = Goalw [stable_def] |
11479 | 724 |
"[| I:Fin(X); \ |
12195 | 725 |
\ (!!i. i:I ==> F : A(i) leadsTo A'(i)); \ |
726 |
\ (!!i. i:I ==> F: stable(A'(i))); F:program |] \ |
|
11479 | 727 |
\ ==> F : (INT i:I. A(i)) leadsTo (INT i:I. A'(i))"; |
12195 | 728 |
by (cut_facts_tac [major] 1); |
729 |
by (subgoal_tac "st_set(INT i:I. A'(i))" 1); |
|
730 |
by (blast_tac (claset() addDs [leadsToD2]@prems) 2); |
|
11479 | 731 |
by (res_inst_tac [("C1", "0")] (finite_completion RS leadsTo_weaken_R) 1); |
12195 | 732 |
by (Asm_simp_tac 1); |
733 |
by (assume_tac 6); |
|
734 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps prems))); |
|
735 |
by (resolve_tac prems 2); |
|
736 |
by (resolve_tac prems 1); |
|
737 |
by Auto_tac; |
|
11479 | 738 |
qed "finite_stable_completion"; |
739 |