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