# HG changeset patch
# User paulson
# Date 852637368 -3600
# Node ID 95c2f9c0930abdf1a7b2da7bf8b9dcca8a52b8ec
# Parent  87383dd9f4b543dcfab0e131538004d35d6d4253
Default rewrite rules for quantification over Collect(A,P)

diff -r 87383dd9f4b5 -r 95c2f9c0930a src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Tue Jan 07 12:37:07 1997 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Tue Jan 07 12:42:48 1997 +0100
@@ -398,8 +398,9 @@
 by (rtac CollectI 1);
 by (Fast_tac 1);
 by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1));
-by (Simp_tac 1);
+by (simp_tac (!simpset delsimps ball_simps) 1);
 by (REPEAT (resolve_tac [ballI, impI] 1));
+(** LEVEL 9 **)
 by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1
         THEN REPEAT (assume_tac 1));
 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
@@ -416,12 +417,12 @@
 val ex_eq_succ = result();
 
 goal thy
-        "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}.  \
-\       EX! w. w:t_n & z <= w; \
-\       well_ord(y,R); ~Finite(y); u:x; x Int y = 0;  \
-\       t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)};  \
-\       ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat  \
-\       |] ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}.  \
+\                  EX! w. w:t_n & z <= w; \
+\         well_ord(y,R); ~Finite(y); u:x; x Int y = 0;  \
+\         t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)};  \
+\         ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat  \
+\      |] ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
 by (rtac suppose_not 1);
 by (eresolve_tac [ex_eq_succ RS bexE] 1 THEN (assume_tac 1));
 by (hyp_subst_tac 1);
@@ -579,7 +580,7 @@
 by (res_inst_tac [("x","w Int y")] bexI 1);
 by (etac Int_in_LL 2);
 by (rewtac GG_def);
-by (asm_full_simp_tac (!simpset addsimps [Int_in_LL]) 1);
+by (asm_full_simp_tac (!simpset delsimps ball_simps addsimps [Int_in_LL]) 1);
 by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1
         THEN (assume_tac 1));
 by (REPEAT (fast_tac (!claset addEs [equals0D] addSEs [Int_in_LL]) 1));
@@ -608,9 +609,9 @@
 \       t_n <= {v:Pow(x Un y). v eqpoll n};  \
 \       v : LL(t_n, k, y) |]  \
 \       ==> GG(t_n, k, y) ` v <= x";
-by (Asm_full_simp_tac 1);
 by (forward_tac [the_in_MM_subset] 1 THEN REPEAT (assume_tac 1));
 by (dtac in_LL_eq_Int 1 THEN REPEAT (assume_tac 1));
+by (Asm_full_simp_tac 1);
 by (rtac subsetI 1);
 by (etac DiffE 1);
 by (etac swap 1);
@@ -666,8 +667,11 @@
 \       (GG(t_n, succ(k), y)) `  \
 \       (converse(ordermap(LL(t_n, succ(k), y), S)) ` b) lepoll m";
 by (rtac oallI 1);
-by (asm_full_simp_tac (!simpset addsimps [ltD,
-        ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1);
+by (asm_full_simp_tac 
+    (!simpset delsimps ball_simps
+              addsimps [ltD,
+			ordermap_bij RS bij_converse_bij RS
+			bij_is_fun RS apply_type]) 1);
 by (rtac eqpoll_sum_imp_Diff_lepoll 1);
 by (REPEAT (fast_tac 
 	    (FOL_cs addSDs [ltD]
diff -r 87383dd9f4b5 -r 95c2f9c0930a src/ZF/AC/DC.ML
--- a/src/ZF/AC/DC.ML	Tue Jan 07 12:37:07 1997 +0100
+++ b/src/ZF/AC/DC.ML	Tue Jan 07 12:42:48 1997 +0100
@@ -293,16 +293,16 @@
 \       (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))";
 by (rtac conjI 1);
 by (deepen_tac (!claset addSEs [FinD RS PowI]) 0 1);
-by (rtac ballI 1);
-by (rtac impI 1);
+by (rtac (impI RS ballI) 1);
 by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1
         THEN (assume_tac 1));
 by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f))  \
 \       & (ALL f:Y. restrict(g, domain(f)) = f)" 1);
-by (fast_tac (!claset addss (!simpset)) 2);
+by (etac subst 2 THEN (*elimination equation for greater speed*)
+    fast_tac (!claset addss (!simpset)) 2);
 by (step_tac (!claset delrules [domainE]) 1);
-by(swap_res_tac [bexI] 1 THEN etac singleton_in_funs 2);
-by (asm_simp_tac (!simpset addsimps [nat_0I  RSN (2, bexI), 
+by (swap_res_tac [bexI] 1 THEN etac singleton_in_funs 2);
+by (asm_full_simp_tac (!simpset addsimps [nat_0I  RSN (2, bexI), 
 				     cons_fun_type2, empty_fun]) 1);
 val lemma1 = result();
 
@@ -411,15 +411,15 @@
 by (etac domainE 1);
 
 by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1));
+br bexI 1;
+by (etac nat_succI 2);
 by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1);
+br conjI 1;
 by (fast_tac (FOL_cs
         addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ,
-        subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1);
-by (rtac UN_I 1);
-by (etac nat_succI 1);
-by (rtac CollectI 1);
-by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1
-        THEN REPEAT (assume_tac 1));
+        subst_context, all_in_image_restrict_eq, trans, equalityD1]) 2);
+by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 2
+        THEN REPEAT (assume_tac 2));
 by (rtac ballI 1);
 by (etac succE 1);
 (** LEVEL 25 **)
@@ -431,7 +431,7 @@
 by (asm_full_simp_tac (!simpset addsimps [cons_val_n, cons_val_k]) 1);
 val simplify_recursion = result();
 
- 
+
 goal thy "!!X. [| XX = (UN n:nat.  \
 \               {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R});  \
 \       ALL b<nat. <f``b, f`b> :  \