314 leadsETo_Trans]) 2); |
314 leadsETo_Trans]) 2); |
315 by (rtac leadsETo_Basis 1); |
315 by (rtac leadsETo_Basis 1); |
316 by (auto_tac (claset(), |
316 by (auto_tac (claset(), |
317 simpset() addsimps [Diff_eq_empty_iff RS iffD2, |
317 simpset() addsimps [Diff_eq_empty_iff RS iffD2, |
318 Int_Diff, ensures_def, |
318 Int_Diff, ensures_def, |
319 givenBy_eq_Collect, Join_stable, |
319 givenBy_eq_Collect, Join_transient])); |
320 Join_constrains, Join_transient])); |
|
321 by (blast_tac (claset() addIs [transient_strengthen]) 3); |
320 by (blast_tac (claset() addIs [transient_strengthen]) 3); |
322 by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable))); |
321 by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable))); |
323 by (rewtac stable_def); |
322 by (rewtac stable_def); |
324 by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 2); |
323 by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 2); |
325 by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1); |
324 by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1); |
333 by (blast_tac (claset() addIs [leadsETo_Trans]) 2); |
332 by (blast_tac (claset() addIs [leadsETo_Trans]) 2); |
334 by (rtac leadsETo_Basis 1); |
333 by (rtac leadsETo_Basis 1); |
335 by (case_tac "A <= B" 1); |
334 by (case_tac "A <= B" 1); |
336 by (etac subset_imp_ensures 1); |
335 by (etac subset_imp_ensures 1); |
337 by (auto_tac (claset() addIs [constrains_weaken], |
336 by (auto_tac (claset() addIs [constrains_weaken], |
338 simpset() addsimps [stable_def, ensures_def, |
337 simpset() addsimps [stable_def, ensures_def, Join_transient])); |
339 Join_constrains, Join_transient])); |
|
340 by (REPEAT (thin_tac "?F : ?A co ?B" 1)); |
338 by (REPEAT (thin_tac "?F : ?A co ?B" 1)); |
341 by (etac transientE 1); |
339 by (etac transientE 1); |
342 by (rewtac constrains_def); |
340 by (rewtac constrains_def); |
343 by (blast_tac (claset() addSDs [bspec]) 1); |
341 by (blast_tac (claset() addSDs [bspec]) 1); |
344 qed "Join_leadsETo_stable_imp_leadsETo"; |
342 qed "Join_leadsETo_stable_imp_leadsETo"; |
549 by (asm_simp_tac (simpset() addsimps [Int_Diff, Int_extend_set_lemma, |
547 by (asm_simp_tac (simpset() addsimps [Int_Diff, Int_extend_set_lemma, |
550 extend_set_Diff_distrib RS sym]) 2); |
548 extend_set_Diff_distrib RS sym]) 2); |
551 by (rtac Join_project_ensures_strong 1); |
549 by (rtac Join_project_ensures_strong 1); |
552 by (auto_tac (claset() addDs [preserves_o_project_transient_empty] |
550 by (auto_tac (claset() addDs [preserves_o_project_transient_empty] |
553 addIs [project_stable_project_set], |
551 addIs [project_stable_project_set], |
554 simpset() addsimps [Int_left_absorb, Join_stable])); |
552 simpset() addsimps [Int_left_absorb])); |
555 by (asm_simp_tac |
553 by (asm_simp_tac |
556 (simpset() addsimps [stable_ensures_Int RS ensures_weaken_R, |
554 (simpset() addsimps [stable_ensures_Int RS ensures_weaken_R, |
557 Int_lower2, project_stable_project_set, |
555 Int_lower2, project_stable_project_set, |
558 Join_stable, extend_stable_project_set]) 1); |
556 extend_stable_project_set]) 1); |
559 val lemma = result(); |
557 val lemma = result(); |
560 |
558 |
561 Goal "[| extend h F Join G : stable C; \ |
559 Goal "[| extend h F Join G : stable C; \ |
562 \ F Join project h C G : \ |
560 \ F Join project h C G : \ |
563 \ (project_set h C Int A) \ |
561 \ (project_set h C Int A) \ |
621 \ ==> F Join project h C G \ |
619 \ ==> F Join project h C G \ |
622 \ : project_set h C Int project_set h A leadsTo \ |
620 \ : project_set h C Int project_set h A leadsTo \ |
623 \ project_set h C Int project_set h B"; |
621 \ project_set h C Int project_set h B"; |
624 by (rtac (psp_stable2 RS leadsTo_weaken_L) 1); |
622 by (rtac (psp_stable2 RS leadsTo_weaken_L) 1); |
625 by (auto_tac (claset(), |
623 by (auto_tac (claset(), |
626 simpset() addsimps [project_stable_project_set, Join_stable, |
624 simpset() addsimps [project_stable_project_set, |
627 extend_stable_project_set])); |
625 extend_stable_project_set])); |
628 val lemma = result(); |
626 val lemma = result(); |
629 |
627 |
630 Goal "[| extend h F Join G : stable C; \ |
628 Goal "[| extend h F Join G : stable C; \ |
631 \ extend h F Join G : \ |
629 \ extend h F Join G : \ |
635 by (etac leadsETo_induct 1); |
633 by (etac leadsETo_induct 1); |
636 by (asm_simp_tac (HOL_ss addsimps [Int_UN_distrib, project_set_Union]) 3); |
634 by (asm_simp_tac (HOL_ss addsimps [Int_UN_distrib, project_set_Union]) 3); |
637 by (blast_tac (claset() addIs [leadsTo_UN]) 3); |
635 by (blast_tac (claset() addIs [leadsTo_UN]) 3); |
638 by (blast_tac (claset() addIs [leadsTo_Trans, lemma]) 2); |
636 by (blast_tac (claset() addIs [leadsTo_Trans, lemma]) 2); |
639 by (asm_full_simp_tac |
637 by (asm_full_simp_tac |
640 (simpset() addsimps [givenBy_eq_extend_set, Join_stable]) 1); |
638 (simpset() addsimps [givenBy_eq_extend_set]) 1); |
641 by (rtac leadsTo_Basis 1); |
639 by (rtac leadsTo_Basis 1); |
642 by (blast_tac (claset() addIs [leadsTo_Basis, |
640 by (blast_tac (claset() addIs [leadsTo_Basis, |
643 ensures_extend_set_imp_project_ensures]) 1); |
641 ensures_extend_set_imp_project_ensures]) 1); |
644 |
642 |
645 qed "project_leadsETo_I_lemma"; |
643 qed "project_leadsETo_I_lemma"; |