28 by Auto_tac; |
28 by Auto_tac; |
29 qed "Diff_lift_set"; |
29 qed "Diff_lift_set"; |
30 |
30 |
31 Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set]; |
31 Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set]; |
32 |
32 |
33 (*Converse fails*) |
|
34 Goalw [drop_set_def] "f : A ==> f i : drop_set i A"; |
|
35 by Auto_tac; |
|
36 qed "drop_set_I"; |
|
37 |
|
38 (** lift_act and drop_act **) |
33 (** lift_act and drop_act **) |
39 |
|
40 Goalw [lift_act_def] "lift_act i Id = Id"; |
|
41 by Auto_tac; |
|
42 by (etac rev_mp 1); |
|
43 by (dtac sym 1); |
|
44 by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1); |
|
45 qed "lift_act_Id"; |
|
46 Addsimps [lift_act_Id]; |
|
47 |
34 |
48 (*For compatibility with the original definition and perhaps simpler proofs*) |
35 (*For compatibility with the original definition and perhaps simpler proofs*) |
49 Goalw [lift_act_def] |
36 Goalw [lift_act_def] |
50 "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
37 "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
51 by Auto_tac; |
38 by Auto_tac; |
52 by (rtac exI 1); |
39 by (rtac exI 1); |
53 by Auto_tac; |
40 by Auto_tac; |
54 qed "lift_act_eq"; |
41 qed "lift_act_eq"; |
55 AddIffs [lift_act_eq]; |
42 AddIffs [lift_act_eq]; |
56 |
|
57 Goalw [drop_set_def, drop_act_def] |
|
58 "UNIV <= drop_set i C ==> drop_act i (Restrict C Id) = Id"; |
|
59 by (Blast_tac 1); |
|
60 qed "drop_act_Id"; |
|
61 Addsimps [drop_act_Id]; |
|
62 |
43 |
63 (** lift_prog and drop_prog **) |
44 (** lift_prog and drop_prog **) |
64 |
45 |
65 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)"; |
46 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)"; |
66 by Auto_tac; |
47 by Auto_tac; |
336 lift_export reachable_extend_eq]) 1); |
320 lift_export reachable_extend_eq]) 1); |
337 qed "reachable_lift_prog"; |
321 qed "reachable_lift_prog"; |
338 |
322 |
339 Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \ |
323 Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \ |
340 \ (F : A Co B)"; |
324 \ (F : A Co B)"; |
341 by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog, |
325 by (simp_tac |
342 lift_prog_constrains]) 1); |
326 (simpset() addsimps [lift_prog_correct, lift_set_correct, |
|
327 lift_export extend_Constrains]) 1); |
343 qed "lift_prog_Constrains"; |
328 qed "lift_prog_Constrains"; |
344 |
329 |
345 Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)"; |
330 Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)"; |
346 by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1); |
331 by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1); |
347 qed "lift_prog_Stable"; |
332 qed "lift_prog_Stable"; |
451 \ guarantees increasing (func o sub i)"; |
436 \ guarantees increasing (func o sub i)"; |
452 by (dtac (lift_export extend_localTo_guar_increasing) 1); |
437 by (dtac (lift_export extend_localTo_guar_increasing) 1); |
453 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1); |
438 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1); |
454 qed "lift_prog_localTo_guar_increasing"; |
439 qed "lift_prog_localTo_guar_increasing"; |
455 |
440 |
456 (*** |
441 Goal "[| F : (v LocalTo H) guarantees Increasing func; H <= F |] \ |
457 Goal "F : (v LocalTo G) guarantees Increasing func \ |
442 \ ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i H) \ |
458 \ ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G) \ |
|
459 \ guarantees Increasing (func o sub i)"; |
443 \ guarantees Increasing (func o sub i)"; |
460 by (dtac (lift_export extend_LocalTo_guar_Increasing) 1); |
444 by (dtac (lift_export extend_LocalTo_guar_Increasing) 1); |
461 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1); |
445 by (auto_tac (claset(), |
|
446 simpset() addsimps [lift_prog_correct, o_def])); |
462 qed "lift_prog_LocalTo_guar_Increasing"; |
447 qed "lift_prog_LocalTo_guar_Increasing"; |
463 ***) |
|
464 |
448 |
465 Goal "F : Always A guarantees Always B \ |
449 Goal "F : Always A guarantees Always B \ |
466 \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)"; |
450 \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)"; |
467 by (asm_simp_tac |
451 by (asm_simp_tac |
468 (simpset() addsimps [lift_set_correct, lift_prog_correct, |
452 (simpset() addsimps [lift_set_correct, lift_prog_correct, |