181 by (asm_simp_tac (simpset() addsimps [leadsTo_UN, Times_Union2]) 3); |
184 by (asm_simp_tac (simpset() addsimps [leadsTo_UN, Times_Union2]) 3); |
182 by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
185 by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
183 by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, Lcopy_ensures]) 1); |
186 by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, Lcopy_ensures]) 1); |
184 qed "leadsTo_imp_Lcopy_leadsTo"; |
187 qed "leadsTo_imp_Lcopy_leadsTo"; |
185 |
188 |
186 Goal "Lcopy F : ensures A B ==> F : ensures (Domain A) (Domain B)"; |
189 (** |
187 by (full_simp_tac |
190 Goal "Lcopy F : ensures A B ==> F : ensures (Domain A) (Domain B)"; |
188 (simpset() addsimps [ensures_def, Lcopy_constrains, Lcopy_transient, |
191 by (full_simp_tac |
189 Domain_Un_eq RS sym, |
192 (simpset() addsimps [ensures_def, Lcopy_constrains, Lcopy_transient, |
190 Sigma_Un_distrib1 RS sym, |
193 Domain_Un_eq RS sym, |
191 Sigma_Diff_distrib1 RS sym]) 1); |
194 Sigma_Un_distrib1 RS sym, |
192 by (safe_tac (claset() addSDs [Lcopy_constrains_Domain])); |
195 Sigma_Diff_distrib1 RS sym]) 1); |
193 by (etac constrains_weaken_L 1); |
196 by (safe_tac (claset() addSDs [Lcopy_constrains_Domain])); |
194 by (Blast_tac 1); |
197 by (etac constrains_weaken_L 1); |
195 (*NOT able to prove this: |
198 by (Blast_tac 1); |
196 Lcopy F : ensures A B ==> F : ensures (Domain A) (Domain B) |
199 (*NOT able to prove this: |
197 1. [| Lcopy F : transient (A - B); |
200 Lcopy F : ensures A B ==> F : ensures (Domain A) (Domain B) |
198 F : constrains (Domain (A - B)) (Domain (A Un B)) |] |
201 1. [| Lcopy F : transient (A - B); |
199 ==> F : transient (Domain A - Domain B) |
202 F : constrains (Domain (A - B)) (Domain (A Un B)) |] |
|
203 ==> F : transient (Domain A - Domain B) |
|
204 **) |
|
205 |
|
206 |
|
207 Goal "Lcopy F : leadsTo AU BU ==> F : leadsTo (Domain AU) (Domain BU)"; |
|
208 by (etac leadsTo_induct 1); |
|
209 by (full_simp_tac (simpset() addsimps [Domain_Union]) 3); |
|
210 by (blast_tac (claset() addIs [leadsTo_UN]) 3); |
|
211 by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
212 by (rtac leadsTo_Basis 1); |
|
213 (*...and so CANNOT PROVE THIS*) |
|
214 |
|
215 |
|
216 (*This also seems impossible to prove??*) |
|
217 Goal "(Lcopy F : leadsTo (A Times UNIV) (B Times UNIV)) = \ |
|
218 \ (F : leadsTo A B)"; |
200 **) |
219 **) |
201 |
220 |
202 |
221 |
203 Goal "Lcopy F : leadsTo AU BU ==> F : leadsTo (Domain AU) (Domain BU)"; |
|
204 by (etac leadsTo_induct 1); |
|
205 by (full_simp_tac (simpset() addsimps [Domain_Union]) 3); |
|
206 by (blast_tac (claset() addIs [leadsTo_UN]) 3); |
|
207 by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
208 by (rtac leadsTo_Basis 1); |
|
209 (*...and so CANNOT PROVE THIS*) |
|
210 |
|
211 |
|
212 (*This also seems impossible to prove??*) |
|
213 Goal "(Lcopy F : leadsTo (A Times UNIV) (B Times UNIV)) = \ |
|
214 \ (F : leadsTo A B)"; |
|
215 |
|
216 |
|
217 |
|
218 (**** PPROD ****) |
222 (**** PPROD ****) |
219 |
223 |
220 (*** Basic properties ***) |
224 (*** Basic properties ***) |
221 |
|
222 Goalw [PPROD_def, lift_prog_def] |
|
223 "Init (PPROD I F) = {f. ALL i:I. f i : Init F}"; |
|
224 by Auto_tac; |
|
225 qed "Init_PPROD"; |
|
226 |
225 |
227 Goalw [lift_act_def] "lift_act i Id = Id"; |
226 Goalw [lift_act_def] "lift_act i Id = Id"; |
228 by Auto_tac; |
227 by Auto_tac; |
229 qed "lift_act_Id"; |
228 qed "lift_act_Id"; |
230 Addsimps [lift_act_Id]; |
229 Addsimps [lift_act_Id]; |
|
230 |
|
231 Goalw [lift_prog_def] "Init (lift_prog i F) = {f. f i : Init F}"; |
|
232 by Auto_tac; |
|
233 qed "Init_lift_prog"; |
|
234 Addsimps [Init_lift_prog]; |
|
235 |
|
236 Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; |
|
237 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset())); |
|
238 qed "Acts_lift_prog"; |
|
239 |
|
240 Goalw [PPROD_def] "Init (PPROD I F) = {f. ALL i:I. f i : Init (F i)}"; |
|
241 by Auto_tac; |
|
242 qed "Init_PPROD"; |
|
243 Addsimps [Init_PPROD]; |
231 |
244 |
232 Goalw [lift_act_def] |
245 Goalw [lift_act_def] |
233 "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
246 "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
234 by (Blast_tac 1); |
247 by (Blast_tac 1); |
235 qed "lift_act_eq"; |
248 qed "lift_act_eq"; |
236 AddIffs [lift_act_eq]; |
249 AddIffs [lift_act_eq]; |
237 |
250 |
238 Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts F)"; |
251 Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; |
239 by (auto_tac (claset(), |
252 by (auto_tac (claset(), |
240 simpset() addsimps [PPROD_def, lift_prog_def, Acts_JN])); |
253 simpset() addsimps [PPROD_def, Acts_lift_prog, Acts_JN])); |
241 qed "Acts_PPROD"; |
254 qed "Acts_PPROD"; |
242 |
255 |
243 Addsimps [Init_PPROD]; |
256 Goal "(PPI i: I. SKIP) = SKIP"; |
244 |
257 by (auto_tac (claset() addSIs [program_equalityI], |
245 Goal "PPROD I SKIP = SKIP"; |
258 simpset() addsimps [PPROD_def, Acts_lift_prog, |
246 by (rtac program_equalityI 1); |
|
247 by (auto_tac (claset(), |
|
248 simpset() addsimps [PPROD_def, lift_prog_def, |
|
249 SKIP_def, Acts_JN])); |
259 SKIP_def, Acts_JN])); |
250 qed "PPROD_SKIP"; |
260 qed "PPROD_SKIP"; |
251 |
261 |
252 Goal "PPROD {} F = SKIP"; |
262 Goal "PPROD {} F = SKIP"; |
253 by (simp_tac (simpset() addsimps [PPROD_def]) 1); |
263 by (simp_tac (simpset() addsimps [PPROD_def]) 1); |
254 qed "PPROD_empty"; |
264 qed "PPROD_empty"; |
255 |
265 |
256 Addsimps [PPROD_SKIP, PPROD_empty]; |
266 Addsimps [PPROD_SKIP, PPROD_empty]; |
257 |
267 |
258 Goalw [PPROD_def] "PPROD (insert i I) F = (lift_prog i F) Join (PPROD I F)"; |
268 Goalw [PPROD_def] |
|
269 "PPROD (insert i I) F = (lift_prog i (F i)) Join (PPROD I F)"; |
259 by Auto_tac; |
270 by Auto_tac; |
260 qed "PPROD_insert"; |
271 qed "PPROD_insert"; |
261 |
272 |
262 |
273 Goalw [PPROD_def] "i : I ==> component (lift_prog i (F i)) (PPROD I F)"; |
263 (*** Safety: constrains, stable ***) |
274 (*blast_tac doesn't use HO unification*) |
264 |
275 by (fast_tac (claset() addIs [component_JN]) 1); |
265 val subsetCE' = rinst |
276 qed "component_PPROD"; |
266 [("c", "(%u. ?s)(i:=?s')")] subsetCE; |
277 |
|
278 |
|
279 (*** Safety: constrains, stable, invariant ***) |
|
280 |
|
281 (** 1st formulation of lifting **) |
|
282 |
|
283 Goal "(lift_prog i F : constrains {f. f i : A} {f. f i : B}) = \ |
|
284 \ (F : constrains A B)"; |
|
285 by (auto_tac (claset(), |
|
286 simpset() addsimps [constrains_def, Acts_lift_prog])); |
|
287 by (Blast_tac 2); |
|
288 by (Force_tac 1); |
|
289 qed "lift_prog_constrains_eq"; |
|
290 |
|
291 Goal "(lift_prog i F : stable {f. f i : A}) = (F : stable A)"; |
|
292 by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1); |
|
293 qed "lift_prog_stable_eq"; |
|
294 |
|
295 (*This one looks strange! Proof probably is by case analysis on i=j.*) |
|
296 Goal "F i : constrains A B \ |
|
297 \ ==> lift_prog j (F j) : constrains {f. f i : A} {f. f i : B}"; |
|
298 by (auto_tac (claset(), |
|
299 simpset() addsimps [constrains_def, Acts_lift_prog])); |
|
300 by (REPEAT (Blast_tac 1)); |
|
301 qed "constrains_imp_lift_prog_constrains"; |
267 |
302 |
268 Goal "i : I ==> \ |
303 Goal "i : I ==> \ |
269 \ (PPROD I F : constrains {f. f i : A} {f. f i : B}) = \ |
304 \ (PPROD I F : constrains {f. f i : A} {f. f i : B}) = \ |
270 \ (F : constrains A B)"; |
305 \ (F i : constrains A B)"; |
271 by (auto_tac (claset(), |
306 by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
272 simpset() addsimps [constrains_def, lift_prog_def, PPROD_def, |
307 by (blast_tac (claset() addIs [lift_prog_constrains_eq RS iffD1, |
273 Acts_JN])); |
308 constrains_imp_lift_prog_constrains]) 1); |
274 by (REPEAT (Blast_tac 2)); |
|
275 by (force_tac (claset() addSEs [subsetCE', allE, ballE], simpset()) 1); |
|
276 qed "PPROD_constrains"; |
309 qed "PPROD_constrains"; |
277 |
310 |
278 Goal "[| PPROD I F : constrains AA BB; i: I |] \ |
311 Goal "i : I ==> (PPROD I F : stable {f. f i : A}) = (F i : stable A)"; |
|
312 by (asm_simp_tac (simpset() addsimps [stable_def, PPROD_constrains]) 1); |
|
313 qed "PPROD_stable"; |
|
314 |
|
315 |
|
316 (** 2nd formulation of lifting **) |
|
317 |
|
318 Goal "[| lift_prog i F : constrains AA BB |] \ |
279 \ ==> F : constrains (Applyall AA i) (Applyall BB i)"; |
319 \ ==> F : constrains (Applyall AA i) (Applyall BB i)"; |
280 by (auto_tac (claset(), |
320 by (auto_tac (claset(), |
281 simpset() addsimps [Applyall_def, constrains_def, |
321 simpset() addsimps [Applyall_def, constrains_def, |
282 lift_prog_def, PPROD_def, Acts_JN])); |
322 Acts_lift_prog])); |
283 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI] |
323 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
284 addSEs [rinst [("c", "?ff(i := ?u)")] subsetCE, ballE], |
|
285 simpset()) 1); |
324 simpset()) 1); |
|
325 qed "lift_prog_constrains_projection"; |
|
326 |
|
327 Goal "[| PPROD I F : constrains AA BB; i: I |] \ |
|
328 \ ==> F i : constrains (Applyall AA i) (Applyall BB i)"; |
|
329 by (rtac lift_prog_constrains_projection 1); |
|
330 (*rotate this assumption to be last*) |
|
331 by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1); |
|
332 by (asm_full_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
286 qed "PPROD_constrains_projection"; |
333 qed "PPROD_constrains_projection"; |
287 |
334 |
288 |
335 |
289 Goal "i : I ==> (PPROD I F : stable {f. f i : A}) = (F : stable A)"; |
336 (** invariant **) |
290 by (asm_simp_tac (simpset() addsimps [stable_def, PPROD_constrains]) 1); |
337 |
291 qed "PPROD_stable"; |
338 Goal "F : invariant A ==> lift_prog i F : invariant {f. f i : A}"; |
292 |
339 by (auto_tac (claset(), |
293 Goal "i : I ==> (PPROD I F : invariant {f. f i : A}) = (F : invariant A)"; |
340 simpset() addsimps [invariant_def, lift_prog_stable_eq])); |
|
341 qed "invariant_imp_lift_prog_invariant"; |
|
342 |
|
343 Goal "[| lift_prog i F : invariant {f. f i : A} |] ==> F : invariant A"; |
|
344 by (auto_tac (claset(), |
|
345 simpset() addsimps [invariant_def, lift_prog_stable_eq])); |
|
346 qed "lift_prog_invariant_imp_invariant"; |
|
347 |
|
348 (*NOT clear that the previous lemmas help in proving this one.*) |
|
349 Goal "[| F i : invariant A; i : I |] ==> PPROD I F : invariant {f. f i : A}"; |
294 by (auto_tac (claset(), |
350 by (auto_tac (claset(), |
295 simpset() addsimps [invariant_def, PPROD_stable])); |
351 simpset() addsimps [invariant_def, PPROD_stable])); |
|
352 qed "invariant_imp_PPROD_invariant"; |
|
353 |
|
354 (*The f0 premise ensures that the product is well-defined.*) |
|
355 Goal "[| PPROD I F : invariant {f. f i : A}; i : I; \ |
|
356 \ f0: Init (PPROD I F) |] ==> F i : invariant A"; |
|
357 by (auto_tac (claset(), |
|
358 simpset() addsimps [invariant_def, PPROD_stable])); |
|
359 by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1); |
|
360 by Auto_tac; |
|
361 qed "PPROD_invariant_imp_invariant"; |
|
362 |
|
363 Goal "[| i : I; f0: Init (PPROD I F) |] \ |
|
364 \ ==> (PPROD I F : invariant {f. f i : A}) = (F i : invariant A)"; |
|
365 by (blast_tac (claset() addIs [invariant_imp_PPROD_invariant, |
|
366 PPROD_invariant_imp_invariant]) 1); |
296 qed "PPROD_invariant"; |
367 qed "PPROD_invariant"; |
297 |
368 |
298 |
369 (*The f0 premise isn't needed if F is a constant program because then |
299 (** Substitution Axiom versions: Constrains, Stable **) |
370 we get an initial state by replicating that of F*) |
300 |
371 Goal "i : I \ |
301 Goal "[| f : reachable (PPROD I F); i : I |] ==> f i : reachable F"; |
372 \ ==> ((PPI x:I. F) : invariant {f. f i : A}) = (F : invariant A)"; |
|
373 by (auto_tac (claset(), |
|
374 simpset() addsimps [invariant_def, PPROD_stable])); |
|
375 qed "PFUN_invariant"; |
|
376 |
|
377 |
|
378 (*** Substitution Axiom versions: Constrains, Stable ***) |
|
379 |
|
380 (** Reachability **) |
|
381 |
|
382 Goal "[| f : reachable (PPROD I F); i : I |] ==> f i : reachable (F i)"; |
302 by (etac reachable.induct 1); |
383 by (etac reachable.induct 1); |
303 by (auto_tac |
384 by (auto_tac |
304 (claset() addIs reachable.intrs, |
385 (claset() addIs reachable.intrs, |
305 simpset() addsimps [Acts_PPROD])); |
386 simpset() addsimps [Acts_PPROD])); |
306 qed "reachable_PPROD"; |
387 qed "reachable_PPROD"; |
307 |
388 |
308 Goal "reachable (PPROD I F) <= {f. ALL i:I. f i : reachable F}"; |
389 Goal "reachable (PPROD I F) <= {f. ALL i:I. f i : reachable (F i)}"; |
309 by (force_tac (claset() addSDs [reachable_PPROD], simpset()) 1); |
390 by (force_tac (claset() addSDs [reachable_PPROD], simpset()) 1); |
310 qed "reachable_PPROD_subset1"; |
391 qed "reachable_PPROD_subset1"; |
311 |
392 |
312 Goal "[| i ~: I; A : reachable F |] \ |
393 Goal "[| i ~: I; A : reachable (F i) |] \ |
313 \ ==> ALL f. f : reachable (PPROD I F) \ |
394 \ ==> ALL f. f : reachable (PPROD I F) \ |
314 \ --> f(i:=A) : reachable (lift_prog i F Join PPROD I F)"; |
395 \ --> f(i:=A) : reachable (lift_prog i (F i) Join PPROD I F)"; |
315 by (etac reachable.induct 1); |
396 by (etac reachable.induct 1); |
316 by (ALLGOALS Clarify_tac); |
397 by (ALLGOALS Clarify_tac); |
317 by (etac reachable.induct 1); |
398 by (etac reachable.induct 1); |
318 (*Init, Init case*) |
399 (*Init, Init case*) |
319 by (force_tac (claset() addIs reachable.intrs, |
400 by (force_tac (claset() addIs reachable.intrs, |
320 simpset() addsimps [lift_prog_def]) 1); |
401 simpset() addsimps [Acts_lift_prog]) 1); |
321 (*Init of F, action of PPROD F case*) |
402 (*Init of F, action of PPROD F case*) |
322 br reachable.Acts 1; |
403 by (rtac reachable.Acts 1); |
323 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
404 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
324 ba 1; |
405 by (assume_tac 1); |
325 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
406 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
326 (*induction over the 2nd "reachable" assumption*) |
407 (*induction over the 2nd "reachable" assumption*) |
327 by (eres_inst_tac [("xa","f")] reachable.induct 1); |
408 by (eres_inst_tac [("xa","f")] reachable.induct 1); |
328 (*Init of PPROD F, action of F case*) |
409 (*Init of PPROD F, action of F case*) |
329 by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
410 by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
330 by (force_tac (claset(), simpset() addsimps [lift_prog_def, Acts_Join]) 1); |
411 by (force_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join]) 1); |
331 by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
412 by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
332 by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
413 by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
333 (*last case: an action of PPROD I F*) |
414 (*last case: an action of PPROD I F*) |
334 br reachable.Acts 1; |
415 by (rtac reachable.Acts 1); |
335 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
416 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
336 ba 1; |
417 by (assume_tac 1); |
337 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
418 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
338 qed_spec_mp "reachable_lift_Join_PPROD"; |
419 qed_spec_mp "reachable_lift_Join_PPROD"; |
339 |
420 |
340 |
421 |
341 (*The index set must be finite: otherwise infinitely many copies of F can |
422 (*The index set must be finite: otherwise infinitely many copies of F can |
342 perform actions, and PPROD can never catch up in finite time.*) |
423 perform actions, and PPROD can never catch up in finite time.*) |
343 Goal "finite I ==> {f. ALL i:I. f i : reachable F} <= reachable (PPROD I F)"; |
424 Goal "finite I \ |
|
425 \ ==> {f. ALL i:I. f i : reachable (F i)} <= reachable (PPROD I F)"; |
344 by (etac finite_induct 1); |
426 by (etac finite_induct 1); |
345 by (Simp_tac 1); |
427 by (Simp_tac 1); |
346 by (force_tac (claset() addDs [reachable_lift_Join_PPROD], |
428 by (force_tac (claset() addDs [reachable_lift_Join_PPROD], |
347 simpset() addsimps [PPROD_insert]) 1); |
429 simpset() addsimps [PPROD_insert]) 1); |
348 qed "reachable_PPROD_subset2"; |
430 qed "reachable_PPROD_subset2"; |
349 |
431 |
350 Goal "finite I ==> reachable (PPROD I F) = {f. ALL i:I. f i : reachable F}"; |
432 Goal "finite I ==> \ |
|
433 \ reachable (PPROD I F) = {f. ALL i:I. f i : reachable (F i)}"; |
351 by (REPEAT_FIRST (ares_tac [equalityI, |
434 by (REPEAT_FIRST (ares_tac [equalityI, |
352 reachable_PPROD_subset1, |
435 reachable_PPROD_subset1, |
353 reachable_PPROD_subset2])); |
436 reachable_PPROD_subset2])); |
354 qed "reachable_PPROD_eq"; |
437 qed "reachable_PPROD_eq"; |
355 |
438 |
356 |
439 |
357 Goal "i: I ==> Applyall {f. (ALL i:I. f i : R) & f i : A} i = R Int A"; |
440 (** Constrains **) |
358 by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1); |
441 |
359 qed "Applyall_Int"; |
442 Goal "[| F i : Constrains A B; i: I; finite I |] \ |
360 |
443 \ ==> PPROD I F : Constrains {f. f i : A} {f. f i : B}"; |
361 |
|
362 Goal "[| i: I; finite I |] \ |
|
363 \ ==> (PPROD I F : Constrains {f. f i : A} {f. f i : B}) = \ |
|
364 \ (F : Constrains A B)"; |
|
365 by (auto_tac |
444 by (auto_tac |
366 (claset(), |
445 (claset(), |
367 simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
446 simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
368 reachable_PPROD_eq])); |
447 reachable_PPROD_eq])); |
369 bd PPROD_constrains_projection 1; |
|
370 ba 1; |
|
371 by (asm_full_simp_tac (simpset() addsimps [Applyall_Int]) 1); |
|
372 by (auto_tac (claset(), |
448 by (auto_tac (claset(), |
373 simpset() addsimps [constrains_def, lift_prog_def, PPROD_def, |
449 simpset() addsimps [constrains_def, Acts_lift_prog, PPROD_def, |
374 Acts_JN])); |
450 Acts_JN])); |
375 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
451 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
|
452 qed "Constrains_imp_PPROD_Constrains"; |
|
453 |
|
454 Goal "[| ALL i:I. f0 i : R i; i: I |] \ |
|
455 \ ==> Applyall {f. (ALL i:I. f i : R i) & f i : A} i = R i Int A"; |
|
456 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI], |
|
457 simpset() addsimps [Applyall_def]) 1); |
|
458 qed "Applyall_Int_depend"; |
|
459 |
|
460 (*Again, we need the f0 premise because otherwise Constrains holds trivially |
|
461 for PPROD I F.*) |
|
462 Goal "[| PPROD I F : Constrains {f. f i : A} {f. f i : B}; \ |
|
463 \ i: I; finite I; f0: Init (PPROD I F) |] \ |
|
464 \ ==> F i : Constrains A B"; |
|
465 by (full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
|
466 by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1); |
|
467 by (blast_tac (claset() addIs [reachable.Init]) 2); |
|
468 by (dtac PPROD_constrains_projection 1); |
|
469 by (assume_tac 1); |
|
470 by (asm_full_simp_tac |
|
471 (simpset() addsimps [Applyall_Int_depend, Collect_conj_eq RS sym, |
|
472 reachable_PPROD_eq]) 1); |
|
473 qed "PPROD_Constrains_imp_Constrains"; |
|
474 |
|
475 |
|
476 Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \ |
|
477 \ ==> (PPROD I F : Constrains {f. f i : A} {f. f i : B}) = \ |
|
478 \ (F i : Constrains A B)"; |
|
479 by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, |
|
480 PPROD_Constrains_imp_Constrains]) 1); |
376 qed "PPROD_Constrains"; |
481 qed "PPROD_Constrains"; |
377 |
482 |
|
483 Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \ |
|
484 \ ==> (PPROD I F : Stable {f. f i : A}) = (F i : Stable A)"; |
|
485 by (asm_simp_tac (simpset() delsimps [Init_PPROD] |
|
486 addsimps [Stable_def, PPROD_Constrains]) 1); |
|
487 qed "PPROD_Stable"; |
|
488 |
|
489 |
|
490 (** PFUN (no dependence on i) doesn't require the f0 premise **) |
|
491 |
|
492 Goal "i: I ==> Applyall {f. (ALL i:I. f i : R) & f i : A} i = R Int A"; |
|
493 by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1); |
|
494 qed "Applyall_Int"; |
|
495 |
|
496 Goal "[| (PPI x:I. F) : Constrains {f. f i : A} {f. f i : B}; \ |
|
497 \ i: I; finite I |] \ |
|
498 \ ==> F : Constrains A B"; |
|
499 by (full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
|
500 by (dtac PPROD_constrains_projection 1); |
|
501 by (assume_tac 1); |
|
502 by (asm_full_simp_tac |
|
503 (simpset() addsimps [Applyall_Int, Collect_conj_eq RS sym, |
|
504 reachable_PPROD_eq]) 1); |
|
505 qed "PFUN_Constrains_imp_Constrains"; |
378 |
506 |
379 Goal "[| i: I; finite I |] \ |
507 Goal "[| i: I; finite I |] \ |
380 \ ==> (PPROD I F : Stable {f. f i : A}) = (F : Stable A)"; |
508 \ ==> ((PPI x:I. F) : Constrains {f. f i : A} {f. f i : B}) = \ |
381 by (asm_simp_tac (simpset() addsimps [Stable_def, PPROD_Constrains]) 1); |
509 \ (F : Constrains A B)"; |
382 qed "PPROD_Stable"; |
510 by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, |
383 |
511 PFUN_Constrains_imp_Constrains]) 1); |
384 |
512 qed "PFUN_Constrains"; |
385 |
513 |
|
514 Goal "[| i: I; finite I |] \ |
|
515 \ ==> ((PPI x:I. F) : Stable {f. f i : A}) = (F : Stable A)"; |
|
516 by (asm_simp_tac (simpset() addsimps [Stable_def, PFUN_Constrains]) 1); |
|
517 qed "PFUN_Stable"; |
|
518 |
|
519 |
|
520 |
|
521 (*** guarantees properties ***) |
|
522 |
|
523 (*We only need act2=Id but the condition used is very weak*) |
|
524 Goal "(x,y): act2 ==> fst_act (act1 RTimes act2) = act1"; |
|
525 by (auto_tac (claset(), simpset() addsimps [fst_act_def, RTimes_def])); |
|
526 qed "fst_act_RTimes"; |
|
527 Addsimps [fst_act_RTimes]; |
|
528 |
|
529 |
|
530 Goal "(Lcopy F) Join G = Lcopy H ==> EX J. H = F Join J"; |
|
531 by (etac program_equalityE 1); |
|
532 by (auto_tac (claset(), simpset() addsimps [Acts_Join])); |
|
533 by (res_inst_tac |
|
534 [("x", "mk_program(Domain (Init G), fst_act `` Acts G)")] exI 1); |
|
535 by (rtac program_equalityI 1); |
|
536 (*Init*) |
|
537 by (simp_tac (simpset() addsimps [Acts_Join]) 1); |
|
538 by (blast_tac (claset() addEs [equalityE]) 1); |
|
539 (*Now for the Actions*) |
|
540 by (dres_inst_tac [("f", "op `` fst_act")] arg_cong 1); |
|
541 by (asm_full_simp_tac |
|
542 (simpset() addsimps [insert_absorb, Acts_Lcopy, Acts_Join, |
|
543 image_Un, image_compose RS sym, o_def]) 1); |
|
544 qed "Lcopy_Join_eq_Lcopy_D"; |
|
545 |
|
546 |
|
547 Goal "F : X guarantees Y \ |
|
548 \ ==> Lcopy F : (Lcopy `` X) guarantees (Lcopy `` Y)"; |
|
549 by (rtac guaranteesI 1); |
|
550 by Auto_tac; |
|
551 by (blast_tac (claset() addDs [Lcopy_Join_eq_Lcopy_D, guaranteesD]) 1); |
|
552 qed "Lcopy_guarantees"; |
|
553 |
|
554 |
|
555 Goal "drop_act i (lift_act i act) = act"; |
|
556 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI], |
|
557 simpset() addsimps [drop_act_def, lift_act_def]) 1); |
|
558 qed "lift_act_inverse"; |
|
559 Addsimps [lift_act_inverse]; |
|
560 |
|
561 |
|
562 Goal "(lift_prog i F) Join G = lift_prog i H \ |
|
563 \ ==> EX J. H = F Join J"; |
|
564 by (etac program_equalityE 1); |
|
565 by (auto_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join])); |
|
566 by (res_inst_tac [("x", |
|
567 "mk_program(Applyall(Init G) i, drop_act i `` Acts G)")] |
|
568 exI 1); |
|
569 by (rtac program_equalityI 1); |
|
570 (*Init*) |
|
571 by (simp_tac (simpset() addsimps [Applyall_def]) 1); |
|
572 (*Blast_tac can't do HO unification, needed to invent function states*) |
|
573 by (fast_tac (claset() addEs [equalityE]) 1); |
|
574 (*Now for the Actions*) |
|
575 by (dres_inst_tac [("f", "op `` (drop_act i)")] arg_cong 1); |
|
576 by (asm_full_simp_tac |
|
577 (simpset() addsimps [insert_absorb, Acts_Join, |
|
578 image_Un, image_compose RS sym, o_def]) 1); |
|
579 qed "lift_prog_Join_eq_lift_prog_D"; |
|
580 |
|
581 |
|
582 Goal "F : X guarantees Y \ |
|
583 \ ==> lift_prog i F : (lift_prog i `` X) guarantees (lift_prog i `` Y)"; |
|
584 by (rtac guaranteesI 1); |
|
585 by Auto_tac; |
|
586 by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); |
|
587 qed "lift_prog_guarantees"; |
|
588 |
|
589 |