1(* Title: ZF/AC/WO1_AC.thy 2 Author: Krzysztof Grabczewski 3 4The proofs of WO1 ==> AC1 and WO1 ==> AC10(n) for n >= 1 5 6The latter proof is referred to as clear by the Rubins. 7However it seems to be quite complicated. 8The formal proof presented below is a mechanisation of the proof 9by Lawrence C. Paulson which is the following: 10 11Assume WO1. Let s be a set of infinite sets. 12 13Suppose x \<in> s. Then x is equipollent to |x| (by WO1), an infinite cardinal 14call it K. Since K = K \<oplus> K = |K+K| (by InfCard_cdouble_eq) there is an 15isomorphism h \<in> bij(K+K, x). (Here + means disjoint sum.) 16 17So there is a partition of x into 2-element sets, namely 18 19 {{h(Inl(i)), h(Inr(i))} . i \<in> K} 20 21So for all x \<in> s the desired partition exists. By AC1 (which follows from WO1) 22there exists a function f that chooses a partition for each x \<in> s. Therefore we 23have AC10(2). 24 25*) 26 27theory WO1_AC 28imports AC_Equiv 29begin 30 31(* ********************************************************************** *) 32(* WO1 ==> AC1 *) 33(* ********************************************************************** *) 34 35theorem WO1_AC1: "WO1 ==> AC1" 36by (unfold AC1_def WO1_def, fast elim!: ex_choice_fun) 37 38(* ********************************************************************** *) 39(* WO1 ==> AC10(n) (n >= 1) *) 40(* ********************************************************************** *) 41 42lemma lemma1: "[| WO1; \<forall>B \<in> A. \<exists>C \<in> D(B). P(C,B) |] ==> \<exists>f. \<forall>B \<in> A. P(f`B,B)" 43apply (unfold WO1_def) 44apply (erule_tac x = "\<Union>({{C \<in> D (B) . P (C,B) }. B \<in> A}) " in allE) 45apply (erule exE, drule ex_choice_fun, fast) 46apply (erule exE) 47apply (rule_tac x = "\<lambda>x \<in> A. f`{C \<in> D (x) . P (C,x) }" in exI) 48apply (simp, blast dest!: apply_type [OF _ RepFunI]) 49done 50 51lemma lemma2_1: "[| ~Finite(B); WO1 |] ==> |B| + |B| \<approx> B" 52apply (unfold WO1_def) 53apply (rule eqpoll_trans) 54prefer 2 apply (fast elim!: well_ord_cardinal_eqpoll) 55apply (rule eqpoll_sym [THEN eqpoll_trans]) 56apply (fast elim!: well_ord_cardinal_eqpoll) 57apply (drule spec [of _ B]) 58apply (clarify dest!: eqpoll_imp_Finite_iff [OF well_ord_cardinal_eqpoll]) 59apply (simp add: cadd_def [symmetric] 60 eqpoll_refl InfCard_cdouble_eq Card_cardinal Inf_Card_is_InfCard) 61done 62 63lemma lemma2_2: 64 "f \<in> bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i \<in> D} \<in> Pow(Pow(B))" 65by (fast elim!: bij_is_fun [THEN apply_type]) 66 67 68lemma lemma2_3: 69 "f \<in> bij(D+D, B) ==> pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i \<in> D})" 70apply (unfold pairwise_disjoint_def) 71apply (blast dest: bij_is_inj [THEN inj_apply_equality]) 72done 73 74lemma lemma2_4: 75 "[| f \<in> bij(D+D, B); 1\<le>n |] 76 ==> sets_of_size_between({{f`Inl(i), f`Inr(i)}. i \<in> D}, 2, succ(n))" 77apply (simp (no_asm_simp) add: sets_of_size_between_def succ_def) 78apply (blast intro!: cons_lepoll_cong 79 intro: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll] 80 le_imp_subset [THEN subset_imp_lepoll] lepoll_trans 81 dest: bij_is_inj [THEN inj_apply_equality] elim!: mem_irrefl) 82done 83 84lemma lemma2_5: 85 "f \<in> bij(D+D, B) ==> \<Union>({{f`Inl(i), f`Inr(i)}. i \<in> D})=B" 86apply (unfold bij_def surj_def) 87apply (fast elim!: inj_is_fun [THEN apply_type]) 88done 89 90lemma lemma2: 91 "[| WO1; ~Finite(B); 1\<le>n |] 92 ==> \<exists>C \<in> Pow(Pow(B)). pairwise_disjoint(C) & 93 sets_of_size_between(C, 2, succ(n)) & 94 \<Union>(C)=B" 95apply (drule lemma2_1 [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]], 96 assumption) 97apply (blast intro!: lemma2_2 lemma2_3 lemma2_4 lemma2_5) 98done 99 100theorem WO1_AC10: "[| WO1; 1\<le>n |] ==> AC10(n)" 101apply (unfold AC10_def) 102apply (fast intro!: lemma1 elim!: lemma2) 103done 104 105end 106 107