181 |
181 |
182 Goal "[| F : A leadsTo[CC'] A'; B<=A; A'<=B'; CC' <= CC |] \ |
182 Goal "[| F : A leadsTo[CC'] A'; B<=A; A'<=B'; CC' <= CC |] \ |
183 \ ==> F : B leadsTo[CC] B'"; |
183 \ ==> F : B leadsTo[CC] B'"; |
184 by (dtac (impOfSubs leadsETo_mono) 1); |
184 by (dtac (impOfSubs leadsETo_mono) 1); |
185 by (assume_tac 1); |
185 by (assume_tac 1); |
186 by (blast_tac (claset() addIs [leadsETo_weaken_R, leadsETo_weaken_L, |
186 by (blast_tac (claset() delrules [subsetCE] |
|
187 addIs [leadsETo_weaken_R, leadsETo_weaken_L, |
187 leadsETo_Trans]) 1); |
188 leadsETo_Trans]) 1); |
188 qed "leadsETo_weaken"; |
189 qed "leadsETo_weaken"; |
189 |
190 |
190 Goal "[| F : A leadsTo[CC] A'; CC <= givenBy v |] \ |
191 Goal "[| F : A leadsTo[CC] A'; CC <= givenBy v |] \ |
191 \ ==> F : A leadsTo[givenBy v] A'"; |
192 \ ==> F : A leadsTo[givenBy v] A'"; |
532 (*If addIs then PROOF FAILED at depth 2*) |
533 (*If addIs then PROOF FAILED at depth 2*) |
533 by (blast_tac (claset() addSIs [preserves_givenBy_imp_stable, |
534 by (blast_tac (claset() addSIs [preserves_givenBy_imp_stable, |
534 project_preserves_I]) 1); |
535 project_preserves_I]) 1); |
535 result(); |
536 result(); |
536 |
537 |
537 (*Generalizes the version proved in Project.ML*) |
538 (*GENERALIZES the version proved in Project.ML*) |
538 Goal "[| G : preserves (v o f); \ |
539 Goal "[| G : preserves (v o f); \ |
539 \ project h C G : transient (C' Int D); \ |
540 \ project h C G : transient (C' Int D); \ |
540 \ project h C G : stable C'; D : givenBy v |] \ |
541 \ project h C G : stable C'; D : givenBy v |] \ |
541 \ ==> C' Int D = {}"; |
542 \ ==> C' Int D = {}"; |
542 by (rtac stable_transient_empty 1); |
543 by (rtac stable_transient_empty 1); |
568 by (etac leadsETo_induct 1); |
569 by (etac leadsETo_induct 1); |
569 by (asm_simp_tac (simpset() delsimps UN_simps |
570 by (asm_simp_tac (simpset() delsimps UN_simps |
570 addsimps [Int_UN_distrib, leadsETo_UN, extend_set_Union]) 3); |
571 addsimps [Int_UN_distrib, leadsETo_UN, extend_set_Union]) 3); |
571 by (blast_tac (claset() addIs [e_psp_stable2 RS leadsETo_weaken_L, |
572 by (blast_tac (claset() addIs [e_psp_stable2 RS leadsETo_weaken_L, |
572 leadsETo_Trans]) 2); |
573 leadsETo_Trans]) 2); |
573 auto(); |
574 by Auto_tac; |
574 by (force_tac (claset() addIs [leadsETo_Basis, subset_imp_ensures], |
575 by (force_tac (claset() addIs [leadsETo_Basis, subset_imp_ensures], |
575 simpset()) 1); |
576 simpset()) 1); |
576 by (rtac leadsETo_Basis 1); |
577 by (rtac leadsETo_Basis 1); |
577 by (asm_simp_tac (simpset() addsimps [Int_Diff, Int_extend_set_lemma, |
578 by (asm_simp_tac (simpset() addsimps [Int_Diff, Int_extend_set_lemma, |
578 extend_set_Diff_distrib RS sym]) 2); |
579 extend_set_Diff_distrib RS sym]) 2); |
640 qed "extending_LeadsETo"; |
641 qed "extending_LeadsETo"; |
641 |
642 |
642 |
643 |
643 (*** leadsETo in the precondition ***) |
644 (*** leadsETo in the precondition ***) |
644 |
645 |
645 Goalw [transient_def] |
|
646 "[| G : transient (C Int extend_set h A); G : stable C |] \ |
|
647 \ ==> project h C G : transient (project_set h C Int A)"; |
|
648 by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); |
|
649 by (subgoal_tac "act ^^ (C Int extend_set h A) <= - extend_set h A" 1); |
|
650 by (asm_full_simp_tac |
|
651 (simpset() addsimps [stable_def, constrains_def]) 2); |
|
652 by (Blast_tac 2); |
|
653 (*back to main goal*) |
|
654 by (thin_tac "?AA <= -C Un ?BB" 1); |
|
655 by (ball_tac 1); |
|
656 by (asm_full_simp_tac |
|
657 (simpset() addsimps [extend_set_def, project_act_def]) 1); |
|
658 by (Blast_tac 1); |
|
659 qed "transient_extend_set_imp_project_transient"; |
|
660 |
|
661 (*converse might hold too?*) |
|
662 Goalw [transient_def] |
|
663 "project h C (extend h F) : transient (project_set h C Int D) \ |
|
664 \ ==> F : transient (project_set h C Int D)"; |
|
665 by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); |
|
666 by (rtac bexI 1); |
|
667 by (assume_tac 2); |
|
668 by Auto_tac; |
|
669 by (rewtac extend_act_def); |
|
670 by (Blast_tac 1); |
|
671 qed "project_extend_transient_D"; |
|
672 |
|
673 |
|
674 Goal "[| extend h F : stable C; G : stable C; \ |
|
675 \ extend h F Join G : A ensures B; A-B = C Int extend_set h D |] \ |
|
676 \ ==> F Join project h C G \ |
|
677 \ : (project_set h C Int project_set h A) ensures (project_set h B)"; |
|
678 by (asm_full_simp_tac |
|
679 (simpset() addsimps [ensures_def, Join_constrains, project_constrains, |
|
680 Join_transient, extend_transient]) 1); |
|
681 by (Clarify_tac 1); |
|
682 by (REPEAT_FIRST (rtac conjI)); |
|
683 (*first subgoal*) |
|
684 by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS |
|
685 constrains_Int RS constrains_weaken] |
|
686 addSDs [extend_constrains_project_set] |
|
687 addSEs [equalityE]) 1); |
|
688 (*2nd subgoal*) |
|
689 by (etac (stableD RS constrains_Int RS constrains_weaken) 1); |
|
690 by (assume_tac 1); |
|
691 by (Blast_tac 3); |
|
692 by (full_simp_tac (simpset() addsimps [extend_set_Int_distrib, |
|
693 extend_set_Un_distrib]) 2); |
|
694 by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2); |
|
695 by (full_simp_tac (simpset() addsimps [extend_set_def]) 1); |
|
696 by (blast_tac (claset() addSEs [equalityE]) 1); |
|
697 (*The transient part*) |
|
698 by Auto_tac; |
|
699 by (force_tac (claset() addSEs [equalityE] |
|
700 addIs [transient_extend_set_imp_project_transient RS |
|
701 transient_strengthen], |
|
702 simpset()) 2); |
|
703 by (full_simp_tac (simpset() addsimps [Int_Diff]) 1); |
|
704 by (force_tac (claset() addSEs [equalityE] |
|
705 addIs [transient_extend_set_imp_project_transient RS |
|
706 project_extend_transient_D RS transient_strengthen], |
|
707 simpset()) 1); |
|
708 qed "ensures_extend_set_imp_project_ensures"; |
|
709 |
|
710 |
|
711 (*Lemma for the Trans case*) |
646 (*Lemma for the Trans case*) |
712 Goal "[| extend h F Join G : stable C; \ |
647 Goal "[| extend h F Join G : stable C; \ |
713 \ F Join project h C G \ |
648 \ F Join project h C G \ |
714 \ : project_set h C Int project_set h A leadsTo project_set h B |] \ |
649 \ : project_set h C Int project_set h A leadsTo project_set h B |] \ |
715 \ ==> F Join project h C G \ |
650 \ ==> F Join project h C G \ |