(*  Title:      ZF/AC/WO2_AC16.thy
    Author:     Krzysztof Grabczewski

The proof of WO2 \<Longrightarrow> 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)
*)

theory WO2_AC16 imports AC_Equiv AC16_lemmas Cardinal_aux begin

(**** A recursive definition used in the proof of WO2 \<Longrightarrow> AC16 ****)

definition
  recfunAC16 :: "[i,i,i,i] → i"  where
    "recfunAC16(f,h,i,a) ≡
         transrec2(i, 0,
              λg r. if (∃y ∈ r. h`g ⊆ y) then r
                    else r ∪ {f`(μ i. h`g ⊆ f`i ∧
                         (∀b<a. (h`b ⊆ f`i ⟶ (∀t ∈ r. ¬ h`b ⊆ t))))})"

(* ********************************************************************** *)
(* Basic properties of recfunAC16                                         *)
(* ********************************************************************** *)

lemma recfunAC16_0: "recfunAC16(f,h,0,a) = 0"
by (simp add: recfunAC16_def)

lemma recfunAC16_succ: 
     "recfunAC16(f,h,succ(i),a) =
      (if (∃y ∈ recfunAC16(f,h,i,a). h ` i ⊆ y) then recfunAC16(f,h,i,a)
       else recfunAC16(f,h,i,a) ∪
            {f ` (μ j. h ` i ⊆ f ` j ∧
             (∀b<a. (h`b ⊆ f`j
              ⟶ (∀t ∈ recfunAC16(f,h,i,a). ¬ h`b ⊆ t))))})"
apply (simp add: recfunAC16_def)
done

lemma recfunAC16_Limit: "Limit(i)
        ==> recfunAC16(f,h,i,a) = (∪j<i. recfunAC16(f,h,j,a))"
by (simp add: recfunAC16_def transrec2_Limit)

(* ********************************************************************** *)
(* Monotonicity of transrec2                                              *)
(* ********************************************************************** *)

lemma transrec2_mono_lemma [rule_format]:
     "[∧g r. r ⊆ B(g,r); Ord(i)]
      ==> j<i ⟶ transrec2(j, 0, B) ⊆ transrec2(i, 0, B)"
apply (erule trans_induct)
apply (rule Ord_cases, assumption+, fast)
apply (simp (no_asm_simp))
apply (blast elim!: leE) 
apply (simp add: transrec2_Limit) 
apply (blast intro: OUN_I ltI Ord_in_Ord [THEN le_refl]
             elim!: Limit_has_succ [THEN ltE])
done

lemma transrec2_mono:
     "[∧g r. r ⊆ B(g,r); j≤i]
      ==> transrec2(j, 0, B) ⊆ transrec2(i, 0, B)"
apply (erule leE)
apply (rule transrec2_mono_lemma)
apply (auto intro: lt_Ord2 ) 
done

(* ********************************************************************** *)
(* Monotonicity of recfunAC16                                             *)
(* ********************************************************************** *)

lemma recfunAC16_mono: 
       "i≤j ==> recfunAC16(f, g, i, a) ⊆ recfunAC16(f, g, j, a)"
  unfolding recfunAC16_def
apply (rule transrec2_mono, auto) 
done

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


lemma lemma3_1:
    "[∀y<x. ∀z<a. z<y | (∃Y ∈ F(y). f(z)<=Y) ⟶ (∃! Y. Y ∈ F(y) ∧ f(z)<=Y);
        ∀i j. i≤j ⟶ F(i) ⊆ F(j); j≤i; i<x; z<a;
        V ∈ F(i); f(z)<=V; W ∈ F(j); f(z)<=W]
     ==> V = W"
apply (erule asm_rl allE impE)+
apply (drule subsetD, assumption, blast) 
done


lemma lemma3:
    "[∀y<x. ∀z<a. z<y | (∃Y ∈ F(y). f(z)<=Y) ⟶ (∃! Y. Y ∈ F(y) ∧ f(z)<=Y);
        ∀i j. i≤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"
apply (rule_tac j=j in Ord_linear_le [OF lt_Ord lt_Ord], assumption+)
apply (erule lemma3_1 [symmetric], assumption+)
apply (erule lemma3_1, assumption+)
done

lemma lemma4:
     "[∀y<x. F(y) ⊆ X ∧
                (∀x<a. x < y | (∃Y ∈ F(y). h(x) ⊆ Y) ⟶
                 (∃! Y. Y ∈ F(y) ∧ h(x) ⊆ Y));
         x < a]
      ==> ∀y<x. ∀z<a. z < y | (∃Y ∈ F(y). h(z) ⊆ Y) ⟶
                       (∃! Y. Y ∈ F(y) ∧ h(z) ⊆ Y)"
apply (intro oallI impI)
apply (drule ospec, assumption, clarify)
apply (blast elim!: oallE ) 
done

lemma lemma5:
     "[∀y<x. F(y) ⊆ X ∧
               (∀x<a. x < y | (∃Y ∈ F(y). h(x) ⊆ Y) ⟶
                (∃! Y. Y ∈ F(y) ∧ h(x) ⊆ Y));
         x < a; Limit(x); ∀i j. i≤j ⟶ F(i) ⊆ F(j)]
      ==> (∪x<x. F(x)) ⊆ X ∧
          (∀xa<a. xa < x | (∃x ∈ ∪x<x. F(x). h(xa) ⊆ x)
                ⟶ (∃! Y. Y ∈ (∪x<x. F(x)) ∧ h(xa) ⊆ Y))"
apply (rule conjI)
apply (rule subsetI)
apply (erule OUN_E)
apply (drule ospec, assumption, fast)
apply (drule lemma4, assumption)
apply (rule oallI)
apply (rule impI)
apply (erule disjE)
apply (frule ospec, erule Limit_has_succ, assumption) 
apply (drule_tac A = a and x = xa in ospec, assumption)
apply (erule impE, rule le_refl [THEN disjI1], erule lt_Ord) 
apply (blast intro: lemma3 Limit_has_succ) 
apply (blast intro: lemma3) 
done

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

(*
  First quite complicated proof of the fact used in the recursive construction
  of the family T_gamma (WO2 \<Longrightarrow> 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                                                   *)
(* ********************************************************************** *)


lemma dbl_Diff_eqpoll_Card:
      "[A≈a; Card(a); ¬Finite(a); B≺a; C≺a] ==> A - B - C≈a"
by (blast intro: Diff_lesspoll_eqpoll_Card) 

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


lemma Finite_lesspoll_infinite_Ord: 
      "[Finite(X); ¬Finite(a); Ord(a)] ==> X≺a"
  unfolding lesspoll_def
apply (rule conjI)
apply (drule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption)
  unfolding Finite_def
apply (blast intro: leI [THEN le_imp_subset, THEN subset_imp_lepoll]
                    ltI eqpoll_imp_lepoll lepoll_trans) 
apply (blast intro: eqpoll_sym [THEN eqpoll_trans])
done

lemma Union_lesspoll:
     "[∀x ∈ X. x < n ∧ x ⊆ T; well_ord(T, R); X < b;
         b<a; ¬Finite(a); Card(a); n ∈ nat]
      ==> ∪(X)≺a"
apply (case_tac "Finite (X)")
apply (blast intro: Card_is_Ord Finite_lesspoll_infinite_Ord 
                    lepoll_nat_imp_Finite Finite_Union)
apply (drule lepoll_imp_ex_le_eqpoll) 
apply (erule lt_Ord) 
apply (elim exE conjE)
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
apply (erule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1],
                         THEN exE])
apply (frule bij_is_surj [THEN surj_image_eq])
apply (drule image_fun [OF bij_is_fun subset_refl])
apply (drule sym [THEN trans], assumption)
apply (blast intro: lt_Ord UN_lepoll lt_Card_imp_lesspoll
                    lt_trans1 lesspoll_trans1)
done

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

lemma Un_sing_eq_cons: "A ∪ {a} = cons(a, A)"
by fast

lemma Un_lepoll_succ: "A < B ==> A ∪ {a} < succ(B)"
apply (simp add: Un_sing_eq_cons succ_def)
apply (blast elim!: mem_irrefl intro: cons_lepoll_cong)
done

lemma Diff_UN_succ_empty: "Ord(a) ==> F(a) - (∪b<succ(a). F(b)) = 0"
by (fast intro!: le_refl)

lemma Diff_UN_succ_subset: "Ord(a) ==> F(a) ∪ X - (∪b<succ(a). F(b)) ⊆ X"
by blast

lemma recfunAC16_Diff_lepoll_1:
     "Ord(x)
      ==> recfunAC16(f, g, x, a) - (∪i<x. recfunAC16(f, g, i, a)) < 1"
apply (erule Ord_cases)
  apply (simp add: recfunAC16_0 empty_subsetI [THEN subset_imp_lepoll])
(*Limit case*)
prefer 2 apply (simp add: recfunAC16_Limit Diff_cancel 
                          empty_subsetI [THEN subset_imp_lepoll])
(*succ case*)
apply (simp add: recfunAC16_succ
                 Diff_UN_succ_empty [of _ "λj. recfunAC16(f,g,j,a)"]
                 empty_subsetI [THEN subset_imp_lepoll])
apply (best intro: Diff_UN_succ_subset [THEN subset_imp_lepoll]
                   singleton_eqpoll_1 [THEN eqpoll_imp_lepoll] lepoll_trans)
done

lemma in_Least_Diff:
     "[z ∈ F(x); Ord(x)]
      ==> z ∈ F(μ i. z ∈ F(i)) - (∪j<(μ i. z ∈ F(i)). F(j))"
by (fast elim: less_LeastE elim!: LeastI)

lemma Least_eq_imp_ex:
     "[(μ i. w ∈ F(i)) = (μ i. z ∈ F(i));
         w ∈ (∪i<a. F(i)); z ∈ (∪i<a. F(i))]
      ==> ∃b<a. w ∈ (F(b) - (∪c<b. F(c))) ∧ z ∈ (F(b) - (∪c<b. F(c)))"
apply (elim OUN_E)
apply (drule in_Least_Diff, erule lt_Ord) 
apply (frule in_Least_Diff, erule lt_Ord) 
apply (rule oexI, force) 
apply (blast intro: lt_Ord Least_le [THEN lt_trans1]) 
done


lemma two_in_lepoll_1: "[A < 1; a ∈ A; b ∈ A] ==> a=b"
by (fast dest!: lepoll_1_is_sing)


lemma UN_lepoll_index:
     "[∀i<a. F(i)-(∪j<i. F(j)) < 1; Limit(a)]
      ==> (∪x<a. F(x)) < a"
apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
apply (rule_tac x = "λz ∈ (∪x<a. F (x)). μ i. z ∈ F (i) " in exI)
  unfolding inj_def
apply (rule CollectI)
apply (rule lam_type)
apply (erule OUN_E)
apply (erule Least_in_Ord)
apply (erule ltD)
apply (erule lt_Ord2)
apply (intro ballI)
apply (simp (no_asm_simp))
apply (rule impI)
apply (drule Least_eq_imp_ex, assumption+)
apply (fast elim!: two_in_lepoll_1)
done


lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) < y"
apply (erule trans_induct3)
(*0 case*)
apply (simp (no_asm_simp) add: recfunAC16_0 lepoll_refl)
(*succ case*)
apply (simp (no_asm_simp) add: recfunAC16_succ)
apply (blast dest!: succI1 [THEN rev_bspec] 
             intro: subset_succI [THEN subset_imp_lepoll] Un_lepoll_succ  
                    lepoll_trans)
apply (simp (no_asm_simp) add: recfunAC16_Limit)
apply (blast intro: lt_Ord [THEN recfunAC16_Diff_lepoll_1] UN_lepoll_index)
done


lemma Union_recfunAC16_lesspoll:
     "[recfunAC16(f,g,y,a) ⊆ {X ∈ Pow(A). X≈n};
         A≈a; y<a; ¬Finite(a); Card(a); n ∈ nat]
      ==> ∪(recfunAC16(f,g,y,a))≺a"
apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE])
apply (rule_tac T=A in Union_lesspoll, simp_all)
apply (blast intro!: eqpoll_imp_lepoll)
apply (blast intro: bij_is_inj Card_is_Ord [THEN well_ord_Memrel]
                    well_ord_rvimage)
apply (erule lt_Ord [THEN recfunAC16_lepoll_index])
done

lemma dbl_Diff_eqpoll:
     "[recfunAC16(f, h, y, a) ⊆ {X ∈ Pow(A) . X≈succ(k #+ m)};
         Card(a); ¬ Finite(a); A≈a;
         k ∈ nat; y<a;
         h ∈ bij(a, {Y ∈ Pow(A). Y≈succ(k)})]
      ==> A - ∪(recfunAC16(f, h, y, a)) - h`y≈a"
apply (rule dbl_Diff_eqpoll_Card, simp_all)
apply (simp add: Union_recfunAC16_lesspoll)
apply (rule Finite_lesspoll_infinite_Ord) 
apply (rule Finite_def [THEN def_imp_iff, THEN iffD2]) 
apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption)  
apply (blast intro: Card_is_Ord) 
done

(* back to the proof *)

lemmas disj_Un_eqpoll_nat_sum = 
    eqpoll_trans [THEN eqpoll_trans, 
                  OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum]


lemma Un_in_Collect: "[x ∈ Pow(A - B - h`i); x≈m;
        h ∈ bij(a, {x ∈ Pow(A) . x≈k}); i<a; k ∈ nat; m ∈ nat]
        ==> h ` i ∪ x ∈ {x ∈ Pow(A) . x≈k #+ m}"
by (blast intro: disj_Un_eqpoll_nat_sum
          dest:  ltD bij_is_fun [THEN apply_type])


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

lemma lemma6:
     "[∀y<succ(j). F(y)<=X ∧ (∀x<a. x<y | P(x,y) ⟶ Q(x,y)); succ(j)<a]
      ==> F(j)<=X ∧ (∀x<a. x<j | P(x,j) ⟶ Q(x,j))"
by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]) 


lemma lemma7:
     "[∀x<a. x<j | P(x,j) ⟶ Q(x,j); succ(j)<a]
      ==> P(j,j) ⟶ (∀x<a. x≤j | P(x,j) ⟶ Q(x,j))"
by (fast elim!: leE)

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

lemma ex_subset_eqpoll:
     "[A≈a; ¬ Finite(a); Ord(a); m ∈ nat] ==> ∃X ∈ Pow(A). X≈m"
apply (rule lepoll_imp_eqpoll_subset [of m A, THEN exE]) 
 apply (rule lepoll_trans, rule leI [THEN le_imp_lepoll])
  apply (blast intro: lt_trans2 [OF ltI nat_le_infinite_Ord] Ord_nat)
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) 
apply (fast elim!: eqpoll_sym)
done

lemma subset_Un_disjoint: "[A ⊆ B ∪ C; A ∩ C = 0] ==> A ⊆ B"
by blast


lemma Int_empty:
     "[X ∈ Pow(A - ∪(B) -C); T ∈ B; F ⊆ T] ==> F ∩ X = 0"
by blast


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


lemma subset_imp_eq_lemma:
     "m ∈ nat ==> ∀A B. A ⊆ B ∧ m < A ∧ B < m ⟶ A=B"
apply (induct_tac "m")
apply (fast dest!: lepoll_0_is_0)
apply (intro allI impI)
apply (elim conjE)
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], assumption)
apply (frule subsetD [THEN Diff_sing_lepoll], assumption+)
apply (frule lepoll_Diff_sing)
apply (erule allE impE)+
apply (rule conjI)
prefer 2 apply fast
apply fast
apply (blast elim: equalityE) 
done


lemma subset_imp_eq: "[A ⊆ B; m < A; B < m; m ∈ nat] ==> A=B"
by (blast dest!: subset_imp_eq_lemma)


lemma bij_imp_arg_eq:
     "[f ∈ bij(a, {Y ∈ X. Y≈succ(k)}); k ∈ nat; f`b ⊆ f`y; b<a; y<a]
      ==> b=y"
apply (drule subset_imp_eq)
apply (erule_tac [3] nat_succI)
  unfolding bij_def inj_def
apply (blast intro: eqpoll_sym eqpoll_imp_lepoll
             dest:  ltD apply_type)+
done


lemma ex_next_set:
     "[recfunAC16(f, h, y, a) ⊆ {X ∈ Pow(A) . X≈succ(k #+ m)};
         Card(a); ¬ Finite(a); A≈a;
         k ∈ nat; m ∈ nat; y<a;
         h ∈ bij(a, {Y ∈ Pow(A). Y≈succ(k)});
         ¬ (∃Y ∈ recfunAC16(f, h, y, a). h`y ⊆ Y)]
      ==> ∃X ∈ {Y ∈ Pow(A). Y≈succ(k #+ m)}. h`y ⊆ X ∧
                (∀b<a. h`b ⊆ X ⟶
                (∀T ∈ recfunAC16(f, h, y, a). ¬ h`b ⊆ T))"
apply (erule_tac m1=m in dbl_Diff_eqpoll [THEN ex_subset_eqpoll, THEN bexE], 
       assumption+)
apply (erule Card_is_Ord, assumption)
apply (frule Un_in_Collect, (erule asm_rl nat_succI)+) 
apply (erule CollectE)
apply (rule rev_bexI, simp)
apply (rule conjI, blast) 
apply (intro ballI impI oallI notI)
apply (drule subset_Un_disjoint, rule Int_empty, assumption+)
apply (blast dest: bij_imp_arg_eq) 
done

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

lemma ex_next_Ord:
     "[recfunAC16(f, h, y, a) ⊆ {X ∈ Pow(A) . X≈succ(k #+ m)};
         Card(a); ¬ Finite(a); A≈a;
         k ∈ nat; m ∈ nat; y<a;
         h ∈ bij(a, {Y ∈ Pow(A). Y≈succ(k)});
         f ∈ bij(a, {Y ∈ Pow(A). Y≈succ(k #+ m)});
         ¬ (∃Y ∈ recfunAC16(f, h, y, a). h`y ⊆ Y)]
      ==> ∃c<a. h`y ⊆ f`c ∧
                (∀b<a. h`b ⊆ f`c ⟶
                (∀T ∈ recfunAC16(f, h, y, a). ¬ h`b ⊆ T))"
apply (drule ex_next_set, assumption+)
apply (erule bexE)
apply (rule_tac x="converse(f)`X" in oexI)
apply (simp add: right_inverse_bij)
apply (blast intro: bij_converse_bij bij_is_fun [THEN apply_type] ltI
                    Card_is_Ord)
done


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

lemma lemma8:
     "[∀x<a. x<j | (∃xa ∈ F(j). P(x, xa))
         ⟶ (∃! Y. Y ∈ F(j) ∧ P(x, Y)); F(j) ⊆ X;
         L ∈ X; P(j, L) ∧ (∀x<a. P(x, L) ⟶ (∀xa ∈ F(j). ¬P(x, xa)))]
      ==> F(j) ∪ {L} ⊆ X ∧
          (∀x<a. x≤j | (∃xa ∈ (F(j) ∪ {L}). P(x, xa)) ⟶
                 (∃! Y. Y ∈ (F(j) ∪ {L}) ∧ P(x, Y)))"
apply (rule conjI)
apply (fast intro!: singleton_subsetI)
apply (rule oallI)
apply (blast elim!: leE oallE)
done

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

lemma main_induct:
     "[b < a; f ∈ bij(a, {Y ∈ Pow(A) . Y≈succ(k #+ m)});
         h ∈ bij(a, {Y ∈ Pow(A) . Y≈succ(k)});
         ¬Finite(a); Card(a); A≈a; k ∈ nat; m ∈ nat]
      ==> recfunAC16(f, h, b, a) ⊆ {X ∈ Pow(A) . X≈succ(k #+ m)} ∧
          (∀x<a. x < b | (∃Y ∈ recfunAC16(f, h, b, a). h ` x ⊆ Y) ⟶
          (∃! Y. Y ∈ recfunAC16(f, h, b, a) ∧ h ` x ⊆ Y))"
apply (erule lt_induct)
apply (frule lt_Ord)
apply (erule Ord_cases)
(* case 0 *)
apply (simp add: recfunAC16_0)
(* case Limit *)
prefer 2  apply (simp add: recfunAC16_Limit)
          apply (rule lemma5, assumption+)
          apply (blast dest!: recfunAC16_mono)
(* case succ *)
apply clarify 
apply (erule lemma6 [THEN conjE], assumption)
apply (simp (no_asm_simp) split del: split_if add: recfunAC16_succ)
apply (rule conjI [THEN split_if [THEN iffD2]])
 apply (simp, erule lemma7, assumption)
apply (rule impI)
apply (rule ex_next_Ord [THEN oexE], 
       assumption+, rule le_refl [THEN lt_trans], assumption+) 
apply (erule lemma8, assumption)
 apply (rule bij_is_fun [THEN apply_type], assumption)
 apply (erule Least_le [THEN lt_trans2, THEN ltD])
  apply (erule lt_Ord) 
 apply (erule succ_leI)
apply (erule LeastI) 
apply (erule lt_Ord) 
done

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

lemma lemma_simp_induct:
     "[∀b. b<a ⟶ F(b) ⊆ S ∧ (∀x<a. (x<b | (∃Y ∈ F(b). f`x ⊆ Y))
                                   ⟶ (∃! Y. Y ∈ F(b) ∧ f`x ⊆ Y));
         f ∈ a->f``(a); Limit(a);
         ∀i j. i≤j ⟶ F(i) ⊆ F(j)]
        ==> (∪j<a. F(j)) ⊆ S ∧
            (∀x ∈ f``a. ∃! Y. Y ∈ (∪j<a. F(j)) ∧ x ⊆ Y)"
apply (rule conjI)
apply (rule subsetI)
apply (erule OUN_E, blast) 
apply (rule ballI)
apply (erule imageE)
apply (drule ltI, erule Limit_is_Ord) 
apply (drule Limit_has_succ, assumption) 
apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption)
apply (erule conjE)
apply (drule ospec) 
(** LEVEL 10 **)
apply (erule leI [THEN succ_leE])
apply (erule impE)
apply (fast elim!: leI [THEN succ_leE, THEN lt_Ord, THEN le_refl])
apply (drule apply_equality, assumption) 
apply (elim conjE ex1E)
(** LEVEL 15 **)
apply (rule ex1I, blast) 
apply (elim conjE OUN_E)
apply (erule_tac i="succ(xa)" and j=aa 
       in Ord_linear_le [OF lt_Ord lt_Ord], assumption)
prefer 2 
apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 
(** LEVEL 20 **)
apply (drule_tac x1=aa in spec [THEN mp], assumption)
apply (frule succ_leE)
apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 
done

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

theorem WO2_AC16: "[WO2; 0<m; k ∈ nat; m ∈ nat] ==> AC16(k #+ m,k)"
  unfolding AC16_def
apply (rule allI)
apply (rule impI)
apply (frule WO2_infinite_subsets_eqpoll_X, assumption+)
apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp, simp) 
apply (frule WO2_imp_ex_Card)
apply (elim exE conjE)
apply (drule eqpoll_trans [THEN eqpoll_sym, 
                           THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]],
       assumption)
apply (drule eqpoll_trans [THEN eqpoll_sym, 
                           THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]], 
       assumption+)
apply (elim exE)
apply (rename_tac h)
apply (rule_tac x = "∪j<a. recfunAC16 (h,f,j,a) " in exI)
apply (rule_tac P="λz. Y ∧ (∀x ∈ z. Z(x))"  for Y Z
       in bij_is_surj [THEN surj_image_eq, THEN subst], assumption)
apply (rule lemma_simp_induct)
apply (blast del: conjI notI
             intro!: main_induct eqpoll_imp_lepoll [THEN lepoll_infinite] ) 
apply (blast intro: bij_is_fun [THEN surj_image, THEN surj_is_fun])
apply (erule eqpoll_imp_lepoll [THEN lepoll_infinite, 
                                THEN infinite_Card_is_InfCard, 
                                THEN InfCard_is_Limit], 
       assumption+)
apply (blast dest!: recfunAC16_mono)
done

end