519 by (asm_full_simp_tac |
519 by (asm_full_simp_tac |
520 (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2); |
520 (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2); |
521 by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1); |
521 by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1); |
522 by (simp_tac (simpset() addsimps [Int_Diff]) 2); |
522 by (simp_tac (simpset() addsimps [Int_Diff]) 2); |
523 by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2); |
523 by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2); |
|
524 (** LEVEL 7 **) |
524 by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1); |
525 by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1); |
525 by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, |
526 by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, |
526 psp2 RS leadsTo_weaken_R, |
527 psp2 RS leadsTo_weaken_R, |
527 subset_refl RS subset_imp_leadsTo, |
528 subset_refl RS subset_imp_leadsTo, |
528 leadsTo_Un_duplicate2]) 2); |
529 leadsTo_Un_duplicate2]) 2); |
529 by (dtac leadsTo_Diff 1); |
530 by (dtac leadsTo_Diff 1); |
530 by (assume_tac 2); |
531 by (assume_tac 2); |
531 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
532 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
532 by (subgoal_tac "A Int B <= A Int W" 1); |
533 by (subgoal_tac "A Int B <= A Int W" 1); |
533 by (blast_tac (claset() addIs [leadsTo_subset, Int_mono] |
534 by (blast_tac (claset() addSDs [leadsTo_subset] |
534 delrules [subsetI]) 2); |
535 addSIs [subset_refl RS Int_mono]) 2); |
535 by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); |
536 by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); |
536 bind_thm("completion", refl RS result()); |
537 bind_thm("completion", refl RS result()); |
537 |
538 |
538 |
539 |
539 Goal "[| finite I; id: acts |] \ |
540 Goal "[| finite I; id: acts |] \ |