# Theory WO1_AC

Up to index of Isabelle/ZF/AC

theory WO1_AC
imports AC_Equiv
begin

    (*  Title:      ZF/AC/WO1_AC.thy
        ID:         $Id: WO1_AC.thy,v 1.3 2005/06/17 14:15:10 haftmann Exp $
        Author:     Krzysztof Grabczewski

    The proofs of WO1 ==> AC1 and WO1 ==> AC10(n) for n >= 1

    The latter proof is referred to as clear by the Rubins.
    However it seems to be quite complicated.
    The formal proof presented below is a mechanisation of the proof
    by Lawrence C. Paulson which is the following:

    Assume WO1.  Let s be a set of infinite sets.

    Suppose x ∈ s.  Then x is equipollent to |x| (by WO1), an infinite cardinal
    call it K.  Since K = K |+| K = |K+K| (by InfCard_cdouble_eq) there is an
    isomorphism h ∈ bij(K+K, x).  (Here + means disjoint sum.)

    So there is a partition of x into 2-element sets, namely

            {{h(Inl(i)), h(Inr(i))} . i ∈ K}

    So for all x ∈ s the desired partition exists.  By AC1 (which follows from WO1)
    there exists a function f that chooses a partition for each x ∈ s.  Therefore we
    have AC10(2).

    *)

    theory WO1_AC imports AC_Equiv begin

    (* ********************************************************************** *)
    (* WO1 ==> AC1                                                            *)
    (* ********************************************************************** *)

    theorem WO1_AC1: "WO1 ==> AC1"
    by (unfold AC1_def WO1_def, fast elim!: ex_choice_fun)

    (* ********************************************************************** *)
    (* WO1 ==> AC10(n) (n >= 1)                                               *)
    (* ********************************************************************** *)

    lemma lemma1: "[| WO1; ∀B ∈ A. ∃C ∈ D(B). P(C,B) |] ==> ∃f. ∀B ∈ A. P(f`B,B)"
    apply (unfold WO1_def)
    apply (erule_tac x = "Union ({{C ∈ D (B) . P (C,B) }. B ∈ A}) " in allE)
    apply (erule exE, drule ex_choice_fun, fast)
    apply (erule exE)
    apply (rule_tac x = "λx ∈ A. f`{C ∈ D (x) . P (C,x) }" in exI)
    apply (simp, blast dest!: apply_type [OF _ RepFunI])
    done

    lemma lemma2_1: "[| ~Finite(B); WO1 |] ==> |B| + |B| ≈  B"
    apply (unfold WO1_def)
    apply (rule eqpoll_trans)
    prefer 2 apply (fast elim!: well_ord_cardinal_eqpoll)
    apply (rule eqpoll_sym [THEN eqpoll_trans])
    apply (fast elim!: well_ord_cardinal_eqpoll)
    apply (drule spec [of _ B])
    apply (clarify dest!: eqpoll_imp_Finite_iff [OF well_ord_cardinal_eqpoll])
    apply (simp add: cadd_def [symmetric]
                eqpoll_refl InfCard_cdouble_eq Card_cardinal Inf_Card_is_InfCard)
    done

    lemma lemma2_2:
         "f ∈ bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i ∈ D} ∈ Pow(Pow(B))"
    by (fast elim!: bij_is_fun [THEN apply_type])

    lemma lemma2_3:
            "f ∈ bij(D+D, B) ==> pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i ∈ D})"
    apply (unfold pairwise_disjoint_def)
    apply (blast dest: bij_is_inj [THEN inj_apply_equality])
    done

    lemma lemma2_4:
         "[| f ∈ bij(D+D, B); 1≤n |]
          ==> sets_of_size_between({{f`Inl(i), f`Inr(i)}. i ∈ D}, 2, succ(n))"
    apply (simp (no_asm_simp) add: sets_of_size_between_def succ_def)
    apply (blast intro!: cons_lepoll_cong
                intro: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll]
                       le_imp_subset [THEN subset_imp_lepoll]  lepoll_trans
                dest: bij_is_inj [THEN inj_apply_equality] elim!: mem_irrefl)
    done

    lemma lemma2_5:
         "f ∈ bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i ∈ D})=B"
    apply (unfold bij_def surj_def)
    apply (fast elim!: inj_is_fun [THEN apply_type])
    done

    lemma lemma2:
         "[| WO1; ~Finite(B); 1≤n  |]
          ==> ∃C ∈ Pow(Pow(B)). pairwise_disjoint(C) &
                    sets_of_size_between(C, 2, succ(n)) &
                    Union(C)=B"
    apply (drule lemma2_1 [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]],
           assumption)
    apply (blast intro!: lemma2_2 lemma2_3 lemma2_4 lemma2_5)
    done

    theorem WO1_AC10: "[| WO1; 1≤n |] ==> AC10(n)"
    apply (unfold AC10_def)
    apply (fast intro!: lemma1 elim!: lemma2)
    done

    end

theorem WO1_AC1:

      WO1 ==> AC1

lemma lemma1:

      [| WO1; ∀B∈A. ∃C∈D(B). P(C, B) |] ==> ∃f. ∀B∈A. P(f ` B, B)

lemma lemma2_1:

      [| ¬ Finite(B); WO1 |] ==> |B| + |B| ≈ B

lemma lemma2_2:

      f ∈ bij(D + D, B) ==> {{f ` Inl(i), f ` Inr(i)} . i ∈ D} ∈ Pow(Pow(B))

lemma lemma2_3:

      f ∈ bij(D + D, B) ==> pairwise_disjoint({{f ` Inl(i), f ` Inr(i)} . i ∈ D})

lemma lemma2_4:

      [| f ∈ bij(D + D, B); 1 ≤ n |]
      ==> sets_of_size_between({{f ` Inl(i), f ` Inr(i)} . i ∈ D}, 2, succ(n))

lemma lemma2_5:

      f ∈ bij(D + D, B) ==> (\<Union>i∈D. {f ` Inl(i), f ` Inr(i)}) = B

lemma lemma2:

      [| WO1; ¬ Finite(B); 1 ≤ n |]
      ==> ∃C∈Pow(Pow(B)).
             pairwise_disjoint(C) ∧
             sets_of_size_between(C, 2, succ(n)) ∧ \<Union>C = B

theorem WO1_AC10:

      [| WO1; 1 ≤ n |] ==> AC10(n)