1.1 --- a/src/HOL/UNITY/WFair.ML	Thu Oct 28 16:04:57 1999 +0200
     1.2 +++ b/src/HOL/UNITY/WFair.ML	Thu Oct 28 16:06:07 1999 +0200
     1.3 @@ -475,37 +475,6 @@
     1.4  
     1.5  (*** Completion: Binary and General Finite versions ***)
     1.6  
     1.7 -Goal "[| F : A leadsTo A';  F : stable A';   \
     1.8 -\        F : B leadsTo B';  F : stable B' |] \
     1.9 -\   ==> F : (A Int B) leadsTo (A' Int B')";
    1.10 -by (subgoal_tac "F : stable (wlt F B')" 1);
    1.11 -by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
    1.12 -by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
    1.13 -	   rtac wlt_constrains_wlt 2,
    1.14 -	   fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
    1.15 -	   Blast_tac 2]);
    1.16 -by (subgoal_tac "F : (A Int wlt F B') leadsTo (A' Int wlt F B')" 1);
    1.17 -by (blast_tac (claset() addIs [psp_stable]) 2);
    1.18 -by (subgoal_tac "F : (A' Int wlt F B') leadsTo (A' Int B')" 1);
    1.19 -by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
    1.20 -by (subgoal_tac "F : (A Int B) leadsTo (A Int wlt F B')" 1);
    1.21 -by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
    1.22 -			       subset_imp_leadsTo]) 2);
    1.23 -by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
    1.24 -qed "stable_completion";
    1.25 -
    1.26 -
    1.27 -Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i)) -->  \
    1.28 -\                  (ALL i:I. F : stable (A' i)) -->         \
    1.29 -\                  F : (INT i:I. A i) leadsTo (INT i:I. A' i)";
    1.30 -by (etac finite_induct 1);
    1.31 -by (Asm_simp_tac 1);
    1.32 -by (asm_simp_tac 
    1.33 -    (simpset() addsimps [stable_completion, stable_def, 
    1.34 -			 ball_constrains_INT]) 1);
    1.35 -qed_spec_mp "finite_stable_completion";
    1.36 -
    1.37 -
    1.38  Goal "[| W = wlt F (B' Un C);     \
    1.39  \      F : A leadsTo (A' Un C);  F : A' co (A' Un C);   \
    1.40  \      F : B leadsTo (B' Un C);  F : B' co (B' Un C) |] \
    1.41 @@ -517,9 +486,8 @@
    1.42  by (asm_full_simp_tac 
    1.43      (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
    1.44  by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1);
    1.45 -by (simp_tac (simpset() addsimps [Int_Diff]) 2);
    1.46  by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2);
    1.47 -(** LEVEL 7 **)
    1.48 +(** LEVEL 6 **)
    1.49  by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
    1.50  by (rtac leadsTo_Un_duplicate2 2);
    1.51  by (blast_tac (claset() addIs [leadsTo_Un_Un, 
    1.52 @@ -538,9 +506,27 @@
    1.53  \                  (ALL i:I. F : (A' i) co (A' i Un C)) --> \
    1.54  \                  F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)";
    1.55  by (etac finite_induct 1);
    1.56 -by (ALLGOALS Asm_simp_tac);
    1.57 -by (Clarify_tac 1);
    1.58 +by Auto_tac;
    1.59  by (dtac ball_constrains_INT 1);
    1.60  by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 
    1.61  qed_spec_mp "finite_completion";
    1.62  
    1.63 +
    1.64 +Goalw [stable_def]
    1.65 +     "[| F : A leadsTo A';  F : stable A';   \
    1.66 +\        F : B leadsTo B';  F : stable B' |] \
    1.67 +\   ==> F : (A Int B) leadsTo (A' Int B')";
    1.68 +by (res_inst_tac [("C1", "{}")] (completion RS leadsTo_weaken_R) 1);
    1.69 +by (REPEAT (Force_tac 1));
    1.70 +qed "stable_completion";
    1.71 +
    1.72 +Goalw [stable_def]
    1.73 +     "[| finite I;  \
    1.74 +\        ALL i:I. F : (A i) leadsTo (A' i);  \
    1.75 +\        ALL i:I. F : stable (A' i) |]       \
    1.76 +\     ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)";
    1.77 +by (res_inst_tac [("C1", "{}")] (finite_completion RS leadsTo_weaken_R) 1);
    1.78 +by (REPEAT (Force_tac 1));
    1.79 +qed_spec_mp "finite_stable_completion";
    1.80 +
    1.81 +