Quelle  WO1_AC.thy

(*  Title:      ZF/AC/WO1_AC.thy
  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 \<Longrightarrow> AC1                                                            *)
(* ********************************************************************** *)

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

(* ********************************************************************** *)
(* WO1 \<Longrightarrow> AC10(n) (n >= 1)                                               *)
(* ********************************************************************** *)

lemma lemma1: "[WO1; ∀B ∈ A. ∃C ∈ D(B). P(C,B)] ==> ∃f. ∀B ∈ A. P(f`B,B)"
  unfolding WO1_def
apply (erule_tac x = "∪({{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"
  unfolding 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})"
  unfolding 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) ==> ∪({{f`Inl(i), f`Inr(i)}. i ∈ D})=B"
  unfolding 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)) ∧
                ∪(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)"
  unfolding AC10_def
apply (fast intro!: lemma1 elim!: lemma2)
done

end