62 by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1); |
62 by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1); |
63 qed "PLam_transient"; |
63 qed "PLam_transient"; |
64 |
64 |
65 Addsimps [PLam_constrains, PLam_stable, PLam_transient]; |
65 Addsimps [PLam_constrains, PLam_stable, PLam_transient]; |
66 |
66 |
|
67 Goal "[| i : I; F i : A ensures B |] ==> \ |
|
68 \ PLam I F : (lift_set i A) ensures lift_set i B"; |
|
69 by (auto_tac (claset(), |
|
70 simpset() addsimps [ensures_def, lift_prog_transient_eq_disj])); |
|
71 qed "PLam_ensures"; |
|
72 |
67 Goal "[| i : I; F i : (A-B) co (A Un B); F i : transient (A-B) |] ==> \ |
73 Goal "[| i : I; F i : (A-B) co (A Un B); F i : transient (A-B) |] ==> \ |
68 \ PLam I F : (lift_set i A) leadsTo lift_set i B"; |
74 \ PLam I F : (lift_set i A) leadsTo lift_set i B"; |
69 by (rtac (ensuresI RS leadsTo_Basis) 1); |
75 by (rtac (PLam_ensures RS leadsTo_Basis) 1); |
70 by (auto_tac (claset(), simpset() addsimps [lift_prog_transient_eq_disj])); |
76 by (rtac ensuresI 2); |
|
77 by (ALLGOALS assume_tac); |
71 qed "PLam_leadsTo_Basis"; |
78 qed "PLam_leadsTo_Basis"; |
72 |
79 |
73 Goal "[| PLam I F : AA co BB; i: I |] \ |
80 Goal "[| PLam I F : AA co BB; i: I |] \ |
74 \ ==> F i : (drop_set i AA) co (drop_set i BB)"; |
81 \ ==> F i : (drop_set i AA) co (drop_set i BB)"; |
75 by (rtac lift_prog_constrains_drop_set 1); |
82 by (rtac lift_prog_constrains_drop_set 1); |