diff -r d5c7a111cea7 -r 6664d0b54d0f src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Thu Apr 13 11:44:37 1995 +0200
+++ b/src/ZF/AC/WO6_WO1.ML	Thu Apr 13 14:15:36 1995 +0200
@@ -2,12 +2,30 @@
     ID:         $Id$
     Author: 	Krzysztof Gr`abczewski
 
-The proof of "WO6 ==> WO1".
+The proof of "WO6 ==> WO1".  Simplified by L C Paulson.
 
 From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
 pages 2-5
+
+Simplifier bug in proof of UN_gg2_eq????
 *)
 
+open WO6_WO1;
+
+goal OrderType.thy 
+      "!!i j k. [| k < i++j;  Ord(i);  Ord(j) |] ==>  \
+\                  k < i  |  (~ k<i & k = i ++ (k--i) & (k--i)<j)";
+by (res_inst_tac [("i","k"),("j","i")] Ord_linear2 1);
+by (dtac odiff_lt_mono2 4 THEN assume_tac 4);
+by (asm_full_simp_tac
+    (ZF_ss addsimps [oadd_odiff_inverse, odiff_oadd_inverse]) 4);
+by (safe_tac (ZF_cs addSEs [lt_Ord]));
+val lt_oadd_odiff_disj = result();
+
+(*The corresponding elimination rule*)
+val lt_oadd_odiff_cases = rule_by_tactic (safe_tac ZF_cs)
+                                         (lt_oadd_odiff_disj RS disjE);
+
 (* ********************************************************************** *)
 (* The most complicated part of the proof - lemma ii - p. 2-4		  *)
 (* ********************************************************************** *)
@@ -20,18 +38,12 @@
 by (fast_tac ZF_cs 1);
 val domain_uu_subset = result();
 
-goal thy "!!a. [| ALL b<a. f`b lepoll m; b<a |]  \
-\		==> domain(uu(f, b, g, d)) lepoll m";
+goal thy "!! a. ALL b<a. f`b lepoll m ==> \
+\               ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m";
 by (fast_tac (AC_cs addSEs
 	[domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1);
-val domain_uu_lepoll_m = result();
-
-goal thy "!! a. ALL b<a. f`b lepoll m ==> \
-\          ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m";
-by (fast_tac (AC_cs addEs [domain_uu_lepoll_m]) 1);
 val quant_domain_uu_lepoll_m = result();
 
-(* used in case 2 *)
 goalw thy [uu_def] "uu(f,b,g,d) <= f`b * f`g";
 by (fast_tac ZF_cs 1);
 val uu_subset1 = result();
@@ -40,7 +52,7 @@
 by (fast_tac ZF_cs 1);
 val uu_subset2 = result();
 
-goal thy "!! a. [| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m";
+goal thy "!! a. [| ALL b<a. f`b lepoll m;  d<a |] ==> uu(f,b,g,d) lepoll m";
 by (fast_tac (AC_cs
 	addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
 val uu_lepoll_m = result();
@@ -50,74 +62,55 @@
 (* ********************************************************************** *)
 goalw thy [lesspoll_def] 
   "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==>  \
-\ (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 &  \
-\				u(f,b,g,d) lesspoll m)) |  \
-\ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 -->  \
-\				u(f,b,g,d) eqpoll m))";
+\            (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 &  \
+\		           		u(f,b,g,d) lesspoll m)) |  \
+\            (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 -->  \
+\		           		u(f,b,g,d) eqpoll m))";
+by (asm_simp_tac OrdQuant_ss 1);
 by (fast_tac AC_cs 1);
 val cases = result();
 
 (* ********************************************************************** *)
 (* Lemmas used in both cases						  *)
 (* ********************************************************************** *)
-goal thy "!!a f. Ord(a) ==> (UN b<a++a. f`b) = (UN b<a. f`b Un f`(a++b))";
-by (resolve_tac [equalityI] 1);
-by (fast_tac (AC_cs addIs [ltI, OUN_I] addSEs [OUN_E]
-		addSDs [lt_oadd_disj]) 1);
-by (fast_tac (AC_cs addSEs [lt_oadd1, oadd_lt_mono2, OUN_E]
-		addSIs [OUN_I]) 1);
+goal thy "!!a C. Ord(a) ==> (UN b<a++a. C(b)) = (UN b<a. C(b) Un C(a++b))";
+by (fast_tac (AC_cs addSIs [equalityI] addIs [ltI] 
+                    addSDs [lt_oadd_disj]
+                    addSEs [lt_oadd1, oadd_lt_mono2]) 1);
 val UN_oadd = result();
 
-val [prem] = goal thy
-	"(!!b. b<a ==> P(b)=Q(b)) ==> (UN b<a. P(b)) = (UN b<a. Q(b))";
-by (fast_tac (ZF_cs addSIs [OUN_I, equalityI] 
-		addSEs [OUN_E, prem RS equalityD1 RS subsetD, 
-			prem RS sym RS equalityD1 RS subsetD]) 1);
-val UN_eq = result();
-
-goal thy "!!a. b<a ==> b = (THE l. l<a & a ++ b = a ++ l)";
-by (fast_tac (ZF_cs addSIs [the_equality RS sym] 
-                    addIs [lt_Ord2, lt_Ord] 
-                    addSEs [oadd_inject RS sym]) 1);
-val the_only_b = result();
-
-goal thy "!!A. B <= A ==> B Un (A-B) = A";
-by (fast_tac (ZF_cs addSIs [equalityI]) 1);
-val subset_imp_Un_Diff_eq = result();
 
 (* ********************************************************************** *)
 (* Case 1 : lemmas							  *)
 (* ********************************************************************** *)
 
-goalw thy [vv1_def] "vv1(f,b,succ(m)) <= f`b";
-by (resolve_tac [expand_if RS iffD2] 1);
-by (fast_tac (ZF_cs addSIs [domain_uu_subset]) 1);
+goalw thy [vv1_def] "vv1(f,m,b) <= f`b";
+by (rtac (letI RS letI) 1);
+by (split_tac [expand_if] 1);
+by (simp_tac (ZF_ss addsimps [domain_uu_subset]) 1);
 val vv1_subset = result();
 
 (* ********************************************************************** *)
 (* Case 1 : Union of images is the whole "y"				  *)
 (* ********************************************************************** *)
-goal thy "!! a f y. [| (UN b<a. f`b) = y; Ord(a); m:nat |] ==>  \
-\	(UN b<a++a. (lam b:a++a. if(b<a, vv1(f,b,succ(m)),  \
-\			ww1(f, THE l. l<a & b=a++l, succ(m)))) ` b) = y";
-by (resolve_tac [UN_oadd RS ssubst] 1 THEN (atac 1));
-by (eresolve_tac [subst] 1);
-by (resolve_tac [UN_eq] 1);
-by (forw_inst_tac [("i","a")] lt_oadd1 1
-	THEN (REPEAT (atac 1)));
-by (forw_inst_tac [("j","a")] oadd_lt_mono2 1
-	THEN (REPEAT (atac 1)));
-by (asm_simp_tac (ZF_ss addsimps [ltD RS beta,
-	oadd_le_self RS le_imp_not_lt RS if_not_P, lt_Ord]) 1);
-by (resolve_tac [the_only_b RS subst] 1 THEN (atac 1));
-by (asm_simp_tac (ZF_ss 
-	addsimps [vv1_subset RS subset_imp_Un_Diff_eq, ltD, ww1_def]) 1);
-val UN_eq_y = result();
+goalw thy [gg1_def]
+  "!! a f y. [| Ord(a);  m:nat |] ==>  	\
+\	     (UN b<a++a. gg1(f,a,m)`b) = (UN b<a. f`b)";
+by (asm_simp_tac
+    (OrdQuant_ss addsimps [UN_oadd, lt_oadd1,
+			   oadd_le_self RS le_imp_not_lt, lt_Ord,
+			   odiff_oadd_inverse, ltD,
+			   vv1_subset RS Diff_partition, ww1_def]) 1);
+val UN_gg1_eq = result();
+
+goal thy "domain(gg1(f,a,m)) = a++a";
+by (simp_tac (ZF_ss addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1);
+val domain_gg1 = result();
 
 (* ********************************************************************** *)
 (* every value of defined function is less than or equipollent to m	  *)
 (* ********************************************************************** *)
-goal thy "!!a b. [| P(a, b); Ord(a); Ord(b);  \
+goal thy "!!a b. [| P(a, b);  Ord(a);  Ord(b);  \
 \		Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |]  \
 \		==> P(Least_a, LEAST b. P(Least_a, b))";
 by (eresolve_tac [ssubst] 1);
@@ -125,69 +118,40 @@
 by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1));
 val nested_LeastI = result();
 
-val nested_Least_instance = read_instantiate 
+val nested_Least_instance = 
+   standard
+     (read_instantiate 
 	[("P","%g d. domain(uu(f,b,g,d)) ~= 0 &  \
-\		domain(uu(f,b,g,d)) lesspoll succ(m)")] nested_LeastI;
+\		domain(uu(f,b,g,d)) lepoll m")] nested_LeastI);
 
-goalw thy [vv1_def] "!!a. [| ALL b<a. f`b ~=0 -->  \
-\		(EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 &  \
-\		domain(uu(f,b,g,d)) lesspoll succ(m)); m:nat; b<a |]  \
-\		==> vv1(f,b,succ(m)) lesspoll succ(m)";
-by (resolve_tac [expand_if RS iffD2] 1);
+goalw thy [gg1_def]
+    "!!a. [| Ord(a);  m:nat;  \
+\	     ALL b<a. f`b ~=0 -->  					\
+\	     (EX g<a. EX d<a. domain(uu(f,b,g,d)) ~= 0  &  		\
+\	                      domain(uu(f,b,g,d)) lepoll m);    	\
+\            ALL b<a. f`b lepoll succ(m);  b<a++a			\
+\	  |] ==> gg1(f,a,m)`b lepoll m";
+by (asm_simp_tac OrdQuant_ss 1);
+by (safe_tac (OrdQuant_cs addSEs [lt_oadd_odiff_cases]));
+(*Case b<a   : show vv1(f,m,b) lepoll m *)
+by (asm_simp_tac (ZF_ss addsimps [vv1_def, Let_def] 
+                        setloop split_tac [expand_if]) 1);
 by (fast_tac (AC_cs addIs [nested_Least_instance RS conjunct2]
 		addSEs [lt_Ord]
-		addSIs [empty_lepollI RS lepoll_imp_lesspoll_succ]) 1);
-val vv1_lesspoll_succ = result();
-
-goalw thy [vv1_def] "!!a. [| ALL b<a. f`b ~=0 -->  \
-\	(EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 &  \
-\	domain(uu(f,b,g,d)) lesspoll succ(m)); m:nat; b<a; f`b ~= 0 |]  \
-\	==> vv1(f,b,succ(m)) ~= 0";
-by (resolve_tac [expand_if RS iffD2] 1);
-by (resolve_tac [conjI] 1);
-by (fast_tac ZF_cs 2);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [oallE] 1);
-by (mp_tac 1);
-by (contr_tac 2);
-by (REPEAT (eresolve_tac [oexE] 1));
+		addSIs [empty_lepollI]) 1);
+(*Case a le b: show ww1(f,m,b--a) lepoll m *)
+by (asm_simp_tac (ZF_ss addsimps [ww1_def]) 1);
+by (excluded_middle_tac "f`(b--a) = 0" 1);
+by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
+by (resolve_tac [Diff_lepoll] 1);
+by (fast_tac AC_cs 1);
+by (rtac vv1_subset 1);
+by (dtac (ospec RS mp) 1);
+by (REPEAT (eresolve_tac [asm_rl, oexE] 1));
 by (asm_simp_tac (ZF_ss
-	addsimps [lt_Ord, nested_Least_instance RS conjunct1]) 1);
-val vv1_not_0 = result();
-
-goalw thy [ww1_def] "!!a. [| ALL b<a. f`b ~=0 -->  \
-\	(EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 &  \
-\	domain(uu(f,b,g,d)) lesspoll succ(m));  \
-\	ALL b<a. f`b lepoll succ(m); m:nat; b<a  |]  \
-\	==> ww1(f,b,succ(m)) lesspoll succ(m)";
-by (excluded_middle_tac "f`b = 0" 1);
-by (asm_full_simp_tac (AC_ss
-	addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2);
-by (resolve_tac [Diff_lepoll RS lepoll_imp_lesspoll_succ] 1);
-by (fast_tac AC_cs 1);
-by (REPEAT (ares_tac [vv1_subset, vv1_not_0] 1));
-val ww1_lesspoll_succ = result();
-
-goal thy "!!a. [| Ord(a); m:nat;  \
-\	ALL b<a. f`b ~=0 --> (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 &  \
-\			domain(uu(f,b,g,d)) lesspoll succ(m));  \
-\	ALL b<a. f`b lepoll succ(m) |]  \
-\	==> ALL b<a++a. (lam b:a++a. if(b<a, vv1(f,b,succ(m)),  \
-\		ww1(f,THE l. l<a & b = a ++ l,succ(m))))`b lepoll m";
-by (resolve_tac [oallI] 1);
-by (asm_full_simp_tac (ZF_ss addsimps [ltD RS beta]) 1);
-by (resolve_tac [lesspoll_succ_imp_lepoll] 1 THEN (atac 2));
-by (resolve_tac [expand_if RS iffD2] 1);
-by (resolve_tac [conjI] 1);
-by (resolve_tac [impI] 1);
-by (forward_tac [lt_oadd_disj1] 2 THEN (REPEAT (atac 2)));
-by (resolve_tac [impI] 2);
-by (eresolve_tac [disjE] 2 THEN (fast_tac (ZF_cs addSEs [ltE]) 2));
-by (asm_full_simp_tac (ZF_ss addsimps [vv1_lesspoll_succ]) 1);
-by (dresolve_tac [theI] 1);
-by (eresolve_tac [conjE] 1);
-by (resolve_tac [ww1_lesspoll_succ] 1 THEN (REPEAT (atac 1)));
-val all_sum_lepoll_m = result();
+	addsimps [vv1_def, Let_def, lt_Ord, 
+		  nested_Least_instance RS conjunct1]) 1);
+val gg1_lepoll_m = result();
 
 (* ********************************************************************** *)
 (* Case 2 : lemmas							  *)
@@ -197,9 +161,9 @@
 (* Case 2 : vv2_subset							  *)
 (* ********************************************************************** *)
 
-goalw thy [uu_def] "!!f. [| b<a; g<a; f`b~=0; f`g~=0;  \
-\			y*y <= y; (UN b<a. f`b)=y |]  \
-\			==> EX d<a. uu(f,b,g,d)~=0";
+goalw thy [uu_def] "!!f. [| b<a;  g<a;  f`b~=0;  f`g~=0;  \
+\			    y*y <= y;  (UN b<a. f`b)=y  \
+\			 |] ==> EX d<a. uu(f,b,g,d) ~= 0";
 by (fast_tac (AC_cs addSIs [not_emptyI] 
 		addSDs [SigmaI RSN (2, subsetD)]
 		addSEs [not_emptyE]) 1);
@@ -208,12 +172,11 @@
 goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0;  \
 \			y*y<=y;	(UN b<a. f`b)=y |]  \
 \		==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
-by (dresolve_tac [ex_d_uu_not_empty] 1 THEN (REPEAT (atac 1)));
+by (dresolve_tac [ex_d_uu_not_empty] 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (AC_cs addSEs [LeastI, lt_Ord]) 1);
 val uu_not_empty = result();
 
-(* moved from ZF_aux.ML *)
-goal thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
+goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
 by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, 
 		sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
 val not_empty_rel_imp_domain = result();
@@ -222,131 +185,125 @@
 \			y*y <= y; (UN b<a. f`b)=y |]  \
 \		==> (LEAST d. uu(f,b,g,d) ~= 0) < a";
 by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1
-	THEN (REPEAT (atac 1)));
+	THEN REPEAT (assume_tac 1));
 by (resolve_tac [Least_le RS lt_trans1] 1
 	THEN (REPEAT (ares_tac [lt_Ord] 1)));
 val Least_uu_not_empty_lt_a = result();
 
-goal thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
+goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
 by (fast_tac ZF_cs 1);
 val subset_Diff_sing = result();
 
+(*Could this be proved more directly?*)
 goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
 by (eresolve_tac [natE] 1);
 by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
 by (hyp_subst_tac 1);
 by (resolve_tac [equalityI] 1);
-by (atac 2);
+by (assume_tac 2);
 by (resolve_tac [subsetI] 1);
-by (excluded_middle_tac "?P" 1 THEN (atac 2));
+by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
 by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2, 
 		diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS 
 		succ_lepoll_natE] 1
-	THEN (REPEAT (atac 1)));
+	THEN REPEAT (assume_tac 1));
 val supset_lepoll_imp_eq = result();
 
-goalw thy [vv2_def] 
+goal thy
 	"!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 -->  \
 \	domain(uu(f, b, g, d)) eqpoll succ(m);  \
 \	ALL b<a. f`b lepoll succ(m); y*y <= y;  \
-\	(UN b<a. f`b)=y; b<a; g<a; d<a; f`b~=0; f`g~=0; m:nat; aa:f`b |]  \
+\	(UN b<a. f`b)=y; b<a; g<a; d<a; f`b~=0; f`g~=0; m:nat; s:f`b |]  \
 \	 ==> uu(f,b,g,LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g";
 by (eres_inst_tac [("x","g")] oallE 1 THEN (contr_tac 2));
 by (eres_inst_tac [("P","%z. ?QQ(z) ~= 0 --> ?RR(z)")] oallE 1);
 by (eresolve_tac [impE] 1);
-by (eresolve_tac [uu_not_empty RS (uu_subset1 RS 
-	not_empty_rel_imp_domain)] 1
-	THEN (REPEAT (atac 1)));
+by (eresolve_tac [uu_not_empty RS (uu_subset1 RS not_empty_rel_imp_domain)] 1
+	THEN REPEAT (assume_tac 1));
 by (eresolve_tac [Least_uu_not_empty_lt_a RSN (2, notE)] 2
-	THEN (TRYALL atac));
+	THEN (TRYALL assume_tac));
 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS 
 	(Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2, 
 	uu_subset1 RSN (4, rel_is_fun)))] 1
-	THEN (TRYALL atac));
+	THEN (TRYALL assume_tac));
 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, 
 		supset_lepoll_imp_eq)] 1);
 by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1));
 val uu_Least_is_fun = result();
 
 goalw thy [vv2_def]
-	"!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 -->  \
-\		domain(uu(f, b, g, d)) eqpoll succ(m);  \
-\		ALL b<a. f`b lepoll succ(m); y*y <= y;  \
-\		(UN b<a. f`b)=y; b<a; g<a; m:nat; aa:f`b |]  \
-\		==> vv2(f,b,g,aa) <= f`g";
-by (fast_tac (FOL_cs addIs [expand_if RS iffD2]
-	addSEs [uu_Least_is_fun]
-	addSIs [empty_subsetI, not_emptyI, 
-		singleton_subsetI, apply_type]) 1);
+    "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 -->		\
+\	     domain(uu(f, b, g, d)) eqpoll succ(m);			\
+\	     ALL b<a. f`b lepoll succ(m); y*y <= y;			\
+\	     (UN b<a. f`b)=y;  b<a;  g<a;  m:nat;  s:f`b		\
+\	   |] ==> vv2(f,b,g,s) <= f`g";
+by (split_tac [expand_if] 1);
+by (fast_tac (FOL_cs addSEs [uu_Least_is_fun]
+	             addSIs [empty_subsetI, not_emptyI, 
+			     singleton_subsetI, apply_type]) 1);
 val vv2_subset = result();
 
 (* ********************************************************************** *)
 (* Case 2 : Union of images is the whole "y"				  *)
 (* ********************************************************************** *)
-goal thy "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 -->  \
-\	domain(uu(f,b,g,d)) eqpoll succ(m);  \
-\	ALL b<a. f`b lepoll succ(m); y*y<=y;  \
-\	(UN b<a.f`b)=y; Ord(a); m:nat; aa:f`b; b<a |]  \
-\	==> (UN g<a++a. (lam g:a++a. if(g<a, vv2(f,b,g,aa),  \
-\			ww2(f,b,THE l. l<a & g=a++l,aa)))`g) = y";
-by (resolve_tac [UN_oadd RS ssubst] 1 THEN (atac 1));
-by (resolve_tac [subst] 1 THEN (atac 1));
-by (resolve_tac [UN_eq] 1);
-by (forw_inst_tac [("i","a"),("k","ba")] lt_oadd1 1
-	THEN (REPEAT (atac 1)));
-by (forw_inst_tac [("j","a"),("k","ba")] oadd_lt_mono2 1
-	THEN (REPEAT (atac 1)));
-by (asm_simp_tac (ZF_ss addsimps [ltD RS beta,
-	oadd_le_self RS le_imp_not_lt RS if_not_P, lt_Ord]) 1);
-by (resolve_tac [the_only_b RS subst] 1 THEN (atac 1));
-by (asm_simp_tac (ZF_ss 
-	addsimps [vv2_subset RS subset_imp_Un_Diff_eq, ltI, ww2_def]) 1);
-val UN_eq_y_2 = result();
+goalw thy [gg2_def]
+    "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 -->  		\
+\	     domain(uu(f,b,g,d)) eqpoll succ(m);  			\
+\	     ALL b<a. f`b lepoll succ(m); y*y<=y;  			\
+\	     (UN b<a.f`b)=y;  Ord(a);  m:nat;  s:f`b;  b<a		\
+\	  |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
+bd sym 1;
+by (asm_simp_tac
+    (OrdQuant_ss addsimps [UN_oadd, lt_oadd1,
+			   oadd_le_self RS le_imp_not_lt, lt_Ord,
+			   odiff_oadd_inverse, ww2_def,
+			   standard (vv2_subset RS Diff_partition)]) 1);
+(*Omitting "standard" above causes "Failed congruence proof!" bug??*)
+val UN_gg2_eq = result();
+
+goal thy "domain(gg2(f,a,b,s)) = a++a";
+by (simp_tac (ZF_ss addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1);
+val domain_gg2 = result();
 
 (* ********************************************************************** *)
 (* every value of defined function is less than or equipollent to m	  *)
 (* ********************************************************************** *)
 
 goalw thy [vv2_def]
-	"!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,aa) lesspoll succ(m)";
-by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
-by (asm_simp_tac (AC_ss
-	addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2);
+    "!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
+by (asm_simp_tac (OrdQuant_ss
+	addsimps [empty_lepollI]
+        setloop split_tac [expand_if]) 1);
 by (fast_tac (AC_cs
 	addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0]
-	addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS 
-			lepoll_trans RS lepoll_imp_lesspoll_succ,
+	addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
 		not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll,
 		nat_into_Ord, nat_1I]) 1);
-val vv2_lesspoll_succ = result();
-
-goalw thy [ww2_def] "!!m. [| ALL b<a. f`b lepoll succ(m); g<a; m:nat;  \
-\			vv2(f,b,g,d) <= f`g |]  \
-\			==> ww2(f,b,g,d) lesspoll succ(m)";
-by (excluded_middle_tac "f`g = 0" 1);
-by (asm_simp_tac (AC_ss
-		addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2);
-by (dresolve_tac [ospec] 1 THEN (atac 1));
-by (resolve_tac [Diff_lepoll RS lepoll_imp_lesspoll_succ] 1
-	THEN (TRYALL atac));
-by (asm_simp_tac (AC_ss addsimps [vv2_def, expand_if, not_emptyI]) 1);
-val ww2_lesspoll_succ = result();
+val vv2_lepoll = result();
 
-goal thy "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 -->  \
-\		domain(uu(f,b,g,d)) eqpoll succ(m);  \
-\		ALL b<a. f`b lepoll succ(m); y*y <= y;  \
-\		(UN b<a. f`b)=y; b<a; aa:f`b; m:nat; m~= 0 |]  \
-\		==> ALL ba<a++a. (lam g:a++a. if(g<a, vv2(f,b,g,aa),  \
-\			ww2(f,b,THE l. l<a & g=a++l,aa)))`ba lepoll m";
-by (resolve_tac [oallI] 1);
-by (asm_full_simp_tac AC_ss 1);
-by (resolve_tac [lesspoll_succ_imp_lepoll] 1 THEN (atac 2));
-by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
-by (asm_simp_tac (AC_ss addsimps [vv2_lesspoll_succ]) 1);
-by (forward_tac [lt_oadd_disj1] 1 THEN (REPEAT (ares_tac [lt_Ord2] 1)));
-by (fast_tac (FOL_cs addSIs [ww2_lesspoll_succ, vv2_subset]
-		addSDs [theI]) 1);
-val all_sum_lepoll_m_2 = result();
+goalw thy [ww2_def]
+    "!!m. [| ALL b<a. f`b lepoll succ(m);  g<a;  m:nat;  vv2(f,b,g,d) <= f`g  \
+\	  |] ==> ww2(f,b,g,d) lepoll m";
+by (excluded_middle_tac "f`g = 0" 1);
+by (asm_simp_tac (OrdQuant_ss
+		addsimps [empty_lepollI]) 2);
+by (dresolve_tac [ospec] 1 THEN (assume_tac 1));
+by (resolve_tac [Diff_lepoll] 1
+	THEN (TRYALL assume_tac));
+by (asm_simp_tac (OrdQuant_ss addsimps [vv2_def, expand_if, not_emptyI]) 1);
+val ww2_lepoll = result();
+
+goalw thy [gg2_def]
+    "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 -->		\
+\	     domain(uu(f,b,g,d)) eqpoll succ(m);			\
+\	     ALL b<a. f`b lepoll succ(m);  y*y <= y;			\
+\	     (UN b<a. f`b)=y;  b<a;  s:f`b;  m:nat;  m~= 0;  g<a++a	\
+\         |] ==> gg2(f,a,b,s) ` g lepoll m";
+by (asm_simp_tac OrdQuant_ss 1);
+by (safe_tac (OrdQuant_cs addSEs [lt_oadd_odiff_cases, lt_Ord2]));
+by (asm_simp_tac (OrdQuant_ss addsimps [vv2_lepoll]) 1);
+by (asm_simp_tac (ZF_ss addsimps [ww2_lepoll, vv2_subset]) 1);
+val gg2_lepoll_m = result();
 
 (* ********************************************************************** *)
 (* lemma ii	 							  *)
@@ -355,25 +312,23 @@
 	"!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1));
 by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1
-    THEN (atac 1));
+    THEN (assume_tac 1));
 (* case 1 *)
-by (resolve_tac [CollectI] 1);
-by (atac 1);
-by (res_inst_tac [("x","a ++ a")] exI 1);
-by (res_inst_tac [("x","lam b:a++a. if (b<a, vv1(f,b,succ(m)),  \
-\			ww1(f,THE l. l<a & b=a++l,succ(m)))")] exI 1);
-by (fast_tac (FOL_cs addSIs [Ord_oadd, lam_funtype RS domain_of_fun,
-				UN_eq_y, all_sum_lepoll_m]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [lesspoll_succ_iff]) 1);
+by (res_inst_tac [("x","a++a")] exI 1);
+by (fast_tac (OrdQuant_cs addSIs [Ord_oadd, domain_gg1, UN_gg1_eq, 
+				  gg1_lepoll_m]) 1);
 (* case 2 *)
 by (REPEAT (eresolve_tac [oexE, conjE] 1));
+by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (assume_tac 1));
 by (resolve_tac [CollectI] 1);
 by (eresolve_tac [succ_natD] 1);
-by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (atac 1));
 by (res_inst_tac [("x","a++a")] exI 1);
-by (res_inst_tac [("x","lam g:a++a. if (g<a, vv2(f,b,g,x),  \
-\			ww2(f,b,THE l. l<a & g=a++l,x))")] exI 1);
-by (fast_tac (FOL_cs addSIs [Ord_oadd, lam_funtype RS domain_of_fun,
-				UN_eq_y_2, all_sum_lepoll_m_2]) 1);
+by (res_inst_tac [("x","gg2(f,a,b,x)")] exI 1);
+(*Calling fast_tac might get rid of the res_inst_tac calls, but it
+  is just too slow.*)
+by (asm_simp_tac (OrdQuant_ss addsimps 
+		  [Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1);
 val lemma_ii = result();
 
 
@@ -392,7 +347,7 @@
 
 goal thy "!!n. [| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |]  \
 \              ==> f(n)<=f(m)";
-by (res_inst_tac [("P","n le m")] impE 1 THEN (REPEAT (atac 2)));
+by (res_inst_tac [("P","n le m")] impE 1 THEN (REPEAT (assume_tac 2)));
 by (res_inst_tac [("P","%z. n le z --> f(n) <= f(z)")] nat_induct 1);
 by (REPEAT (fast_tac lt_cs 1));
 val le_subsets = result();
@@ -400,26 +355,20 @@
 goal thy "!!n m. [| n le m; m:nat |] ==>  \
 \	rec(n, x, %k r. r Un r*r) <= rec(m, x, %k r. r Un r*r)";
 by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1 
-    THEN (TRYALL atac));
+    THEN (TRYALL assume_tac));
 by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1
-    THEN (atac 1));
+    THEN (assume_tac 1));
 val le_imp_rec_subset = result();
 
-goal thy "!!x. EX y. x Un y*y <= y";
+goal thy "EX y. x Un y*y <= y";
 by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [UnE] 1);
-by (resolve_tac [UN_I] 1);
-by (eresolve_tac [rec_0 RS ssubst] 2);
-by (resolve_tac [nat_0I] 1);
-by (eresolve_tac [SigmaE] 1);
-by (REPEAT (eresolve_tac [UN_E] 1));
+by (safe_tac ZF_cs);
+by (fast_tac (ZF_cs addSIs [nat_0I] addss nat_ss) 1);
 by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
-by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (atac 1));
-by (resolve_tac [rec_succ RS ssubst] 1);
+by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (assume_tac 1));
 by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD]
 		addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type]
-		addSEs [nat_into_Ord]) 1);
+		addSEs [nat_into_Ord] addss nat_ss) 1);
 val lemma_iv = result();
 
 (* ********************************************************************** *)
@@ -453,7 +402,7 @@
 
 goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |]  \
 \		==> f` (LEAST i. f`i = {x}) = {x}";
-by (dresolve_tac [lemma1] 1 THEN (REPEAT (atac 1)));
+by (dresolve_tac [lemma1] 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (AC_cs addSEs [lt_Ord] addIs [LeastI]) 1);
 val lemma2 = result();
 
@@ -462,11 +411,11 @@
 by (REPEAT (eresolve_tac [exE, conjE] 1));
 by (res_inst_tac [("x","a")] exI 1);
 by (res_inst_tac [("x","lam x:y. LEAST i. f`i = {x}")] exI 1);
-by (resolve_tac [conjI] 1 THEN (atac 1));
+by (resolve_tac [conjI] 1 THEN (assume_tac 1));
 by (res_inst_tac [("d","%i. THE x. x:f`i")] lam_injective 1);
-by (dresolve_tac [lemma1] 1 THEN (REPEAT (atac 1)));
+by (dresolve_tac [lemma1] 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (AC_cs addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
-by (resolve_tac [lemma2 RS ssubst] 1 THEN (REPEAT (atac 1)));
+by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (ZF_cs addSIs [the_equality]) 1);
 val NN_imp_ex_inj = result();
 
@@ -495,7 +444,7 @@
 \	!!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |]  \
 \	==> P(1)";
 by (resolve_tac [rev_induct_lemma RS impE] 1);
-by (eresolve_tac [impE] 4 THEN (atac 5));
+by (eresolve_tac [impE] 4 THEN (assume_tac 5));
 by (REPEAT (ares_tac prems 1));
 val rev_induct = result();
 
@@ -505,7 +454,7 @@
 
 goal thy "!!n. [| n:NN(y); y*y <= y; n~=0 |] ==> 1:NN(y)";
 by (resolve_tac [rev_induct] 1 THEN (REPEAT (ares_tac [NN_into_nat] 1)));
-by (resolve_tac [lemma_ii] 1 THEN (REPEAT (atac 1)));
+by (resolve_tac [lemma_ii] 1 THEN REPEAT (assume_tac 1));
 val lemma3 = result();
 
 (* ********************************************************************** *)