author | paulson |
Mon, 07 Dec 1998 18:26:46 +0100 | |
changeset 6020 | 4b109bf75976 |
parent 6012 | 1894bfc4aee9 |
child 6295 | 351b3c2b0d83 |
permissions | -rw-r--r-- |
5899 | 1 |
(* Title: HOL/UNITY/PPROD.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
*) |
|
6 |
||
6020 | 7 |
|
8 |
val rinst = read_instantiate_sg (sign_of thy); |
|
9 |
||
10 |
(*** General lemmas ***) |
|
5899 | 11 |
|
6020 | 12 |
Goalw [sharing_def] "((x,y): sharing Rsh A) = (x: A & y : range (Rsh x))"; |
13 |
by Auto_tac; |
|
14 |
qed "sharing_iff"; |
|
15 |
AddIffs [sharing_iff]; |
|
5899 | 16 |
|
6020 | 17 |
Goalw [sharing_def] "(sharing Rsh A <= sharing Rsh B) = (A <= B)"; |
18 |
by Auto_tac; |
|
19 |
qed "sharing_subset_iff"; |
|
20 |
AddIffs [sharing_subset_iff]; |
|
21 |
||
22 |
Goalw [sharing_def] "sharing Rsh (A Un B) = sharing Rsh A Un sharing Rsh B"; |
|
23 |
by Auto_tac; |
|
24 |
qed "sharing_Un_distrib"; |
|
5899 | 25 |
|
6020 | 26 |
Goalw [sharing_def] "sharing Rsh (A Int B) = sharing Rsh A Int sharing Rsh B"; |
27 |
by Auto_tac; |
|
28 |
qed "sharing_Int_distrib"; |
|
29 |
||
30 |
Goalw [sharing_def] "sharing Rsh (A - B) = sharing Rsh A - sharing Rsh B"; |
|
31 |
by Auto_tac; |
|
32 |
qed "sharing_Diff_distrib"; |
|
33 |
||
34 |
Goalw [sharing_def] "sharing Rsh (Union A) = (UN X:A. sharing Rsh X)"; |
|
5899 | 35 |
by (Blast_tac 1); |
6020 | 36 |
qed "sharing_Union"; |
5899 | 37 |
|
6020 | 38 |
Goal "(sharing Rsh A <= - sharing Rsh B) = (A <= - B)"; |
39 |
by (force_tac (claset(),simpset() addsimps [sharing_def, Image_iff]) 1); |
|
40 |
qed "Lcopy_subset_Compl_eq"; |
|
5899 | 41 |
|
6020 | 42 |
Goal "(((a,b), (a',b')) : Lcopy_act Rsh act) = \ |
43 |
\ ((a,a'):act & Rsh a b = b & Rsh a' b = b')"; |
|
44 |
by (simp_tac (simpset() addsimps [Lcopy_act_def]) 1); |
|
45 |
qed "mem_Lcopy_act_iff"; |
|
46 |
AddIffs [mem_Lcopy_act_iff]; |
|
5899 | 47 |
|
6020 | 48 |
(*NEEDED????????????????*) |
49 |
Goal "[| (a,a'):act; Rsh a b = b |] ==> (((a,b), (a', Rsh a' b)) : Lcopy_act Rsh act)"; |
|
5899 | 50 |
by Auto_tac; |
6020 | 51 |
qed "mem_Lcopy_actI"; |
5899 | 52 |
|
53 |
||
6020 | 54 |
Goal "act : Acts F \ |
55 |
\ ==> Lcopy_act Rsh act <= \ |
|
56 |
\ sharing Rsh (States F) Times sharing Rsh (States F)"; |
|
57 |
by (auto_tac (claset() addIs [range_eqI, sym] |
|
58 |
addDs [impOfSubs Acts_subset_Pow_States], |
|
59 |
simpset())); |
|
60 |
qed "Lcopy_act_subset_Times"; |
|
5899 | 61 |
|
6020 | 62 |
|
63 |
||
64 |
Open_locale "Share"; |
|
65 |
||
66 |
val overwrite = thm "overwrite"; |
|
67 |
Addsimps [overwrite]; |
|
5899 | 68 |
|
6020 | 69 |
Goal "Lcopy_act Rsh act ^^ sharing Rsh A = sharing Rsh (act ^^ A)"; |
70 |
by (force_tac (claset(),simpset() addsimps [sharing_def, Image_iff]) 1); |
|
71 |
qed "Lcopy_act_Image"; |
|
72 |
Addsimps [Lcopy_act_Image]; |
|
5899 | 73 |
|
6020 | 74 |
|
75 |
||
76 |
Goal "(Lcopy_act Rsh act ^^ sharing Rsh A <= sharing Rsh B) = (act ^^ A <= B)"; |
|
77 |
by (force_tac (claset(),simpset() addsimps [sharing_def, Image_iff]) 1); |
|
78 |
qed "Lcopy_act_Image_subset_eq"; |
|
5899 | 79 |
|
6020 | 80 |
Goal "Domain (Lcopy_act Rsh act) = sharing Rsh (Domain act)"; |
81 |
by (auto_tac (claset() addIs [sym], simpset() addsimps [Domain_iff])); |
|
82 |
qed "Domain_Lcopy_act"; |
|
5899 | 83 |
|
6020 | 84 |
(*?? needed?? |
85 |
Goal "(Lcopy_act Rsh act) ^^ (SIGMA x:A. B Int range(Rsh x)) = (SIGMA x: act^^A. Rsh x `` B)"; |
|
5899 | 86 |
by (auto_tac (claset(), simpset() addsimps [Image_iff])); |
6020 | 87 |
qed "Image_Lcopy_act"; |
88 |
**) |
|
89 |
||
90 |
Goal "Lcopy_act Rsh (diag A) = diag (sharing Rsh A)"; |
|
91 |
by (auto_tac (claset() addIs [sym], simpset())); |
|
92 |
qed "Lcopy_diag"; |
|
93 |
||
94 |
Addsimps [Lcopy_diag]; |
|
5899 | 95 |
|
96 |
||
97 |
(**** Lcopy ****) |
|
98 |
||
99 |
(*** Basic properties ***) |
|
100 |
||
6020 | 101 |
Goalw [Lcopy_def] "States (Lcopy Rsh F) = sharing Rsh (States F)"; |
102 |
by Auto_tac; |
|
103 |
qed "States_Lcopy"; |
|
104 |
||
105 |
Goalw [Lcopy_def] "Init (Lcopy Rsh F) = sharing Rsh (Init F)"; |
|
106 |
by (auto_tac (claset() addIs [impOfSubs Init_subset_States], simpset())); |
|
5899 | 107 |
qed "Init_Lcopy"; |
108 |
||
6020 | 109 |
Goal "diag (sharing Rsh (States F)) : Lcopy_act Rsh `` Acts F"; |
5899 | 110 |
by (rtac image_eqI 1); |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5972
diff
changeset
|
111 |
by (rtac diag_in_Acts 2); |
5899 | 112 |
by Auto_tac; |
113 |
val lemma = result(); |
|
114 |
||
6020 | 115 |
Goal "Acts (Lcopy Rsh F) = (Lcopy_act Rsh `` Acts F)"; |
116 |
by (auto_tac (claset() addSIs [lemma] |
|
117 |
addDs [impOfSubs Acts_subset_Pow_States], |
|
118 |
simpset() addsimps [Lcopy_def, Lcopy_act_subset_Times, |
|
119 |
image_subset_iff])); |
|
5899 | 120 |
qed "Acts_Lcopy"; |
121 |
||
6020 | 122 |
Addsimps [States_Lcopy, Init_Lcopy, Acts_Lcopy]; |
5899 | 123 |
|
6020 | 124 |
Goalw [SKIP_def] "Lcopy Rsh (SKIP A) = SKIP(sharing Rsh A)"; |
5899 | 125 |
by (rtac program_equalityI 1); |
126 |
by Auto_tac; |
|
127 |
qed "Lcopy_SKIP"; |
|
128 |
||
129 |
||
130 |
(*** Safety: constrains, stable ***) |
|
131 |
||
6020 | 132 |
Goal "(Lcopy Rsh F : constrains (sharing Rsh A) (sharing Rsh B)) = \ |
133 |
\ (F : constrains A B)"; |
|
134 |
by (simp_tac (simpset() addsimps [constrains_def, |
|
135 |
Lcopy_act_Image_subset_eq]) 1); |
|
5899 | 136 |
qed "Lcopy_constrains"; |
137 |
||
6020 | 138 |
Goal "[| Lcopy Rsh F : constrains A B; A <= States (Lcopy Rsh F) |] \ |
139 |
\ ==> F : constrains (Domain A) (Domain B)"; |
|
140 |
by (force_tac (claset() addIs [rev_bexI], |
|
141 |
simpset() addsimps [constrains_def, sharing_def, Image_iff]) 1); |
|
5899 | 142 |
qed "Lcopy_constrains_Domain"; |
143 |
||
6020 | 144 |
Goal "(Lcopy Rsh F : stable (sharing Rsh A)) = (F : stable A)"; |
5899 | 145 |
by (asm_simp_tac (simpset() addsimps [stable_def, Lcopy_constrains]) 1); |
146 |
qed "Lcopy_stable"; |
|
147 |
||
6020 | 148 |
Goal "(Lcopy Rsh F : invariant (sharing Rsh A)) = (F : invariant A)"; |
149 |
by (asm_simp_tac (simpset() addsimps [invariant_def, Lcopy_stable]) 1); |
|
5899 | 150 |
qed "Lcopy_invariant"; |
151 |
||
152 |
(** Substitution Axiom versions: Constrains, Stable **) |
|
153 |
||
6020 | 154 |
Goal "p : reachable (Lcopy Rsh F) \ |
155 |
\ ==> (%(a,b). a : reachable F & b : range (Rsh a)) p"; |
|
5899 | 156 |
by (etac reachable.induct 1); |
157 |
by (auto_tac |
|
158 |
(claset() addIs reachable.intrs, |
|
159 |
simpset() addsimps [Acts_Lcopy])); |
|
160 |
qed "reachable_Lcopy_fst"; |
|
161 |
||
6020 | 162 |
Goal "(a,b) : reachable (Lcopy Rsh F) \ |
163 |
\ ==> a : reachable F & b : range (Rsh a)"; |
|
5899 | 164 |
by (force_tac (claset() addSDs [reachable_Lcopy_fst], simpset()) 1); |
165 |
qed "reachable_LcopyD"; |
|
166 |
||
6020 | 167 |
Goal "reachable (Lcopy Rsh F) = sharing Rsh (reachable F)"; |
5899 | 168 |
by (rtac equalityI 1); |
169 |
by (force_tac (claset() addSDs [reachable_LcopyD], simpset()) 1); |
|
170 |
by (Clarify_tac 1); |
|
171 |
by (etac reachable.induct 1); |
|
172 |
by (ALLGOALS (force_tac (claset() addIs reachable.intrs, |
|
6020 | 173 |
simpset()))); |
5899 | 174 |
qed "reachable_Lcopy_eq"; |
175 |
||
6020 | 176 |
Goal "(Lcopy Rsh F : Constrains (sharing Rsh A) (sharing Rsh B)) = \ |
5899 | 177 |
\ (F : Constrains A B)"; |
178 |
by (simp_tac |
|
179 |
(simpset() addsimps [Constrains_def, reachable_Lcopy_eq, |
|
6020 | 180 |
Lcopy_constrains, sharing_Int_distrib RS sym]) 1); |
5899 | 181 |
qed "Lcopy_Constrains"; |
182 |
||
6020 | 183 |
Goal "(Lcopy Rsh F : Stable (sharing Rsh A)) = (F : Stable A)"; |
5899 | 184 |
by (simp_tac (simpset() addsimps [Stable_def, Lcopy_Constrains]) 1); |
185 |
qed "Lcopy_Stable"; |
|
186 |
||
187 |
||
188 |
(*** Progress: transient, ensures ***) |
|
189 |
||
6020 | 190 |
Goal "(Lcopy Rsh F : transient (sharing Rsh A)) = (F : transient A)"; |
5899 | 191 |
by (auto_tac (claset(), |
6020 | 192 |
simpset() addsimps [transient_def, Lcopy_subset_Compl_eq, |
193 |
Domain_Lcopy_act])); |
|
5899 | 194 |
qed "Lcopy_transient"; |
195 |
||
6020 | 196 |
Goal "(Lcopy Rsh F : ensures (sharing Rsh A) (sharing Rsh B)) = \ |
5899 | 197 |
\ (F : ensures A B)"; |
198 |
by (simp_tac |
|
199 |
(simpset() addsimps [ensures_def, Lcopy_constrains, Lcopy_transient, |
|
6020 | 200 |
sharing_Un_distrib RS sym, |
201 |
sharing_Diff_distrib RS sym]) 1); |
|
5899 | 202 |
qed "Lcopy_ensures"; |
203 |
||
6020 | 204 |
Goal "F : leadsTo A B \ |
205 |
\ ==> Lcopy Rsh F : leadsTo (sharing Rsh A) (sharing Rsh B)"; |
|
5899 | 206 |
by (etac leadsTo_induct 1); |
6020 | 207 |
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, sharing_Union]) 3); |
5899 | 208 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
209 |
by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, Lcopy_ensures]) 1); |
|
210 |
qed "leadsTo_imp_Lcopy_leadsTo"; |
|
211 |
||
5972 | 212 |
(** |
6020 | 213 |
Goal "Lcopy Rsh F : ensures A B ==> F : ensures (Domain A) (Domain B)"; |
5972 | 214 |
by (full_simp_tac |
215 |
(simpset() addsimps [ensures_def, Lcopy_constrains, Lcopy_transient, |
|
216 |
Domain_Un_eq RS sym, |
|
6020 | 217 |
sharing_Un_distrib RS sym, |
218 |
sharing_Diff_distrib RS sym]) 1); |
|
5972 | 219 |
by (safe_tac (claset() addSDs [Lcopy_constrains_Domain])); |
220 |
by (etac constrains_weaken_L 1); |
|
221 |
by (Blast_tac 1); |
|
222 |
(*NOT able to prove this: |
|
6020 | 223 |
Lcopy Rsh F : ensures A B ==> F : ensures (Domain A) (Domain B) |
224 |
1. [| Lcopy Rsh F : transient (A - B); |
|
5972 | 225 |
F : constrains (Domain (A - B)) (Domain (A Un B)) |] |
226 |
==> F : transient (Domain A - Domain B) |
|
227 |
**) |
|
5899 | 228 |
|
229 |
||
6020 | 230 |
Goal "Lcopy Rsh F : leadsTo AU BU ==> F : leadsTo (Domain AU) (Domain BU)"; |
5972 | 231 |
by (etac leadsTo_induct 1); |
232 |
by (full_simp_tac (simpset() addsimps [Domain_Union]) 3); |
|
233 |
by (blast_tac (claset() addIs [leadsTo_UN]) 3); |
|
234 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
235 |
by (rtac leadsTo_Basis 1); |
|
236 |
(*...and so CANNOT PROVE THIS*) |
|
5899 | 237 |
|
238 |
||
5972 | 239 |
(*This also seems impossible to prove??*) |
6020 | 240 |
Goal "(Lcopy Rsh F : leadsTo (sharing Rsh A) (sharing Rsh B)) = \ |
5972 | 241 |
\ (F : leadsTo A B)"; |
242 |
**) |
|
5899 | 243 |
|
244 |
||
245 |
(**** PPROD ****) |
|
246 |
||
247 |
(*** Basic properties ***) |
|
248 |
||
6020 | 249 |
Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)"; |
250 |
by Auto_tac; |
|
251 |
qed "lift_set_iff"; |
|
252 |
AddIffs [lift_set_iff]; |
|
253 |
||
254 |
Goalw [lift_act_def] "lift_act i (diag A) = (diag (lift_set i A))"; |
|
5899 | 255 |
by Auto_tac; |
6020 | 256 |
qed "lift_act_diag"; |
257 |
Addsimps [lift_act_diag]; |
|
5899 | 258 |
|
6020 | 259 |
Goalw [lift_prog_def] "States (lift_prog i F) = (lift_set i (States F))"; |
5972 | 260 |
by Auto_tac; |
6020 | 261 |
qed "States_lift_prog"; |
262 |
Addsimps [States_lift_prog]; |
|
263 |
||
264 |
Goalw [lift_prog_def] "Init (lift_prog i F) = (lift_set i (Init F))"; |
|
265 |
by (auto_tac (claset() addIs [impOfSubs Init_subset_States], simpset())); |
|
5972 | 266 |
qed "Init_lift_prog"; |
267 |
Addsimps [Init_lift_prog]; |
|
268 |
||
6020 | 269 |
Goalw [lift_act_def] |
270 |
"act : Acts F \ |
|
271 |
\ ==> lift_act i act <= lift_set i (States F) Times lift_set i (States F)"; |
|
272 |
by (force_tac (claset() addIs [range_eqI, sym] |
|
273 |
addDs [impOfSubs Acts_subset_Pow_States], |
|
274 |
simpset()) 1); |
|
275 |
qed "lift_act_subset_Times"; |
|
276 |
||
5972 | 277 |
Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; |
6020 | 278 |
by (auto_tac (claset() addIs [diag_in_Acts RSN (2,image_eqI)], |
279 |
simpset() addsimps [lift_act_subset_Times, |
|
280 |
image_subset_iff])); |
|
5972 | 281 |
qed "Acts_lift_prog"; |
282 |
||
6020 | 283 |
Goalw [PPROD_def] "States (PPROD I F) = (INT i:I. lift_set i (States (F i)))"; |
284 |
by Auto_tac; |
|
285 |
qed "States_PPROD"; |
|
286 |
Addsimps [States_PPROD]; |
|
287 |
||
288 |
Goalw [PPROD_def] "Init (PPROD I F) = (INT i:I. lift_set i (Init (F i)))"; |
|
5972 | 289 |
by Auto_tac; |
290 |
qed "Init_PPROD"; |
|
291 |
Addsimps [Init_PPROD]; |
|
292 |
||
5899 | 293 |
Goalw [lift_act_def] |
294 |
"((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
|
295 |
by (Blast_tac 1); |
|
296 |
qed "lift_act_eq"; |
|
297 |
AddIffs [lift_act_eq]; |
|
298 |
||
6020 | 299 |
Goalw [eqStates_def] "eqStates I (%i. lift_prog i F)"; |
300 |
||
301 |
Goalw [eqStates_def] "eqStates I (%i. lift_prog i (F i))"; |
|
302 |
||
303 |
Goal "[| eqStates I (%i. lift_prog i (F i)); i: I |] \ |
|
304 |
\ ==> Acts (PPROD I F) = (UN i:I. lift_act i `` Acts (F i))"; |
|
5899 | 305 |
by (auto_tac (claset(), |
5972 | 306 |
simpset() addsimps [PPROD_def, Acts_lift_prog, Acts_JN])); |
5899 | 307 |
qed "Acts_PPROD"; |
308 |
||
6020 | 309 |
Goal "PPROD {} F = SKIP UNIV"; |
310 |
by (simp_tac (simpset() addsimps [PPROD_def]) 1); |
|
311 |
qed "Acts_PPROD"; |
|
312 |
||
313 |
Goal "i : I ==> (PPI i: I. SKIP A) = SKIP (INT i:I. lift_set i A)"; |
|
5972 | 314 |
by (auto_tac (claset() addSIs [program_equalityI], |
6020 | 315 |
simpset() addsimps [eqStates_def, Acts_lift_prog, |
316 |
SKIP_def, Acts_PPROD])); |
|
5899 | 317 |
qed "PPROD_SKIP"; |
318 |
||
319 |
Goal "PPROD {} F = SKIP"; |
|
320 |
by (simp_tac (simpset() addsimps [PPROD_def]) 1); |
|
321 |
qed "PPROD_empty"; |
|
322 |
||
323 |
Addsimps [PPROD_SKIP, PPROD_empty]; |
|
324 |
||
5972 | 325 |
Goalw [PPROD_def] |
326 |
"PPROD (insert i I) F = (lift_prog i (F i)) Join (PPROD I F)"; |
|
5899 | 327 |
by Auto_tac; |
328 |
qed "PPROD_insert"; |
|
329 |
||
5972 | 330 |
Goalw [PPROD_def] "i : I ==> component (lift_prog i (F i)) (PPROD I F)"; |
331 |
(*blast_tac doesn't use HO unification*) |
|
332 |
by (fast_tac (claset() addIs [component_JN]) 1); |
|
333 |
qed "component_PPROD"; |
|
5899 | 334 |
|
5972 | 335 |
|
336 |
(*** Safety: constrains, stable, invariant ***) |
|
337 |
||
338 |
(** 1st formulation of lifting **) |
|
5899 | 339 |
|
6020 | 340 |
Goal "(lift_prog i F : constrains (lift_set i A) (lift_set i B)) = \ |
5972 | 341 |
\ (F : constrains A B)"; |
342 |
by (auto_tac (claset(), |
|
343 |
simpset() addsimps [constrains_def, Acts_lift_prog])); |
|
344 |
by (Blast_tac 2); |
|
345 |
by (Force_tac 1); |
|
346 |
qed "lift_prog_constrains_eq"; |
|
347 |
||
6020 | 348 |
Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)"; |
5972 | 349 |
by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1); |
350 |
qed "lift_prog_stable_eq"; |
|
351 |
||
352 |
(*This one looks strange! Proof probably is by case analysis on i=j.*) |
|
353 |
Goal "F i : constrains A B \ |
|
6020 | 354 |
\ ==> lift_prog j (F j) : constrains (lift_set i A) (lift_set i B)"; |
5972 | 355 |
by (auto_tac (claset(), |
356 |
simpset() addsimps [constrains_def, Acts_lift_prog])); |
|
357 |
by (REPEAT (Blast_tac 1)); |
|
358 |
qed "constrains_imp_lift_prog_constrains"; |
|
5899 | 359 |
|
360 |
Goal "i : I ==> \ |
|
6020 | 361 |
\ (PPROD I F : constrains (lift_set i A) (lift_set i B)) = \ |
5972 | 362 |
\ (F i : constrains A B)"; |
363 |
by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
|
364 |
by (blast_tac (claset() addIs [lift_prog_constrains_eq RS iffD1, |
|
365 |
constrains_imp_lift_prog_constrains]) 1); |
|
5899 | 366 |
qed "PPROD_constrains"; |
367 |
||
6020 | 368 |
Goal "i : I ==> (PPROD I F : stable (lift_set i A)) = (F i : stable A)"; |
5972 | 369 |
by (asm_simp_tac (simpset() addsimps [stable_def, PPROD_constrains]) 1); |
370 |
qed "PPROD_stable"; |
|
371 |
||
372 |
||
373 |
(** 2nd formulation of lifting **) |
|
374 |
||
375 |
Goal "[| lift_prog i F : constrains AA BB |] \ |
|
5899 | 376 |
\ ==> F : constrains (Applyall AA i) (Applyall BB i)"; |
377 |
by (auto_tac (claset(), |
|
378 |
simpset() addsimps [Applyall_def, constrains_def, |
|
5972 | 379 |
Acts_lift_prog])); |
380 |
by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
|
5899 | 381 |
simpset()) 1); |
5972 | 382 |
qed "lift_prog_constrains_projection"; |
383 |
||
384 |
Goal "[| PPROD I F : constrains AA BB; i: I |] \ |
|
385 |
\ ==> F i : constrains (Applyall AA i) (Applyall BB i)"; |
|
386 |
by (rtac lift_prog_constrains_projection 1); |
|
387 |
(*rotate this assumption to be last*) |
|
388 |
by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1); |
|
389 |
by (asm_full_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
|
5899 | 390 |
qed "PPROD_constrains_projection"; |
391 |
||
392 |
||
5972 | 393 |
(** invariant **) |
394 |
||
6020 | 395 |
Goal "F : invariant A ==> lift_prog i F : invariant (lift_set i A)"; |
5972 | 396 |
by (auto_tac (claset(), |
397 |
simpset() addsimps [invariant_def, lift_prog_stable_eq])); |
|
398 |
qed "invariant_imp_lift_prog_invariant"; |
|
5899 | 399 |
|
6020 | 400 |
Goal "[| lift_prog i F : invariant (lift_set i A) |] ==> F : invariant A"; |
5972 | 401 |
by (auto_tac (claset(), |
402 |
simpset() addsimps [invariant_def, lift_prog_stable_eq])); |
|
403 |
qed "lift_prog_invariant_imp_invariant"; |
|
404 |
||
405 |
(*NOT clear that the previous lemmas help in proving this one.*) |
|
6020 | 406 |
Goal "[| F i : invariant A; i : I |] ==> PPROD I F : invariant (lift_set i A)"; |
5972 | 407 |
by (auto_tac (claset(), |
408 |
simpset() addsimps [invariant_def, PPROD_stable])); |
|
409 |
qed "invariant_imp_PPROD_invariant"; |
|
410 |
||
411 |
(*The f0 premise ensures that the product is well-defined.*) |
|
6020 | 412 |
Goal "[| PPROD I F : invariant (lift_set i A); i : I; \ |
5972 | 413 |
\ f0: Init (PPROD I F) |] ==> F i : invariant A"; |
5899 | 414 |
by (auto_tac (claset(), |
415 |
simpset() addsimps [invariant_def, PPROD_stable])); |
|
5972 | 416 |
by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1); |
417 |
by Auto_tac; |
|
418 |
qed "PPROD_invariant_imp_invariant"; |
|
419 |
||
420 |
Goal "[| i : I; f0: Init (PPROD I F) |] \ |
|
6020 | 421 |
\ ==> (PPROD I F : invariant (lift_set i A)) = (F i : invariant A)"; |
5972 | 422 |
by (blast_tac (claset() addIs [invariant_imp_PPROD_invariant, |
423 |
PPROD_invariant_imp_invariant]) 1); |
|
5899 | 424 |
qed "PPROD_invariant"; |
425 |
||
5972 | 426 |
(*The f0 premise isn't needed if F is a constant program because then |
427 |
we get an initial state by replicating that of F*) |
|
428 |
Goal "i : I \ |
|
6020 | 429 |
\ ==> ((PPI x:I. F) : invariant (lift_set i A)) = (F : invariant A)"; |
5972 | 430 |
by (auto_tac (claset(), |
431 |
simpset() addsimps [invariant_def, PPROD_stable])); |
|
432 |
qed "PFUN_invariant"; |
|
433 |
||
5899 | 434 |
|
5972 | 435 |
(*** Substitution Axiom versions: Constrains, Stable ***) |
5899 | 436 |
|
5972 | 437 |
(** Reachability **) |
438 |
||
439 |
Goal "[| f : reachable (PPROD I F); i : I |] ==> f i : reachable (F i)"; |
|
5899 | 440 |
by (etac reachable.induct 1); |
441 |
by (auto_tac |
|
442 |
(claset() addIs reachable.intrs, |
|
443 |
simpset() addsimps [Acts_PPROD])); |
|
444 |
qed "reachable_PPROD"; |
|
445 |
||
5972 | 446 |
Goal "reachable (PPROD I F) <= {f. ALL i:I. f i : reachable (F i)}"; |
5899 | 447 |
by (force_tac (claset() addSDs [reachable_PPROD], simpset()) 1); |
448 |
qed "reachable_PPROD_subset1"; |
|
449 |
||
5972 | 450 |
Goal "[| i ~: I; A : reachable (F i) |] \ |
451 |
\ ==> ALL f. f : reachable (PPROD I F) \ |
|
452 |
\ --> f(i:=A) : reachable (lift_prog i (F i) Join PPROD I F)"; |
|
5899 | 453 |
by (etac reachable.induct 1); |
454 |
by (ALLGOALS Clarify_tac); |
|
455 |
by (etac reachable.induct 1); |
|
456 |
(*Init, Init case*) |
|
457 |
by (force_tac (claset() addIs reachable.intrs, |
|
5972 | 458 |
simpset() addsimps [Acts_lift_prog]) 1); |
5899 | 459 |
(*Init of F, action of PPROD F case*) |
5972 | 460 |
by (rtac reachable.Acts 1); |
5899 | 461 |
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
5972 | 462 |
by (assume_tac 1); |
5899 | 463 |
by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
464 |
(*induction over the 2nd "reachable" assumption*) |
|
465 |
by (eres_inst_tac [("xa","f")] reachable.induct 1); |
|
466 |
(*Init of PPROD F, action of F case*) |
|
467 |
by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
|
5972 | 468 |
by (force_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join]) 1); |
5899 | 469 |
by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
470 |
by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
|
471 |
(*last case: an action of PPROD I F*) |
|
5972 | 472 |
by (rtac reachable.Acts 1); |
5899 | 473 |
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
5972 | 474 |
by (assume_tac 1); |
5899 | 475 |
by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
476 |
qed_spec_mp "reachable_lift_Join_PPROD"; |
|
477 |
||
478 |
||
479 |
(*The index set must be finite: otherwise infinitely many copies of F can |
|
480 |
perform actions, and PPROD can never catch up in finite time.*) |
|
5972 | 481 |
Goal "finite I \ |
482 |
\ ==> {f. ALL i:I. f i : reachable (F i)} <= reachable (PPROD I F)"; |
|
5899 | 483 |
by (etac finite_induct 1); |
484 |
by (Simp_tac 1); |
|
485 |
by (force_tac (claset() addDs [reachable_lift_Join_PPROD], |
|
486 |
simpset() addsimps [PPROD_insert]) 1); |
|
487 |
qed "reachable_PPROD_subset2"; |
|
488 |
||
5972 | 489 |
Goal "finite I ==> \ |
490 |
\ reachable (PPROD I F) = {f. ALL i:I. f i : reachable (F i)}"; |
|
5899 | 491 |
by (REPEAT_FIRST (ares_tac [equalityI, |
492 |
reachable_PPROD_subset1, |
|
493 |
reachable_PPROD_subset2])); |
|
494 |
qed "reachable_PPROD_eq"; |
|
495 |
||
496 |
||
5972 | 497 |
(** Constrains **) |
5899 | 498 |
|
5972 | 499 |
Goal "[| F i : Constrains A B; i: I; finite I |] \ |
6020 | 500 |
\ ==> PPROD I F : Constrains (lift_set i A) (lift_set i B)"; |
5899 | 501 |
by (auto_tac |
502 |
(claset(), |
|
503 |
simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
|
504 |
reachable_PPROD_eq])); |
|
505 |
by (auto_tac (claset(), |
|
5972 | 506 |
simpset() addsimps [constrains_def, Acts_lift_prog, PPROD_def, |
5899 | 507 |
Acts_JN])); |
508 |
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
|
5972 | 509 |
qed "Constrains_imp_PPROD_Constrains"; |
510 |
||
511 |
Goal "[| ALL i:I. f0 i : R i; i: I |] \ |
|
512 |
\ ==> Applyall {f. (ALL i:I. f i : R i) & f i : A} i = R i Int A"; |
|
513 |
by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI], |
|
514 |
simpset() addsimps [Applyall_def]) 1); |
|
515 |
qed "Applyall_Int_depend"; |
|
516 |
||
517 |
(*Again, we need the f0 premise because otherwise Constrains holds trivially |
|
518 |
for PPROD I F.*) |
|
6020 | 519 |
Goal "[| PPROD I F : Constrains (lift_set i A) (lift_set i B); \ |
5972 | 520 |
\ i: I; finite I; f0: Init (PPROD I F) |] \ |
521 |
\ ==> F i : Constrains A B"; |
|
522 |
by (full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
|
523 |
by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1); |
|
524 |
by (blast_tac (claset() addIs [reachable.Init]) 2); |
|
525 |
by (dtac PPROD_constrains_projection 1); |
|
526 |
by (assume_tac 1); |
|
527 |
by (asm_full_simp_tac |
|
528 |
(simpset() addsimps [Applyall_Int_depend, Collect_conj_eq RS sym, |
|
529 |
reachable_PPROD_eq]) 1); |
|
530 |
qed "PPROD_Constrains_imp_Constrains"; |
|
5899 | 531 |
|
532 |
||
5972 | 533 |
Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \ |
6020 | 534 |
\ ==> (PPROD I F : Constrains (lift_set i A) (lift_set i B)) = \ |
5972 | 535 |
\ (F i : Constrains A B)"; |
536 |
by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, |
|
537 |
PPROD_Constrains_imp_Constrains]) 1); |
|
538 |
qed "PPROD_Constrains"; |
|
539 |
||
540 |
Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \ |
|
6020 | 541 |
\ ==> (PPROD I F : Stable (lift_set i A)) = (F i : Stable A)"; |
5972 | 542 |
by (asm_simp_tac (simpset() delsimps [Init_PPROD] |
543 |
addsimps [Stable_def, PPROD_Constrains]) 1); |
|
5899 | 544 |
qed "PPROD_Stable"; |
545 |
||
546 |
||
5972 | 547 |
(** PFUN (no dependence on i) doesn't require the f0 premise **) |
5899 | 548 |
|
5972 | 549 |
Goal "i: I ==> Applyall {f. (ALL i:I. f i : R) & f i : A} i = R Int A"; |
550 |
by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1); |
|
551 |
qed "Applyall_Int"; |
|
552 |
||
6020 | 553 |
Goal "[| (PPI x:I. F) : Constrains (lift_set i A) (lift_set i B); \ |
5972 | 554 |
\ i: I; finite I |] \ |
555 |
\ ==> F : Constrains A B"; |
|
556 |
by (full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
|
557 |
by (dtac PPROD_constrains_projection 1); |
|
558 |
by (assume_tac 1); |
|
559 |
by (asm_full_simp_tac |
|
560 |
(simpset() addsimps [Applyall_Int, Collect_conj_eq RS sym, |
|
561 |
reachable_PPROD_eq]) 1); |
|
562 |
qed "PFUN_Constrains_imp_Constrains"; |
|
563 |
||
564 |
Goal "[| i: I; finite I |] \ |
|
6020 | 565 |
\ ==> ((PPI x:I. F) : Constrains (lift_set i A) (lift_set i B)) = \ |
5972 | 566 |
\ (F : Constrains A B)"; |
567 |
by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, |
|
568 |
PFUN_Constrains_imp_Constrains]) 1); |
|
569 |
qed "PFUN_Constrains"; |
|
570 |
||
571 |
Goal "[| i: I; finite I |] \ |
|
6020 | 572 |
\ ==> ((PPI x:I. F) : Stable (lift_set i A)) = (F : Stable A)"; |
5972 | 573 |
by (asm_simp_tac (simpset() addsimps [Stable_def, PFUN_Constrains]) 1); |
574 |
qed "PFUN_Stable"; |
|
575 |
||
576 |
||
577 |
||
578 |
(*** guarantees properties ***) |
|
579 |
||
580 |
(*We only need act2=Id but the condition used is very weak*) |
|
6020 | 581 |
Goal "(x,y): act2 ==> fst_act (act1 Lcopy_act act2) = act1"; |
582 |
by (auto_tac (claset(), simpset() addsimps [fst_act_def, Lcopy_act_def])); |
|
583 |
qed "fst_act_Lcopy_act"; |
|
584 |
Addsimps [fst_act_Lcopy_act]; |
|
5972 | 585 |
|
586 |
||
6020 | 587 |
Goal "(Lcopy Rsh F) Join G = Lcopy H ==> EX J. H = F Join J"; |
5972 | 588 |
by (etac program_equalityE 1); |
589 |
by (auto_tac (claset(), simpset() addsimps [Acts_Join])); |
|
590 |
by (res_inst_tac |
|
591 |
[("x", "mk_program(Domain (Init G), fst_act `` Acts G)")] exI 1); |
|
592 |
by (rtac program_equalityI 1); |
|
593 |
(*Init*) |
|
594 |
by (simp_tac (simpset() addsimps [Acts_Join]) 1); |
|
595 |
by (blast_tac (claset() addEs [equalityE]) 1); |
|
596 |
(*Now for the Actions*) |
|
597 |
by (dres_inst_tac [("f", "op `` fst_act")] arg_cong 1); |
|
598 |
by (asm_full_simp_tac |
|
599 |
(simpset() addsimps [insert_absorb, Acts_Lcopy, Acts_Join, |
|
600 |
image_Un, image_compose RS sym, o_def]) 1); |
|
601 |
qed "Lcopy_Join_eq_Lcopy_D"; |
|
602 |
||
603 |
||
604 |
Goal "F : X guarantees Y \ |
|
6020 | 605 |
\ ==> Lcopy Rsh F : (Lcopy `` X) guarantees (Lcopy `` Y)"; |
5972 | 606 |
by (rtac guaranteesI 1); |
607 |
by Auto_tac; |
|
608 |
by (blast_tac (claset() addDs [Lcopy_Join_eq_Lcopy_D, guaranteesD]) 1); |
|
609 |
qed "Lcopy_guarantees"; |
|
610 |
||
611 |
||
612 |
Goal "drop_act i (lift_act i act) = act"; |
|
613 |
by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI], |
|
614 |
simpset() addsimps [drop_act_def, lift_act_def]) 1); |
|
615 |
qed "lift_act_inverse"; |
|
616 |
Addsimps [lift_act_inverse]; |
|
617 |
||
618 |
||
619 |
Goal "(lift_prog i F) Join G = lift_prog i H \ |
|
620 |
\ ==> EX J. H = F Join J"; |
|
621 |
by (etac program_equalityE 1); |
|
622 |
by (auto_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join])); |
|
623 |
by (res_inst_tac [("x", |
|
624 |
"mk_program(Applyall(Init G) i, drop_act i `` Acts G)")] |
|
625 |
exI 1); |
|
626 |
by (rtac program_equalityI 1); |
|
627 |
(*Init*) |
|
628 |
by (simp_tac (simpset() addsimps [Applyall_def]) 1); |
|
629 |
(*Blast_tac can't do HO unification, needed to invent function states*) |
|
630 |
by (fast_tac (claset() addEs [equalityE]) 1); |
|
631 |
(*Now for the Actions*) |
|
632 |
by (dres_inst_tac [("f", "op `` (drop_act i)")] arg_cong 1); |
|
633 |
by (asm_full_simp_tac |
|
634 |
(simpset() addsimps [insert_absorb, Acts_Join, |
|
635 |
image_Un, image_compose RS sym, o_def]) 1); |
|
636 |
qed "lift_prog_Join_eq_lift_prog_D"; |
|
637 |
||
638 |
||
639 |
Goal "F : X guarantees Y \ |
|
640 |
\ ==> lift_prog i F : (lift_prog i `` X) guarantees (lift_prog i `` Y)"; |
|
641 |
by (rtac guaranteesI 1); |
|
642 |
by Auto_tac; |
|
643 |
by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); |
|
644 |
qed "lift_prog_guarantees"; |
|
645 |
||
646 |