Theory AC16_WO4

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

The proof of AC16(n, k) ⟹ WO4(n-k)

Tidied (using locales) by LCP
*)

theory AC16_WO4
imports AC16_lemmas
begin

(* ********************************************************************** *)
(* The case of finite set                                                 *)
(* ********************************************************************** *)

lemma lemma1:
     "⟦Finite(A); 0<m; m ∈ nat⟧ 
      ⟹ ∃a f. Ord(a) ∧ domain(f) = a ∧   
                (⋃b<a. f`b) = A ∧ (∀b<a. f`b ≲ m)"
  unfolding Finite_def
apply (erule bexE)
apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
apply (erule exE)
apply (rule_tac x = n in exI)
apply (rule_tac x = "λi ∈ n. {f`i}" in exI)
apply (simp add: ltD bij_def surj_def)
apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun] 
               singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
                    nat_1_lepoll_iff [THEN iffD2]
          elim!: apply_type ltE)
done

(* ********************************************************************** *)
(* The case of infinite set                                               *)
(* ********************************************************************** *)

(* well_ord(x,r) ⟹ well_ord({{y,z}. y ∈ x}, Something(x,z))  **)
lemmas well_ord_paired = paired_bij [THEN bij_is_inj, THEN well_ord_rvimage]

lemma lepoll_trans1: "⟦A ≲ B; ¬ A ≲ C⟧ ⟹ ¬ B ≲ C"
by (blast intro: lepoll_trans)

(* ********************************************************************** *)
(* There exists a well ordered set y such that ...                        *)
(* ********************************************************************** *)

lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]

lemma lemma2: "∃y R. well_ord(y,R) ∧ x ∩ y = 0 ∧ ¬y ≲ z ∧ ¬Finite(y)"
apply (rule_tac x = "{{a,x}. a ∈ nat ∪ Hartog (z) }" in exI)
apply (rule well_ord_Un [OF Ord_nat [THEN well_ord_Memrel] 
                         Ord_Hartog [THEN well_ord_Memrel], THEN exE])
apply (blast intro!: Ord_Hartog well_ord_Memrel well_ord_paired
                      lepoll_trans1 [OF _ not_Hartog_lepoll_self]
                      lepoll_trans [OF subset_imp_lepoll lepoll_paired]
       elim!: nat_not_Finite [THEN notE]
       elim: mem_asym 
       dest!: Un_upper1 [THEN subset_imp_lepoll, THEN lepoll_Finite]
              lepoll_paired [THEN lepoll_Finite])
done

lemma infinite_Un: "¬Finite(B) ⟹ ¬Finite(A ∪ B)"
by (blast intro: subset_Finite)

(* ********************************************************************** *)
(* There is a v ∈ s(u) such that k ≲ x ∩ y (in our case succ(k))    *)
(* The idea of the proof is the following ∈                               *)
(* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y   *)
(* Thence y is less than or equipollent to {v ∈ Pow(x). v ≈ n#-k}      *)
(*   We have obtained this result in two steps ∈                          *)
(*   1. y is less than or equipollent to {v ∈ s(u). a ⊆ v}                  *)
(*      where a is certain k-2 element subset of y                        *)
(*   2. {v ∈ s(u). a ⊆ v} is less than or equipollent                       *)
(*      to {v ∈ Pow(x). v ≈ n-k}                                       *)
(* ********************************************************************** *)

(*Proof simplified by LCP*)
lemma succ_not_lepoll_lemma:
     "⟦¬(∃x ∈ A. f`x=y); f ∈ inj(A, B); y ∈ B⟧   
      ⟹ (λa ∈ succ(A). if(a=A, y, f`a)) ∈ inj(succ(A), B)"
apply (rule_tac d = "λz. if (z=y, A, converse (f) `z) " in lam_injective)
apply (force simp add: inj_is_fun [THEN apply_type])
(*this preliminary simplification prevents looping somehow*)
apply (simp (no_asm_simp))
apply force
done

lemma succ_not_lepoll_imp_eqpoll: "⟦¬A ≈ B; A ≲ B⟧ ⟹ succ(A) ≲ B"
  unfolding lepoll_def eqpoll_def bij_def surj_def
apply (fast elim!: succ_not_lepoll_lemma inj_is_fun)
done


(* ********************************************************************** *)
(* There is a k-2 element subset of y                                     *)
(* ********************************************************************** *)

lemmas ordertype_eqpoll =
       ordermap_bij [THEN exI [THEN eqpoll_def [THEN def_imp_iff, THEN iffD2]]]

lemma cons_cons_subset:
     "⟦a ⊆ y; b ∈ y-a; u ∈ x⟧ ⟹ cons(b, cons(u, a)) ∈ Pow(x ∪ y)"
by fast

lemma cons_cons_eqpoll:
     "⟦a ≈ k; a ⊆ y; b ∈ y-a; u ∈ x; x ∩ y = 0⟧    
      ⟹ cons(b, cons(u, a)) ≈ succ(succ(k))"
by (fast intro!: cons_eqpoll_succ)

lemma set_eq_cons:
     "⟦succ(k) ≈ A; k ≈ B; B ⊆ A; a ∈ A-B; k ∈ nat⟧ ⟹ A = cons(a, B)"
apply (rule equalityI)
prefer 2 apply fast
apply (rule Diff_eq_0_iff [THEN iffD1])
apply (rule equals0I)
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
apply (drule eqpoll_sym [THEN cons_eqpoll_succ], fast)
apply (drule cons_eqpoll_succ, fast)
apply (fast elim!: lepoll_trans [THEN lepoll_trans, THEN succ_lepoll_natE,
         OF eqpoll_sym [THEN eqpoll_imp_lepoll] subset_imp_lepoll])
done

lemma cons_eqE: "⟦cons(x,a) = cons(y,a); x ∉ a⟧ ⟹ x = y "
by (fast elim!: equalityE)

lemma eq_imp_Int_eq: "A = B ⟹ A ∩ C = B ∩ C"
by blast

(* ********************************************************************** *)
(* some arithmetic                                                        *)
(* ********************************************************************** *)

lemma eqpoll_sum_imp_Diff_lepoll_lemma [rule_format]:
     "⟦k ∈ nat; m ∈ nat⟧ 
      ⟹ ∀A B. A ≈ k #+ m ∧ k ≲ B ∧ B ⊆ A ⟶ A-B ≲ m"
apply (induct_tac "k")
apply (simp add: add_0)
apply (blast intro: eqpoll_imp_lepoll lepoll_trans
                    Diff_subset [THEN subset_imp_lepoll])
apply (intro allI impI)
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], fast)
apply (erule_tac x = "A - {xa}" in allE)
apply (erule_tac x = "B - {xa}" in allE)
apply (erule impE)
apply (simp add: add_succ)
apply (fast intro!: Diff_sing_eqpoll lepoll_Diff_sing) 
apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
apply blast 
done

lemma eqpoll_sum_imp_Diff_lepoll:
     "⟦A ≈ succ(k #+ m); B ⊆ A; succ(k) ≲ B;  k ∈ nat; m ∈ nat⟧   
      ⟹ A-B ≲ m"
apply (simp only: add_succ [symmetric]) 
apply (blast intro: eqpoll_sum_imp_Diff_lepoll_lemma) 
done

(* ********************************************************************** *)
(* similar properties for ≈                                          *)
(* ********************************************************************** *)

lemma eqpoll_sum_imp_Diff_eqpoll_lemma [rule_format]:
     "⟦k ∈ nat; m ∈ nat⟧ 
      ⟹ ∀A B. A ≈ k #+ m ∧ k ≈ B ∧ B ⊆ A ⟶ A-B ≈ m"
apply (induct_tac "k")
apply (force dest!: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_0_is_0])
apply (intro allI impI)
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE])
apply (fast elim!: eqpoll_imp_lepoll)
apply (erule_tac x = "A - {xa}" in allE)
apply (erule_tac x = "B - {xa}" in allE)
apply (erule impE)
apply (force intro: eqpoll_sym intro!: Diff_sing_eqpoll)
apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
apply blast 
done

lemma eqpoll_sum_imp_Diff_eqpoll:
     "⟦A ≈ succ(k #+ m); B ⊆ A; succ(k) ≈ B; k ∈ nat; m ∈ nat⟧   
      ⟹ A-B ≈ m"
apply (simp only: add_succ [symmetric]) 
apply (blast intro: eqpoll_sum_imp_Diff_eqpoll_lemma) 
done


(* ********************************************************************** *)
(* LL can be well ordered                                                 *)
(* ********************************************************************** *)

lemma subsets_lepoll_0_eq_unit: "{x ∈ Pow(X). x ≲ 0} = {0}"
by (fast dest!: lepoll_0_is_0 intro!: lepoll_refl)

lemma subsets_lepoll_succ:
     "n ∈ nat ⟹ {z ∈ Pow(y). z ≲ succ(n)} =   
                  {z ∈ Pow(y). z ≲ n} ∪ {z ∈ Pow(y). z ≈ succ(n)}"
by (blast intro: leI le_imp_lepoll nat_into_Ord 
                    lepoll_trans eqpoll_imp_lepoll
          dest!: lepoll_succ_disj)

lemma Int_empty:
     "n ∈ nat ⟹ {z ∈ Pow(y). z ≲ n} ∩ {z ∈ Pow(y). z ≈ succ(n)} = 0"
by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
                 succ_lepoll_natE)

locale AC16 =
  fixes x and y and k and l and m and t_n and R and MM and LL and GG and s 
  defines k_def:     "k   ≡ succ(l)"
      and MM_def:    "MM  ≡ {v ∈ t_n. succ(k) ≲ v ∩ y}"
      and LL_def:    "LL  ≡ {v ∩ y. v ∈ MM}"
      and GG_def:    "GG  ≡ λv ∈ LL. (THE w. w ∈ MM ∧ v ⊆ w) - v"
      and s_def:     "s(u) ≡ {v ∈ t_n. u ∈ v ∧ k ≲ v ∩ y}"
  assumes all_ex:    "∀z ∈ {z ∈ Pow(x ∪ y) . z ≈ succ(k)}.
                       ∃! w. w ∈ t_n ∧ z ⊆ w "
    and disjoint[iff]:  "x ∩ y = 0"
    and "includes":  "t_n ⊆ {v ∈ Pow(x ∪ y). v ≈ succ(k #+ m)}"
    and WO_R[iff]:      "well_ord(y,R)"
    and lnat[iff]:      "l ∈ nat"
    and mnat[iff]:      "m ∈ nat"
    and mpos[iff]:      "0<m"
    and Infinite[iff]:  "¬ Finite(y)"
    and noLepoll:  "¬ y ≲ {v ∈ Pow(x). v ≈ m}"
begin

lemma knat [iff]: "k ∈ nat"
by (simp add: k_def)


(* ********************************************************************** *)
(*   1. y is less than or equipollent to {v ∈ s(u). a ⊆ v}                *)
(*      where a is certain k-2 element subset of y                        *)
(* ********************************************************************** *)

lemma Diff_Finite_eqpoll: "⟦l ≈ a; a ⊆ y⟧ ⟹ y - a ≈ y"
apply (insert WO_R Infinite lnat)
apply (rule eqpoll_trans) 
apply (rule Diff_lesspoll_eqpoll_Card) 
apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])
apply (blast intro: lesspoll_trans1
            intro!: Card_cardinal  
                    Card_cardinal [THEN Card_is_Ord, THEN nat_le_infinite_Ord,
                                   THEN le_imp_lepoll] 
            dest: well_ord_cardinal_eqpoll 
                   eqpoll_sym  eqpoll_imp_lepoll
                   n_lesspoll_nat [THEN lesspoll_trans2]
                   well_ord_cardinal_eqpoll [THEN eqpoll_sym, 
                          THEN eqpoll_imp_lepoll, THEN lepoll_infinite])+
done


lemma s_subset: "s(u) ⊆ t_n"
by (unfold s_def, blast)

lemma sI: 
      "⟦w ∈ t_n; cons(b,cons(u,a)) ⊆ w; a ⊆ y; b ∈ y-a; l ≈ a⟧ 
       ⟹ w ∈ s(u)"
  unfolding s_def succ_def k_def
apply (blast intro!: eqpoll_imp_lepoll [THEN cons_lepoll_cong]
             intro: subset_imp_lepoll lepoll_trans)
done

lemma in_s_imp_u_in: "v ∈ s(u) ⟹ u ∈ v"
by (unfold s_def, blast)


lemma ex1_superset_a:
     "⟦l ≈ a;  a ⊆ y;  b ∈ y - a;  u ∈ x⟧   
      ⟹ ∃! c. c ∈ s(u) ∧ a ⊆ c ∧ b ∈ c"
apply (rule all_ex [simplified k_def, THEN ballE])
 apply (erule ex1E)
 apply (rule_tac a = w in ex1I, blast intro: sI)
 apply (blast dest: s_subset [THEN subsetD] in_s_imp_u_in)
apply (blast del: PowI 
             intro!: cons_cons_subset eqpoll_sym [THEN cons_cons_eqpoll])
done

lemma the_eq_cons:
     "⟦∀v ∈ s(u). succ(l) ≈ v ∩ y;   
         l ≈ a;  a ⊆ y;  b ∈ y - a;  u ∈ x⟧    
      ⟹ (THE c. c ∈ s(u) ∧ a ⊆ c ∧ b ∈ c) ∩ y = cons(b, a)"
apply (frule ex1_superset_a [THEN theI], assumption+)
apply (rule set_eq_cons)
apply (fast+)
done

lemma y_lepoll_subset_s:
     "⟦∀v ∈ s(u). succ(l) ≈ v ∩ y;   
         l ≈ a;  a ⊆ y;  u ∈ x⟧   
      ⟹ y ≲ {v ∈ s(u). a ⊆ v}"
apply (rule Diff_Finite_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, 
                                THEN lepoll_trans],  fast+)
apply (rule_tac  f3 = "λb ∈ y-a. THE c. c ∈ s (u) ∧ a ⊆ c ∧ b ∈ c" 
        in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
apply (simp add: inj_def)
apply (rule conjI)
apply (rule lam_type)
apply (frule ex1_superset_a [THEN theI], fast+, clarify)
apply (rule cons_eqE [of _ a])
apply (drule_tac A = "THE c. P (c)" and C = y for P in eq_imp_Int_eq)
apply (simp_all add: the_eq_cons)
done


(* ********************************************************************** *)
(* back to the second part                                                *)
(* ********************************************************************** *)


(*relies on the disjointness of x, y*)
lemma x_imp_not_y [dest]: "a ∈ x ⟹ a ∉ y"
by (blast dest:  disjoint [THEN equalityD1, THEN subsetD, OF IntI])

lemma w_Int_eq_w_Diff:
     "w ⊆ x ∪ y ⟹ w ∩ (x - {u}) = w - cons(u, w ∩ y)" 
by blast

lemma w_Int_eqpoll_m:
     "⟦w ∈ {v ∈ s(u). a ⊆ v};   
         l ≈ a;  u ∈ x;   
         ∀v ∈ s(u). succ(l) ≈ v ∩ y⟧ 
      ⟹ w ∩ (x - {u}) ≈ m"
apply (erule CollectE)
apply (subst w_Int_eq_w_Diff)
apply (fast dest!: s_subset [THEN subsetD] 
                   "includes" [simplified k_def, THEN subsetD])
apply (blast dest: s_subset [THEN subsetD] 
                   "includes" [simplified k_def, THEN subsetD] 
             dest: eqpoll_sym [THEN cons_eqpoll_succ, THEN eqpoll_sym] 
                   in_s_imp_u_in
            intro!: eqpoll_sum_imp_Diff_eqpoll)
done


(* ********************************************************************** *)
(*   2. {v ∈ s(u). a ⊆ v} is less than or equipollent                       *)
(*      to {v ∈ Pow(x). v ≈ n-k}                                       *)
(* ********************************************************************** *)

lemma eqpoll_m_not_empty: "a ≈ m ⟹ a ≠ 0"
apply (insert mpos)
apply (fast elim!: zero_lt_natE dest!: eqpoll_succ_imp_not_empty)
done

lemma cons_cons_in:
     "⟦z ∈ xa ∩ (x - {u}); l ≈ a; a ⊆ y; u ∈ x⟧   
      ⟹ ∃! w. w ∈ t_n ∧ cons(z, cons(u, a)) ⊆ w"
apply (rule all_ex [THEN bspec])
  unfolding k_def
apply (fast intro!: cons_eqpoll_succ elim: eqpoll_sym)
done

lemma subset_s_lepoll_w:
     "⟦∀v ∈ s(u). succ(l) ≈ v ∩ y; a ⊆ y; l ≈ a; u ∈ x⟧   
      ⟹ {v ∈ s(u). a ⊆ v} ≲ {v ∈ Pow(x). v ≈ m}"
apply (rule_tac f3 = "λw ∈ {v ∈ s (u) . a ⊆ v}. w ∩ (x - {u})" 
       in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
apply (simp add: inj_def)
apply (intro conjI lam_type CollectI)
  apply fast
 apply (blast intro: w_Int_eqpoll_m) 
apply (intro ballI impI)
(** LEVEL 8 **)
apply (rule w_Int_eqpoll_m [THEN eqpoll_m_not_empty, THEN not_emptyE])
apply (blast, assumption+)
apply (drule equalityD1 [THEN subsetD], assumption)
apply (frule cons_cons_in, assumption+)
apply (blast dest: ex1_two_eq intro: s_subset [THEN subsetD] in_s_imp_u_in)+
done


(* ********************************************************************** *)
(* well_ord_subsets_lepoll_n                                              *)
(* ********************************************************************** *)

lemma well_ord_subsets_eqpoll_n:
     "n ∈ nat ⟹ ∃S. well_ord({z ∈ Pow(y) . z ≈ succ(n)}, S)"
apply (rule WO_R [THEN well_ord_infinite_subsets_eqpoll_X,
                  THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
apply (fast intro: bij_is_inj [THEN well_ord_rvimage])+
done

lemma well_ord_subsets_lepoll_n:
     "n ∈ nat ⟹ ∃R. well_ord({z ∈ Pow(y). z ≲ n}, R)"
apply (induct_tac "n")
apply (force intro!: well_ord_unit simp add: subsets_lepoll_0_eq_unit)
apply (erule exE)
apply (rule well_ord_subsets_eqpoll_n [THEN exE], assumption)
apply (simp add: subsets_lepoll_succ)
apply (drule well_ord_radd, assumption)
apply (erule Int_empty [THEN disj_Un_eqpoll_sum,
                  THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
apply (fast elim!: bij_is_inj [THEN well_ord_rvimage])
done


lemma LL_subset: "LL ⊆ {z ∈ Pow(y). z ≲ succ(k #+ m)}"
  unfolding LL_def MM_def
apply (insert "includes")
apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
done

lemma well_ord_LL: "∃S. well_ord(LL,S)"
apply (rule well_ord_subsets_lepoll_n [THEN exE, of "succ(k#+m)"])
apply simp 
apply (blast intro: well_ord_subset [OF _ LL_subset])
done

(* ********************************************************************** *)
(* every element of LL is a contained in exactly one element of MM        *)
(* ********************************************************************** *)

lemma unique_superset_in_MM:
     "v ∈ LL ⟹ ∃! w. w ∈ MM ∧ v ⊆ w"
apply (unfold MM_def LL_def, safe, fast)
apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
apply (rule_tac x = x in all_ex [THEN ballE]) 
apply (blast intro: eqpoll_sym)+
done


(* ********************************************************************** *)
(* The function GG satisfies the conditions of WO4                        *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* The union of appropriate values is the whole x                         *)
(* ********************************************************************** *)

lemma Int_in_LL: "w ∈ MM ⟹ w ∩ y ∈ LL"
by (unfold LL_def, fast)

lemma in_LL_eq_Int: 
     "v ∈ LL ⟹ v = (THE x. x ∈ MM ∧ v ⊆ x) ∩ y"
apply (unfold LL_def, clarify)
apply (subst unique_superset_in_MM [THEN the_equality2])
apply (auto simp add: Int_in_LL)
done

lemma unique_superset1: "a ∈ LL ⟹ (THE x. x ∈ MM ∧ a ⊆ x) ∈ MM"
by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]) 

lemma the_in_MM_subset:
     "v ∈ LL ⟹ (THE x. x ∈ MM ∧ v ⊆ x) ⊆ x ∪ y"
apply (drule unique_superset1)
  unfolding MM_def
apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
done

lemma GG_subset: "v ∈ LL ⟹ GG ` v ⊆ x"
  unfolding GG_def
apply (frule the_in_MM_subset)
apply (frule in_LL_eq_Int)
apply (force elim: equalityE)
done

lemma nat_lepoll_ordertype: "nat ≲ ordertype(y, R)"
apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll]) 
 apply (rule Ord_ordertype [OF WO_R]) 
apply (rule ordertype_eqpoll [THEN eqpoll_imp_lepoll, THEN lepoll_infinite]) 
 apply (rule WO_R) 
apply (rule Infinite) 
done

lemma ex_subset_eqpoll_n: "n ∈ nat ⟹ ∃z. z ⊆ y ∧ n ≈ z"
apply (erule nat_lepoll_imp_ex_eqpoll_n)
apply (rule lepoll_trans [OF nat_lepoll_ordertype]) 
apply (rule ordertype_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]) 
apply (rule WO_R) 
done


lemma exists_proper_in_s: "u ∈ x ⟹ ∃v ∈ s(u). succ(k) ≲ v ∩ y"
apply (rule ccontr)
apply (subgoal_tac "∀v ∈ s (u) . k ≈ v ∩ y")
prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
  unfolding k_def
apply (insert all_ex "includes" lnat)
apply (rule ex_subset_eqpoll_n [THEN exE], assumption)
apply (rule noLepoll [THEN notE])
apply (blast intro: lepoll_trans [OF y_lepoll_subset_s subset_s_lepoll_w])
done

lemma exists_in_MM: "u ∈ x ⟹ ∃w ∈ MM. u ∈ w"
apply (erule exists_proper_in_s [THEN bexE])
apply (unfold MM_def s_def, fast)
done

lemma exists_in_LL: "u ∈ x ⟹ ∃w ∈ LL. u ∈ GG`w"
apply (rule exists_in_MM [THEN bexE], assumption)
apply (rule bexI)
apply (erule_tac [2] Int_in_LL)
  unfolding GG_def
apply (simp add: Int_in_LL)
apply (subst unique_superset_in_MM [THEN the_equality2])
apply (fast elim!: Int_in_LL)+
done

lemma OUN_eq_x: "well_ord(LL,S) ⟹       
      (⋃b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x"
apply (rule equalityI)
apply (rule subsetI)
apply (erule OUN_E)
apply (rule GG_subset [THEN subsetD])
prefer 2 apply assumption
apply (blast intro: ltD  ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun,
                                       THEN apply_type])
apply (rule subsetI)
apply (erule exists_in_LL [THEN bexE])
apply (force intro: ltI [OF _ Ord_ordertype]
                    ordermap_type [THEN apply_type]
             simp add: ordermap_bij [THEN bij_is_inj, THEN left_inverse])
done

(* ********************************************************************** *)
(* Every element of the family is less than or equipollent to n-k (m)     *)
(* ********************************************************************** *)

lemma in_MM_eqpoll_n: "w ∈ MM ⟹ w ≈ succ(k #+ m)"
  unfolding MM_def
apply (fast dest: "includes" [THEN subsetD])
done

lemma in_LL_eqpoll_n: "w ∈ LL ⟹ succ(k) ≲ w"
by (unfold LL_def MM_def, fast)

lemma in_LL: "w ∈ LL ⟹ w ⊆ (THE x. x ∈ MM ∧ w ⊆ x)"
by (erule subset_trans [OF in_LL_eq_Int [THEN equalityD1] Int_lower1])

lemma all_in_lepoll_m: 
      "well_ord(LL,S) ⟹       
       ∀b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) ≲ m"
  unfolding GG_def
apply (rule oallI)
apply (simp add: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN apply_type])
apply (insert "includes")
apply (rule eqpoll_sum_imp_Diff_lepoll)
apply (blast del: subsetI
             dest!: ltD 
             intro!: eqpoll_sum_imp_Diff_lepoll in_LL_eqpoll_n
             intro: in_LL   unique_superset1 [THEN in_MM_eqpoll_n] 
                    ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, 
                                  THEN apply_type])+
done

lemma "conclusion":
     "∃a f. Ord(a) ∧ domain(f) = a ∧ (⋃b<a. f ` b) = x ∧ (∀b<a. f ` b ≲ m)"
apply (rule well_ord_LL [THEN exE])
apply (rename_tac S)
apply (rule_tac x = "ordertype (LL,S)" in exI)
apply (rule_tac x = "λb ∈ ordertype(LL,S). 
                      GG ` (converse (ordermap (LL,S)) ` b)"  in exI)
apply (simp add: ltD)
apply (blast intro: lam_funtype [THEN domain_of_fun] 
                    Ord_ordertype  OUN_eq_x  all_in_lepoll_m [THEN ospec])
done

end


(* ********************************************************************** *)
(* The main theorem AC16(n, k) ⟹ WO4(n-k)                               *)
(* ********************************************************************** *)

theorem AC16_WO4: 
     "⟦AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k ∈ nat; m ∈ nat⟧ ⟹ WO4(m)"
  unfolding AC_Equiv.AC16_def WO4_def
apply (rule allI)
apply (case_tac "Finite (A)")
apply (rule lemma1, assumption+)
apply (cut_tac lemma2)
apply (elim exE conjE)
apply (erule_tac x = "A ∪ y" in allE)
apply (frule infinite_Un, drule mp, assumption)
apply (erule zero_lt_natE, assumption, clarify)
apply (blast intro: AC16.conclusion [OF AC16.intro])
done

end