src/ZF/AC/WO2_AC16.ML

Renamed equals0D to equals0E; tidied

(*  Title:      ZF/AC/WO2_AC16.ML
    ID:         $Id$
    Author:     Krzysztof Grabczewski

  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 "[| 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 (dtac subsetD 1 THEN (assume_tac 1));
by (REPEAT (dtac ospec 1 THEN (assume_tac 1)));
by (eresolve_tac [disjI2 RSN (2, impE)] 1);
by (fast_tac (FOL_cs addSIs [bexI]) 1);
by (etac ex1_two_eq 1 THEN (REPEAT (ares_tac [conjI] 1)));
val lemma3_1 = result();


Goal "[| 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 (etac lemma3_1 1 THEN (REPEAT (assume_tac 1)));
val lemma3 = result();


Goal "[| ALL y<x. 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 (dtac ospec 1 THEN (assume_tac 1));
by (fast_tac (FOL_cs addSEs [oallE]) 1);
val lemma4 = result();


Goal "[| ALL y<x. 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 (rtac conjI 1);
by (rtac subsetI 1);
by (etac OUN_E 1);
by (dtac ospec 1 THEN (assume_tac 1));
by (Fast_tac 1);
by (dtac lemma4 1 THEN (assume_tac 1));
by (rtac oallI 1);
by (rtac impI 1);
by (etac 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 (rtac ex1I 1);
by (rtac 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 (etac lemma3 1 THEN (TRYALL assume_tac));
by (etac Limit_has_succ 1 THEN (assume_tac 1));
by (etac bexE 1);
by (rtac ex1I 1);
by (etac conjI 1 THEN (assume_tac 1));
by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
by (etac 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 "[| A eqpoll a; Card(a); ~Finite(a); B lesspoll a;  \
\       C lesspoll a |] ==> A - B - C eqpoll a";
by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1)));
by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1)));
qed "dbl_Diff_eqpoll_Card";

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


Goalw [lesspoll_def]
        "!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a";
by (rtac conjI 1);
by (dresolve_tac [nat_le_infinite_Ord RS le_imp_lepoll] 1
        THEN (assume_tac 1));
by (rewtac Finite_def);
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_trans]) 2);
by (rtac lepoll_trans 1 THEN (assume_tac 2));
by (fast_tac (claset() 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);
qed "Finite_lesspoll_infinite_Ord";


Goal "x:X ==> Union(X) = Union(X-{x}) Un x";
by (Fast_tac 1);
qed "Union_eq_Un_Diff";


Goal "n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x))  \
\       --> Finite(Union(X))";
by (etac nat_induct 1);
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]
        addSIs [nat_0I RS nat_into_Finite] addss (simpset())) 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 (rtac Finite_Un 1);
by (Fast_tac 2);
by (fast_tac (claset() addSIs [Diff_sing_eqpoll]) 1);
qed "Finite_Union_lemma";


Goal "[| 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 (dtac Finite_Union_lemma 1);
by (Fast_tac 1);
qed "Finite_Union";


Goalw [Finite_def] "[| x lepoll n; n:nat |] ==> Finite(x)";
by (fast_tac (claset()
        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);
qed "lepoll_nat_num_imp_Finite";


Goal "[| 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 (claset() 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 (rtac lepoll_lesspoll_lesspoll 1);
by (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1
        THEN REPEAT (assume_tac 1));
by (rtac UN_lepoll 1
        THEN (TRYALL (fast_tac (claset() addSEs [lt_Ord]))));
qed "Union_lesspoll";

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


Goal "A Un {a} = cons(a, A)";
by (Fast_tac 1);
qed "Un_sing_eq_cons";


Goal "A lepoll B ==> A Un {a} lepoll succ(B)";
by (asm_simp_tac (simpset() addsimps [Un_sing_eq_cons, succ_def]) 1);
by (eresolve_tac [mem_not_refl RSN (2, cons_lepoll_cong)] 1);
qed "Un_lepoll_succ";


Goal "Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0";
by (fast_tac (claset() addSIs [OUN_I, le_refl]) 1);
qed "Diff_UN_succ_empty";


Goal "Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X";
by (fast_tac (claset() addSIs [OUN_I, le_refl]) 1);
qed "Diff_UN_succ_subset";


Goal "Ord(x) ==>  \
\       recfunAC16(f, g, x, a) - (UN i<x. recfunAC16(f, g, i, a)) lepoll 1";
by (etac Ord_cases 1);
by (asm_simp_tac (simpset() addsimps [recfunAC16_0,
				      empty_subsetI RS subset_imp_lepoll]) 1);
by (asm_simp_tac (simpset() addsimps [recfunAC16_Limit, Diff_cancel, 
				      empty_subsetI RS subset_imp_lepoll]) 2);
by (asm_simp_tac (simpset() addsimps [recfunAC16_succ]) 1);
by (rtac conjI 1);
by (fast_tac (claset() addSIs [empty_subsetI RS subset_imp_lepoll]
                      addSEs [Diff_UN_succ_empty RS ssubst]) 1);
by (fast_tac (claset() addSEs [Diff_UN_succ_subset RS subset_imp_lepoll RS
        (singleton_eqpoll_1 RS eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1);
qed "recfunAC16_Diff_lepoll_1";


Goal "[| z : F(x); Ord(x) |]  \
\       ==> z:F(LEAST i. z:F(i)) - (UN j<(LEAST i. z:F(i)). F(j))";
by (fast_tac (claset() addEs [less_LeastE] addSEs [OUN_E, LeastI]) 1);
qed "in_Least_Diff";


Goal "[| (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 (etac 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 (rtac oexI 1);
by (rtac conjI 1 THEN (assume_tac 2));
by (etac subst 1 THEN (assume_tac 1));
by (eresolve_tac [lt_Ord RSN (2, Least_le) RS lt_trans1] 1
        THEN (REPEAT (assume_tac 1)));
qed "Least_eq_imp_ex";


Goal "[| A lepoll 1; a:A; b:A |] ==> a=b";
by (fast_tac (claset() addSDs [lepoll_1_is_sing]) 1);
qed "two_in_lepoll_1";


Goal "[| 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 (rewtac inj_def);
by (rtac CollectI 1);
by (rtac lam_type 1);
by (etac OUN_E 1);
by (etac Least_in_Ord 1);
by (etac ltD 1);
by (etac lt_Ord2 1);
by (rtac ballI 1);
by (rtac ballI 1);
by (Asm_simp_tac 1);
by (rtac impI 1);
by (dtac Least_eq_imp_ex 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (claset() addSEs [two_in_lepoll_1]) 1);
qed "UN_lepoll_index";


Goal "Ord(y) ==> recfunAC16(f, fa, y, a) lepoll y";
by (etac trans_induct 1);
by (etac Ord_cases 1);
by (asm_simp_tac (simpset() addsimps [recfunAC16_0, lepoll_refl]) 1);
by (asm_simp_tac (simpset() addsimps [recfunAC16_succ]) 1);
by (fast_tac (claset() 
        addSDs [succI1 RSN (2, bspec)]
        addSEs [subset_succI RS subset_imp_lepoll RSN (2, lepoll_trans),
                Un_lepoll_succ]) 1);
by (asm_simp_tac (simpset() addsimps [recfunAC16_Limit]) 1);
by (fast_tac (claset() addSEs [lt_Ord RS recfunAC16_Diff_lepoll_1]
                       addSIs [UN_lepoll_index]) 1);
qed "recfunAC16_lepoll_index";


Goal "[| 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 (rtac 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 (claset() addSEs [eqpoll_imp_lepoll]) 1);
qed "Union_recfunAC16_lesspoll";


Goal
  "!!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 (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac));
by (rtac 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));
qed "dbl_Diff_eqpoll";

(* 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 "[| 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 (rtac CollectI 1);
by (fast_tac (claset() addSIs [PowD RS (PowD RSN (2, Un_least RS PowI))] 
        addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1);
by (rtac disj_Un_eqpoll_nat_sum 1
        THEN (TRYALL assume_tac));
by (fast_tac (claset() addSIs [equals0I]) 1);
by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)] 1
        THEN (REPEAT (assume_tac 1)));
qed "Un_in_Collect";

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


Goal "[| ALL y<succ(j). 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 (dtac ospec 1);
by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl)] 1
        THEN (REPEAT (assume_tac 1)));
val lemma6 = result();


Goal "[| ALL x<a. x<j | P(x,j) --> Q(x,j);  succ(j)<a |]  \
\     ==> P(j,j) --> (ALL x<a. x le j | P(x,j) --> Q(x,j))";
by (fast_tac (claset() 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 "[| 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 (claset() addSEs [eqpoll_sym]) 1);
qed "ex_subset_eqpoll";


Goal "[| A <= B Un C; A Int C = 0 |] ==> A <= B";
by (fast_tac (claset() addEs [equals0E]) 1);
qed "subset_Un_disjoint";


Goal "[| X:Pow(A - Union(B) -C); T:B; F<=T |] ==> F Int X = 0";
by (fast_tac (claset() addSIs [equals0I]) 1);
qed "Int_empty";

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


Goal "[| A <= B; a : A; A - {a} = B - {a} |] ==> A = B";
by (fast_tac (claset() addSEs [equalityE]) 1);
qed "Diffs_eq_imp_eq";


Goal "m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
by (etac nat_induct 1);
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
by (REPEAT (etac 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 (rtac conjI 1);
by (Fast_tac 2);
by (Fast_tac 1);
by (etac Diffs_eq_imp_eq 1
        THEN REPEAT (assume_tac 1));
qed "subset_imp_eq_lemma";


Goal "[| A <= B; m lepoll A; B lepoll m; m:nat |] ==> A=B";
by (fast_tac (FOL_cs addSDs [subset_imp_eq_lemma]) 1);
qed "subset_imp_eq";


Goal "[| f:bij(a, {Y:X. Y eqpoll succ(k)}); k:nat; f`b<=f`y; b<a;  \
\       y<a |] ==> b=y";
by (dtac subset_imp_eq 1);
by (etac nat_succI 3);
by (fast_tac (claset() addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS
                CollectE, eqpoll_sym RS eqpoll_imp_lepoll]) 1);
by (fast_tac (claset() 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 (claset() addSDs [ltD]) 1);
qed "bij_imp_arg_eq";


Goal
  "!!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 (etac Card_is_Ord 1);
by (forward_tac [Un_in_Collect] 2 THEN REPEAT (assume_tac 2));
by (etac CollectE 4);
by (rtac bexI 4);
by (rtac CollectI 5);
by (assume_tac 5);
by (eresolve_tac [add_succ RS subst] 5);
by (assume_tac 1);
by (etac nat_succI 1);
by (assume_tac 1);
by (rtac conjI 1);
by (Fast_tac 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 (dtac 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);
qed "ex_next_set";

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


Goal
  "!!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 (dtac ex_next_set 1 THEN REPEAT (assume_tac 1));
by (etac 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));
qed "ex_next_Ord";


Goal "[| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y: (Z Un {W}) & P(Y)";
by (Fast_tac 1);
qed "ex1_in_Un_sing";

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


Goal "[| 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 (rtac conjI 1);
by (fast_tac (claset() addSIs [singleton_subsetI]) 1);
by (rtac oallI 1);
by (etac oallE 1 THEN (contr_tac 2));
by (blast_tac (claset() addSEs [leE]) 1);
val lemma8 = result();

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


Goal "[| 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 (etac lt_induct 1);
by (forward_tac [lt_Ord] 1);
by (etac Ord_cases 1);
(* case 0 *)
by (asm_simp_tac (simpset() addsimps [recfunAC16_0]) 1);
(* case Limit *)
by (asm_simp_tac (simpset() addsimps [recfunAC16_Limit]) 2);
by (rtac 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 (simpset() delsplits [split_if]
			    addsimps [recfunAC16_succ]) 1);
by (resolve_tac [conjI RS (split_if RS iffD2)] 1);
by (Asm_simp_tac 1);
by (etac lemma7 1 THEN  assume_tac 1);
by (rtac impI 1);
by (resolve_tac [ex_next_Ord RS oexE] 1 
    THEN REPEAT (ares_tac [le_refl RS lt_trans] 1));
by (etac 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));
(*SLOW!  5 secs?*)
by (eresolve_tac [lt_Ord RSN (2, LeastI)] 1 THEN (assume_tac 1));
qed "main_induct";

(* ********************************************************************** *)
(* Lemma to simplify the inductive proof                                  *)
(*   - the desired 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 (rtac conjI 1);
by (rtac subsetI 1);
by (etac OUN_E 1);
by (dtac prem1 1);
by (Fast_tac 1);
(** LEVEL 5 **)
by (rtac ballI 1);
by (etac 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 (etac conjE 1);
(** LEVEL 10 **)
by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1));
by (etac impE 1);
by (fast_tac (claset() 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));
(** LEVEL 15 **)
by (rtac ex1I 1);
by (fast_tac (claset() 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));
(** LEVEL 20 **)
by (fast_tac FOL_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 (etac conjE 1);
(** LEVEL 25 **)
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 (etac ex1_two_eq 1);
by (REPEAT (Fast_tac 1));
qed "lemma_simp_induct";

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


Goalw [AC16_def]
        "!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
by (rtac allI 1);
by (rtac 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 (etac 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 (rtac 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 (etac recfunAC16_mono 2);
by (rtac main_induct 1 
        THEN REPEAT (ares_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1));
qed "WO2_AC16";