--- 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]
--- 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> : \