src/ZF/AC/WO2_AC16.ML

Numerous small improvements by KG and LCP

(*  Title: 	ZF/AC/WO2_AC16.ML
    ID:         $Id$
    Author: 	Krzysztof Gr`abczewski

  The proof of WO2 ==> AC16(k #+ m, k)
  
  The main part of the proof is the inductive reasoning concerning
  properties of constructed family T_gamma.
  The proof deals with three cases for ordinals: 0, succ and limit ordinal.
  The first instance is trivial, the third not difficult, but the second
  is very complicated requiring many lemmas.
  We also need to prove that at any stage gamma the set 
  (s - Union(...) - k_gamma)   (Rubin & Rubin page 15)
  contains m distinct elements (in fact is equipollent to s)
*)

(* ********************************************************************** *)
(* case of limit ordinal						  *)
(* ********************************************************************** *)

goal thy "!!Z. [| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y)  \
\		--> (EX! Y. Y:F(y) & f(z)<=Y);  \
\		ALL i j. i le j --> F(i) <= F(j); j le i; i<x; z<a;  \
\		V: F(i); f(z)<=V; W:F(j); f(z)<=W |]  \
\		==> V = W";
by (REPEAT (eresolve_tac [asm_rl, allE, impE] 1));
by (dresolve_tac [subsetD] 1 THEN (assume_tac 1));
by (REPEAT (dresolve_tac [ospec] 1 THEN (assume_tac 1)));
by (eresolve_tac [disjI2 RSN (2, impE)] 1);
by (fast_tac (FOL_cs addSIs [bexI]) 1);
by (eresolve_tac [ex1_two_eq] 1 THEN (REPEAT (ares_tac [conjI] 1)));
val lemma3_1 = result();

goal thy "!!Z. [| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y)  \
\		--> (EX! Y. Y:F(y) & f(z)<=Y);  \
\		ALL i j. i le j --> F(i) <= F(j); i<x; j<x; z<a;  \
\		V: F(i); f(z)<=V; W:F(j); f(z)<=W |]  \
\		==> V = W";
by (res_inst_tac [("j","j")] (lt_Ord RS (lt_Ord RSN (2, Ord_linear_le))) 1
	THEN (REPEAT (assume_tac 1)));
by (eresolve_tac [lemma3_1 RS sym] 1 THEN (REPEAT (assume_tac 1)));
by (eresolve_tac [lemma3_1] 1 THEN (REPEAT (assume_tac 1)));
val lemma3 = result();

goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X &  \
\		(ALL x<a. x < y | (EX Y:F(y). fa(x) <= Y) -->  \
\			(EX! Y. Y : F(y) & fa(x) <= Y)); x < a |]  \
\		==> ALL y<x. ALL z<a. z < y | (EX Y:F(y). fa(z) <= Y) -->  \
\			(EX! Y. Y : F(y) & fa(z) <= Y)";
by (REPEAT (resolve_tac [oallI, impI] 1));
by (dresolve_tac [ltD RSN (2, bspec)] 1 THEN (assume_tac 1));
by (eresolve_tac [lt_trans RSN (2, impE)] 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (FOL_cs addSEs [oallE]) 1);
val lemma4 = result();

goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X &  \
\		(ALL x<a. x < y | (EX Y:F(y). fa(x) <= Y) -->  \
\			(EX! Y. Y : F(y) & fa(x) <= Y)); \
\		x < a; Limit(x); ALL i j. i le j --> F(i) <= F(j) |]  \
\		==> (UN x<x. F(x)) <= X &  \
\		(ALL xa<a. xa < x | (EX x:UN x<x. F(x). fa(xa) <= x)  \
\		--> (EX! Y. Y : (UN x<x. F(x)) & fa(xa) <= Y))";
by (resolve_tac [conjI] 1);
by (resolve_tac [subsetI] 1);
by (eresolve_tac [OUN_E] 1);
by (dresolve_tac [ltD RSN (2, bspec)] 1 THEN (assume_tac 1));
by (eresolve_tac [lt_trans RSN (2, impE)] 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac AC_cs 1);
by (dresolve_tac [lemma4] 1 THEN (assume_tac 1));
by (resolve_tac [oallI] 1);
by (resolve_tac [impI] 1);
by (eresolve_tac [disjE] 1);
by (forward_tac [Limit_has_succ RSN (2, ospec)] 1 THEN (REPEAT (assume_tac 1)));
by (dres_inst_tac [("A","a"),("x","xa")] ospec 1 THEN (assume_tac 1));
by (eresolve_tac [lt_Ord RS le_refl RSN (2, disjI1 RSN (2, impE))] 1
	THEN (assume_tac 1));
by (REPEAT (eresolve_tac [ex1E, conjE] 1));
by (resolve_tac [ex1I] 1);
by (resolve_tac [conjI] 1 THEN (assume_tac 2));
by (eresolve_tac [Limit_has_succ RS OUN_I] 1 THEN (TRYALL assume_tac));
by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
by (eresolve_tac [lemma3] 1 THEN (TRYALL assume_tac));
by (eresolve_tac [Limit_has_succ] 1 THEN (assume_tac 1));
by (eresolve_tac [bexE] 1);
by (resolve_tac [ex1I] 1);
by (eresolve_tac [conjI] 1 THEN (assume_tac 1));
by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
by (eresolve_tac [lemma3] 1 THEN (TRYALL assume_tac));
val lemma5 = result();

(* ********************************************************************** *)
(* case of successor ordinal						  *)
(* ********************************************************************** *)

(*
  First quite complicated proof of the fact used in the recursive construction
  of the family T_gamma (WO2 ==> AC16(k #+ m, k)) - the fact that at any stage
  gamma the set (s - Union(...) - k_gamma) is equipollent to s
  (Rubin & Rubin page 15).
*)

(* ********************************************************************** *)
(* dbl_Diff_eqpoll_Card							  *)
(* ********************************************************************** *)

goal thy "!!A. [| A eqpoll a; Card(a); ~Finite(a); B lesspoll a;  \
\	C lesspoll a |] ==> A - B - C eqpoll a";
by (resolve_tac [Diff_lesspoll_eqpoll_Card] 1 THEN (REPEAT (assume_tac 1)));
by (resolve_tac [Diff_lesspoll_eqpoll_Card] 1 THEN (REPEAT (assume_tac 1)));
val dbl_Diff_eqpoll_Card = result();

(* ********************************************************************** *)
(* Case of finite ordinals						  *)
(* ********************************************************************** *)

goalw thy [lesspoll_def]
	"!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a";
by (resolve_tac [conjI] 1);
by (dresolve_tac [nat_le_infinite_Ord RS le_imp_lepoll] 1
	THEN (assume_tac 1));
by (rewrite_goals_tac [Finite_def]);
by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_trans]) 2);
by (resolve_tac [lepoll_trans] 1 THEN (assume_tac 2));
by (fast_tac (AC_cs addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_subset RS 
	subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1);
val Finite_lesspoll_infinite_Ord = result();

goal thy "!!x. x:X ==> Union(X) = Union(X-{x}) Un x";
by (fast_tac (AC_cs addIs [equalityI] addSIs [singletonI]
		addSEs [singletonE]) 1);
val Union_eq_Un_Diff = result();

goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x))  \
\	--> Finite(Union(X))";
by (eresolve_tac [nat_induct] 1);
by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]
	addSIs [nat_0I RS nat_into_Finite] addIs [Union_0 RS ssubst]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1));
by (res_inst_tac [("P","%z. Finite(z)")] (Union_eq_Un_Diff RS ssubst) 1
	THEN (assume_tac 1));
by (resolve_tac [Finite_Un] 1);
by (fast_tac AC_cs 2);
by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll]) 1);
val Finite_Union_lemma = result();

goal thy "!!X. [| ALL x:X. Finite(x); Finite(X) |] ==> Finite(Union(X))";
by (eresolve_tac [Finite_def RS def_imp_iff RS iffD1 RS bexE] 1);
by (dresolve_tac [Finite_Union_lemma] 1);
by (fast_tac AC_cs 1);
val Finite_Union = result();

goalw thy [Finite_def] "!!x. [| x lepoll n; n:nat |] ==> Finite(x)";
by (fast_tac (AC_cs
	addEs [nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll) RS exE,
	Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD]) 1);
val lepoll_nat_num_imp_Finite = result();

goal thy "!!X. [| ALL x:X. x lepoll n & x <= T; well_ord(T, R); X lepoll b;  \
\	b<a; ~Finite(a); Card(a); n:nat |]  \
\	==> Union(X) lesspoll a";
by (excluded_middle_tac "Finite(X)" 1);
by (resolve_tac [Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord)] 2
	THEN (REPEAT (assume_tac 3)));
by (fast_tac (AC_cs addSEs [lepoll_nat_num_imp_Finite]
		addSIs [Finite_Union]) 2);
by (dresolve_tac [lt_Ord RSN (2, lepoll_imp_ex_le_eqpoll)] 1 THEN (assume_tac 1));
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1));
by (eresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1) RS
		exE] 1);
by (forward_tac [bij_is_surj RS surj_image_eq] 1);
by (dresolve_tac [[bij_is_fun, subset_refl] MRS image_fun] 1);
by (dresolve_tac [sym RS trans] 1 THEN (assume_tac 1));
by (hyp_subst_tac 1);
by (resolve_tac [lepoll_lesspoll_lesspoll] 1);
by (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1
	THEN REPEAT (assume_tac 1));
by (resolve_tac [UN_lepoll] 1
	THEN (TRYALL (fast_tac (AC_cs addSEs [lt_Ord]))));
val Union_lesspoll = result();

(* ********************************************************************** *)
(* recfunAC16_lepoll_index						  *)
(* ********************************************************************** *)

goal thy "A Un {a} = cons(a, A)";
by (fast_tac (AC_cs addSIs [singletonI]
		addSEs [singletonE] addIs [equalityI]) 1);
val Un_sing_eq_cons = result();

goal thy "!!A. A lepoll B ==> A Un {a} lepoll succ(B)";
by (asm_simp_tac (AC_ss addsimps [Un_sing_eq_cons, succ_def]) 1);
by (eresolve_tac [mem_not_refl RSN (2, cons_lepoll_cong)] 1);
val Un_lepoll_succ = result();

goal thy "!!a. Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0";
by (fast_tac (AC_cs addSIs [OUN_I, le_refl] addIs [equalityI]) 1);
val Diff_UN_succ_empty = result();

goal thy "!!a. Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X";
by (fast_tac (AC_cs addSIs [OUN_I, le_refl]) 1);
val Diff_UN_succ_subset = result();

goal thy "!!x. Ord(x) ==>  \
\	recfunAC16(f, g, x, a) - (UN i<x. recfunAC16(f, g, i, a)) lepoll 1";
by (eresolve_tac [Ord_cases] 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0,
		empty_subsetI RS subset_imp_lepoll]) 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit,
		Diff_cancel, empty_subsetI RS subset_imp_lepoll]) 2);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1);
by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
by (fast_tac (AC_cs addSIs [empty_subsetI RS subset_imp_lepoll]
		addSEs [Diff_UN_succ_empty RS ssubst]) 1);
by (fast_tac (AC_cs addSEs [Diff_UN_succ_subset RS subset_imp_lepoll RS
	(singleton_eqpoll_1 RS eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1);
val recfunAC16_Diff_lepoll_1 = result();

goal thy "!!z. [| z : F(x); Ord(x) |]  \
\	==> z:F(LEAST i. z:F(i)) - (UN j<(LEAST i. z:F(i)). F(j))";
by (fast_tac (AC_cs addEs [less_LeastE] addSEs [OUN_E, LeastI]) 1);
val in_Least_Diff = result();

goal thy "!!w. [| (LEAST i. w:F(i)) = (LEAST i. z:F(i));  \
\	w:(UN i<a. F(i)); z:(UN i<a. F(i)) |]  \
\	==> EX b<a. w:(F(b) - (UN c<b. F(c))) & z:(F(b) - (UN c<b. F(c)))";
by (REPEAT (eresolve_tac [OUN_E] 1));
by (dresolve_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1));
by (forward_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1));
by (resolve_tac [oexI] 1);
by (resolve_tac [conjI] 1 THEN (assume_tac 2));
by (eresolve_tac [subst] 1 THEN (assume_tac 1));
by (eresolve_tac [lt_Ord RSN (2, Least_le) RS lt_trans1] 1
	THEN (REPEAT (assume_tac 1)));
val Least_eq_imp_ex = result();

goal thy "!!A. [| A lepoll 1; a:A; b:A |] ==> a=b";
by (fast_tac (AC_cs addSDs [lepoll_1_is_sing] addSEs [singletonE]) 1);
val two_in_lepoll_1 = result();

goal thy "!!a. [| ALL i<a. F(i)-(UN j<i. F(j)) lepoll 1; Limit(a) |]  \
\	==> (UN x<a. F(x)) lepoll a";
by (resolve_tac [lepoll_def RS (def_imp_iff RS iffD2)] 1);
by (res_inst_tac [("x","lam z: (UN x<a. F(x)). LEAST i. z:F(i)")] exI 1);
by (rewrite_goals_tac [inj_def]);
by (resolve_tac [CollectI] 1);
by (resolve_tac [lam_type] 1);
by (eresolve_tac [OUN_E] 1);
by (eresolve_tac [Least_in_Ord] 1);
by (eresolve_tac [ltD] 1);
by (eresolve_tac [lt_Ord2] 1);
by (resolve_tac [ballI] 1);
by (resolve_tac [ballI] 1);
by (asm_simp_tac AC_ss 1);
by (resolve_tac [impI] 1);
by (dresolve_tac [Least_eq_imp_ex] 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (AC_cs addSEs [two_in_lepoll_1]) 1);
val UN_lepoll_index = result();

goal thy "!!y. Ord(y) ==> recfunAC16(f, fa, y, a) lepoll y";
by (eresolve_tac [trans_induct] 1);
by (eresolve_tac [Ord_cases] 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0, lepoll_refl]) 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1);
by (fast_tac (AC_cs addIs [conjI RS (expand_if RS iffD2)]
	addSDs [succI1 RSN (2, bspec)]
	addSEs [subset_succI RS subset_imp_lepoll RSN (2, lepoll_trans),
		Un_lepoll_succ]) 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 1);
by (fast_tac (AC_cs addSEs [lt_Ord RS recfunAC16_Diff_lepoll_1]
	addSIs [UN_lepoll_index]) 1);
val recfunAC16_lepoll_index = result();

goal thy "!!y. [| recfunAC16(f,g,y,a) <= {X: Pow(A). X eqpoll n};  \
\		A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |]  \
\		==> Union(recfunAC16(f,g,y,a)) lesspoll a";
by (eresolve_tac [eqpoll_def RS def_imp_iff RS iffD1 RS exE] 1);
by (resolve_tac [Union_lesspoll] 1 THEN (TRYALL assume_tac));
by (eresolve_tac [lt_Ord RS recfunAC16_lepoll_index] 3);
by (eresolve_tac [[bij_is_inj, Card_is_Ord RS well_ord_Memrel] MRS
	well_ord_rvimage] 2 THEN (assume_tac 2));
by (fast_tac (AC_cs addSEs [eqpoll_imp_lepoll]) 1);
val Union_recfunAC16_lesspoll = result();

goal thy
  "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
\	Card(a); ~ Finite(a); A eqpoll a;  \
\	k : nat; m : nat; y<a;  \
\	fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |]  \
\	==> A - Union(recfunAC16(f, fa, y, a)) - fa`y eqpoll a";
by (resolve_tac [dbl_Diff_eqpoll_Card] 1 THEN (TRYALL assume_tac));
by (resolve_tac [Union_recfunAC16_lesspoll] 1 THEN (REPEAT (assume_tac 1)));
by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1));
by (resolve_tac [nat_succI RSN (2, bexI RS (Finite_def RS def_imp_iff RS
	iffD2)) RS (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1
	THEN (TRYALL assume_tac));
by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type) RS CollectE] 1
	THEN (TRYALL assume_tac));
val dbl_Diff_eqpoll = result();

(* back to the proof *)

val disj_Un_eqpoll_nat_sum = disj_Un_eqpoll_sum RS (
                             sum_eqpoll_cong RSN (2, 
                             nat_sum_eqpoll_sum RSN (3, 
                             eqpoll_trans RS eqpoll_trans))) |> standard;

goal thy "!!x. [| x : Pow(A - B - fa`i); x eqpoll m;  \
\	fa : bij(a, {x: Pow(A) . x eqpoll k}); i<a; k:nat; m:nat |]  \
\	==> fa ` i Un x : {x: Pow(A) . x eqpoll k #+ m}";
by (resolve_tac [CollectI] 1);
by (fast_tac (AC_cs addSIs [PowD RS (PowD RSN (2, Un_least RS PowI))] 
	addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1);
by (resolve_tac [disj_Un_eqpoll_nat_sum] 1
	THEN (TRYALL assume_tac));
by (fast_tac (AC_cs addSIs [equals0I]) 1);
by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)] 1
	THEN (REPEAT (assume_tac 1)));
val Un_in_Collect = result();

(* ********************************************************************** *)
(* Lemmas simplifying assumptions					  *)
(* ********************************************************************** *)

goal thy "!!j. [| ALL y:succ(j). y<a --> F(y)<=X & (ALL x<a. x<y | P(x,y)  \
\	--> Q(x,y)); succ(j)<a |]  \
\	==> F(j)<=X & (ALL x<a. x<j | P(x,j) --> Q(x,j))";
by (dresolve_tac [succI1 RSN (2, bspec)] 1);
by (eresolve_tac [impE] 1);
by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl) RS lt_trans] 1
	THEN (REPEAT (assume_tac 1)));
val lemma6 = result();

goal thy "!!j. [| F(j)<=X; (ALL x<a. x<j | P(x,j) --> Q(x,j)); succ(j)<a |]  \
\	==> P(j,j) --> F(j) <= X & (ALL x<a. x le j | P(x,j) --> Q(x,j))";
by (fast_tac (AC_cs addSEs [leE]) 1);
val lemma7 = result();

(* ********************************************************************** *)
(* Lemmas needded to prove ex_next_set which means that for any successor *)
(* ordinal there is a set satisfying certain properties			  *)
(* ********************************************************************** *)

goal thy "!!A. [| A eqpoll a; ~ Finite(a); Ord(a); m:nat |]  \
\	==> EX X:Pow(A). X eqpoll m";
by (eresolve_tac [Ord_nat RSN (2, ltI) RS 
		(nat_le_infinite_Ord RSN (2, lt_trans2)) RS 
		leI RS le_imp_lepoll RS 
		((eqpoll_sym RS eqpoll_imp_lepoll) RSN (2, lepoll_trans)) RS 
		lepoll_imp_eqpoll_subset RS exE] 1 
	THEN REPEAT (assume_tac 1));
by (fast_tac (AC_cs addSEs [eqpoll_sym]) 1);
val ex_subset_eqpoll = result();

goal thy "!!A. [| A <= B Un C; A Int C = 0 |] ==> A <= B";
by (fast_tac (AC_cs addDs [equals0D]) 1);
val subset_Un_disjoint = result();

goal thy "!!F. [| X:Pow(A - Union(B) -C); T:B; F<=T |] ==> F Int X = 0";
by (fast_tac (AC_cs addSIs [equals0I]) 1);
val Int_empty = result();

(* ********************************************************************** *)
(* equipollent subset (and finite) is the whole set			  *)
(* ********************************************************************** *)

goal thy "!!A. [| A <= B; a : A; A - {a} = B - {a} |] ==> A = B";
by (fast_tac (AC_cs addSEs [equalityE, singletonE]
		addSIs [equalityI, singletonI]) 1);
val Diffs_eq_imp_eq = result();

goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
by (eresolve_tac [nat_induct] 1);
by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
by (REPEAT (eresolve_tac [conjE] 1));
by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1
	THEN (assume_tac 1));
by (forward_tac [subsetD RS Diff_sing_lepoll] 1
	THEN REPEAT (assume_tac 1));
by (forward_tac [lepoll_Diff_sing] 1);
by (REPEAT (eresolve_tac [allE, impE] 1));
by (resolve_tac [conjI] 1);
by (fast_tac AC_cs 2);
by (fast_tac (AC_cs addSEs [singletonE] addSIs [singletonI]) 1);
by (eresolve_tac [Diffs_eq_imp_eq] 1
	THEN REPEAT (assume_tac 1));
val subset_imp_eq_lemma = result();

goal thy "!!A. [| A <= B; m lepoll A; B lepoll m; m:nat |] ==> A=B";
by (fast_tac (FOL_cs addSDs [subset_imp_eq_lemma]) 1);
val subset_imp_eq = result();

goal thy "!!f. [| f:bij(a, {Y:X. Y eqpoll succ(k)}); k:nat; f`b<=f`y; b<a;  \
\	y<a |] ==> b=y";
by (dresolve_tac [subset_imp_eq] 1);
by (eresolve_tac [nat_succI] 3);
by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS
		CollectE, eqpoll_sym RS eqpoll_imp_lepoll]) 1);
by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS
	CollectE, eqpoll_imp_lepoll]) 1);
by (rewrite_goals_tac [bij_def, inj_def]);
by (fast_tac (AC_cs addSDs [ltD]) 1);
val bij_imp_arg_eq = result();

goal thy
  "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
\	Card(a); ~ Finite(a); A eqpoll a;  \
\	k : nat; m : nat; y<a;  \
\	fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)});  \
\	~ (EX Y:recfunAC16(f, fa, y, a). fa`y <= Y) |]  \
\	==> EX X:{Y: Pow(A). Y eqpoll succ(k #+ m)}. fa`y <= X &  \
\		(ALL b<a. fa`b <= X -->  \
\		(ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))";
by (eresolve_tac [dbl_Diff_eqpoll RS ex_subset_eqpoll RS bexE] 1
	THEN REPEAT (assume_tac 1));
by (eresolve_tac [Card_is_Ord] 1);
by (forward_tac [Un_in_Collect] 2 THEN REPEAT (assume_tac 2));
by (eresolve_tac [CollectE] 4);
by (resolve_tac [bexI] 4);
by (resolve_tac [CollectI] 5);
by (assume_tac 5);
by (eresolve_tac [add_succ RS subst] 5);
by (assume_tac 1);
by (eresolve_tac [nat_succI] 1);
by (assume_tac 1);
by (resolve_tac [conjI] 1);
by (fast_tac AC_cs 1);
by (REPEAT (resolve_tac [ballI, impI, oallI, notI] 1));
by (dresolve_tac [Int_empty RSN (2, subset_Un_disjoint)] 1
	THEN REPEAT (assume_tac 1));
by (dresolve_tac [bij_imp_arg_eq] 1 THEN REPEAT (assume_tac 1));
by (hyp_subst_tac 1);
by (eresolve_tac [bexI RSN (2, notE)] 1 THEN TRYALL assume_tac);
val ex_next_set = result();

(* ********************************************************************** *)
(* Lemma ex_next_Ord states that for any successor			  *)
(* ordinal there is a number of the set satisfying certain properties	  *)
(* ********************************************************************** *)

goal thy
  "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
\	Card(a); ~ Finite(a); A eqpoll a;  \
\	k : nat; m : nat; y<a;  \
\	fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)});  \
\	f : bij(a, {Y: Pow(A). Y eqpoll succ(k #+ m)});  \
\	~ (EX Y:recfunAC16(f, fa, y, a). fa`y <= Y) |]  \
\	==> EX c<a. fa`y <= f`c &  \
\		(ALL b<a. fa`b <= f`c -->  \
\		(ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))";
by (dresolve_tac [ex_next_set] 1 THEN REPEAT (assume_tac 1));
by (eresolve_tac [bexE] 1);
by (resolve_tac [bij_converse_bij RS bij_is_fun RS apply_type RS ltI RSN
	(2, oexI)] 1);
by (resolve_tac [right_inverse_bij RS ssubst] 1
	THEN REPEAT (ares_tac [Card_is_Ord] 1));
val ex_next_Ord = result();

goal thy "!!Z. [| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y:Z Un {W} & P(Y)";
by (fast_tac (AC_cs addSEs [singletonE]) 1);
val ex1_in_Un_sing = result();

(* ********************************************************************** *)
(* Lemma simplifying assumptions					  *)
(* ********************************************************************** *)

goal thy "!!j. [| ALL x<a. x<j | (EX xa:F(j). P(x, xa))  \
\	--> (EX! Y. Y:F(j) & P(x, Y)); F(j) <= X;  \
\	L : X; P(j, L) & (ALL x<a. P(x, L) --> (ALL xa:F(j). ~P(x, xa))) |]  \
\	==> F(j) Un {L} <= X &  \
\	(ALL x<a. x le j | (EX xa:F(j) Un {L}. P(x, xa)) -->  \
\		(EX! Y. Y:F(j) Un {L} & P(x, Y)))";
by (resolve_tac [conjI] 1);
by (fast_tac (AC_cs addSIs [singleton_subsetI]) 1);
by (resolve_tac [oallI] 1);
by (eresolve_tac [oallE] 1 THEN (contr_tac 2));
by (resolve_tac [impI] 1);
by (eresolve_tac [disjE] 1);
by (eresolve_tac [leE] 1);
by (eresolve_tac [disjI1 RSN (2, impE)] 1 THEN (assume_tac 1));
by (resolve_tac [ex1E] 1 THEN (assume_tac 1));
by (eresolve_tac [ex1_in_Un_sing] 1);
by (fast_tac AC_cs 1);
by (fast_tac AC_cs 1);
by (eresolve_tac [bexE] 1);
by (eresolve_tac [UnE] 1);
by (fast_tac (AC_cs addSEs [ex1_in_Un_sing]) 1);
by (fast_tac AC_cs 1);
val lemma8 = result();

(* ********************************************************************** *)
(* The main part of the proof: inductive proof of the property of T_gamma *)
(* lemma main_induct							  *)
(* ********************************************************************** *)

goal thy
	"!!a. [| b < a; f : bij(a, {Y: Pow(A) . Y eqpoll succ(k #+ m)});  \
\	fa : bij(a, {Y: Pow(A) . Y eqpoll succ(k)});  \
\	~Finite(a); Card(a); A eqpoll a; k : nat; m : nat |]  \
\	==> recfunAC16(f, fa, b, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)} &  \
\	(ALL x<a. x < b | (EX Y:recfunAC16(f, fa, b, a). fa ` x <= Y) -->  \
\	(EX! Y. Y:recfunAC16(f, fa, b, a) & fa ` x <= Y))";
by (resolve_tac [impE] 1 THEN (REPEAT (assume_tac 2)));
by (eresolve_tac [lt_Ord RS trans_induct] 1);
by (resolve_tac [impI] 1);
by (eresolve_tac [Ord_cases] 1);
(* case 0 *)
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0]) 1);
by (fast_tac (AC_cs addSEs [ltE]) 1);
(* case Limit *)
by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 2);
by (eresolve_tac [lemma5] 2 THEN (REPEAT (assume_tac 2)));
by (fast_tac (FOL_cs addSEs [recfunAC16_mono]) 2);
(* case succ *)
by (hyp_subst_tac 1);
by (eresolve_tac [lemma6 RS conjE] 1 THEN (assume_tac 1));
by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1);
by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
by (eresolve_tac [lemma7] 1 THEN (REPEAT (assume_tac 1)));
by (resolve_tac [impI] 1);
by (resolve_tac [ex_next_Ord RS oexE] 1 
	THEN REPEAT (ares_tac [le_refl RS lt_trans] 1));
by (eresolve_tac [lemma8] 1 THEN (assume_tac 1));
by (resolve_tac [bij_is_fun RS apply_type] 1 THEN (assume_tac 1));
by (eresolve_tac [Least_le RS lt_trans2 RS ltD] 1 
	THEN REPEAT (ares_tac [lt_Ord, succ_leI] 1));
by (eresolve_tac [lt_Ord RSN (2, LeastI)] 1 THEN (assume_tac 1));
val main_induct = result();

(* ********************************************************************** *)
(* Lemma to simplify the inductive proof				  *)
(*   - the disired property is a consequence of the inductive assumption  *)
(* ********************************************************************** *)

val [prem1, prem2, prem3, prem4] = goal thy
	"[| (!!b. b<a ==> F(b) <= S & (ALL x<a. (x<b | (EX Y:F(b). f`x <= Y)) \
\	--> (EX! Y. Y : F(b) & f`x <= Y)));  \
\	f:a->f``(a); Limit(a); (!!i j. i le j ==> F(i) <= F(j)) |]  \
\	==> (UN j<a. F(j)) <= S &  \
\	(ALL x:f``a. EX! Y. Y : (UN j<a. F(j)) & x <= Y)";
by (resolve_tac [conjI] 1);
by (resolve_tac [subsetI] 1);
by (eresolve_tac [OUN_E] 1);
by (dresolve_tac [prem1] 1);
by (fast_tac AC_cs 1);
by (resolve_tac [ballI] 1);
by (eresolve_tac [imageE] 1);
by (dresolve_tac [prem3 RS Limit_is_Ord RSN (2, ltI) RS
	(prem3 RS Limit_has_succ)] 1);
by (forward_tac [prem1] 1);
by (eresolve_tac [conjE] 1);
by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1));
by (eresolve_tac [impE] 1);
by (fast_tac (AC_cs addSEs [leI RS succ_leE RS lt_Ord RS le_refl]) 1);
by (dresolve_tac [prem2 RSN (2, apply_equality)] 1);
by (REPEAT (eresolve_tac [conjE, ex1E] 1));
by (resolve_tac [ex1I] 1);
by (fast_tac (AC_cs addSIs [OUN_I]) 1);
by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
by (eresolve_tac [lt_Ord RSN (2, lt_Ord RS Ord_linear_le)] 1 THEN (assume_tac 1));
by (dresolve_tac [prem4 RS subsetD] 2 THEN (assume_tac 2));
by (fast_tac AC_cs 2);
by (forward_tac [prem1] 1);
by (forward_tac [succ_leE] 1);
by (dresolve_tac [prem4 RS subsetD] 1 THEN (assume_tac 1));
by (eresolve_tac [conjE] 1);
by (dresolve_tac [lt_trans RSN (2, ospec)] 1 THEN (TRYALL assume_tac));
by (dresolve_tac [disjI1 RSN (2, mp)] 1 THEN (assume_tac 1));
by (eresolve_tac [ex1_two_eq] 1);
by (REPEAT (fast_tac AC_cs 1));
val lemma_simp_induct = result();

(* ********************************************************************** *)
(* The target theorem							  *)
(* ********************************************************************** *)

goalw thy [AC16_def]
	"!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
by (resolve_tac [allI] 1);
by (resolve_tac [impI] 1);
by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 THEN (REPEAT (assume_tac 1)));
by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1
	THEN (REPEAT (ares_tac [add_type] 1)));
by (forward_tac [WO2_imp_ex_Card] 1);
by (REPEAT (eresolve_tac [exE,conjE] 1));
by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS
	def_imp_iff RS iffD1)] 1 THEN (assume_tac 1));
by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS
	def_imp_iff RS iffD1)] 1 THEN (assume_tac 1));
by (REPEAT (eresolve_tac [exE] 1));
by (res_inst_tac [("x","UN j<a. recfunAC16(fa,f,j,a)")] exI 1);
by (res_inst_tac [("P","%z. ?Y & (ALL x:z. ?Z(x))")] 
	(bij_is_surj RS surj_image_eq RS subst) 1
	THEN (assume_tac 1));
by (resolve_tac [lemma_simp_induct] 1);
by (eresolve_tac [bij_is_fun RS surj_image RS surj_is_fun] 2);
by (eresolve_tac [eqpoll_imp_lepoll RS lepoll_infinite RS
	infinite_Card_is_InfCard RS InfCard_is_Limit] 2 
	THEN REPEAT (assume_tac 2));
by (eresolve_tac [recfunAC16_mono] 2);
by (resolve_tac [main_induct] 1 
	THEN REPEAT (ares_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1));
qed "WO2_AC16";