1(* Title: ZF/AC/Cardinal_aux.thy 2 Author: Krzysztof Grabczewski 3 4Auxiliary lemmas concerning cardinalities. 5*) 6 7theory Cardinal_aux imports AC_Equiv begin 8 9lemma Diff_lepoll: "[| A \<lesssim> succ(m); B \<subseteq> A; B\<noteq>0 |] ==> A-B \<lesssim> m" 10apply (rule not_emptyE, assumption) 11apply (blast intro: lepoll_trans [OF subset_imp_lepoll Diff_sing_lepoll]) 12done 13 14 15(* ********************************************************************** *) 16(* Lemmas involving ordinals and cardinalities used in the proofs *) 17(* concerning AC16 and DC *) 18(* ********************************************************************** *) 19 20 21(* j=|A| *) 22lemma lepoll_imp_ex_le_eqpoll: 23 "[| A \<lesssim> i; Ord(i) |] ==> \<exists>j. j \<le> i & A \<approx> j" 24by (blast intro!: lepoll_cardinal_le well_ord_Memrel 25 well_ord_cardinal_eqpoll [THEN eqpoll_sym] 26 dest: lepoll_well_ord) 27 28(* j=|A| *) 29lemma lesspoll_imp_ex_lt_eqpoll: 30 "[| A \<prec> i; Ord(i) |] ==> \<exists>j. j<i & A \<approx> j" 31by (unfold lesspoll_def, blast dest!: lepoll_imp_ex_le_eqpoll elim!: leE) 32 33lemma Un_eqpoll_Inf_Ord: 34 assumes A: "A \<approx> i" and B: "B \<approx> i" and NFI: "\<not> Finite(i)" and i: "Ord(i)" 35 shows "A \<union> B \<approx> i" 36proof (rule eqpollI) 37 have AB: "A \<approx> B" using A B by (blast intro: eqpoll_sym eqpoll_trans) 38 have "2 \<lesssim> nat" 39 by (rule subset_imp_lepoll) (rule OrdmemD [OF nat_2I Ord_nat]) 40 also have "... \<lesssim> i" 41 by (simp add: nat_le_infinite_Ord le_imp_lepoll NFI i)+ 42 also have "... \<approx> A" by (blast intro: eqpoll_sym A) 43 finally have "2 \<lesssim> A" . 44 have ICI: "InfCard(|i|)" 45 by (simp add: Inf_Card_is_InfCard Finite_cardinal_iff NFI i) 46 have "A \<union> B \<lesssim> A + B" by (rule Un_lepoll_sum) 47 also have "... \<lesssim> A \<times> B" 48 by (rule lepoll_imp_sum_lepoll_prod [OF AB [THEN eqpoll_imp_lepoll] \<open>2 \<lesssim> A\<close>]) 49 also have "... \<approx> i \<times> i" 50 by (blast intro: prod_eqpoll_cong eqpoll_imp_lepoll A B) 51 also have "... \<approx> i" 52 by (blast intro: well_ord_InfCard_square_eq well_ord_Memrel ICI i) 53 finally show "A \<union> B \<lesssim> i" . 54next 55 have "i \<approx> A" by (blast intro: A eqpoll_sym) 56 also have "... \<lesssim> A \<union> B" by (blast intro: subset_imp_lepoll) 57 finally show "i \<lesssim> A \<union> B" . 58qed 59 60schematic_goal paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)" 61apply (rule RepFun_bijective) 62apply (simp add: doubleton_eq_iff, blast) 63done 64 65lemma paired_eqpoll: "{{y,z}. y \<in> x} \<approx> x" 66by (unfold eqpoll_def, fast intro!: paired_bij) 67 68lemma ex_eqpoll_disjoint: "\<exists>B. B \<approx> A & B \<inter> C = 0" 69by (fast intro!: paired_eqpoll equals0I elim: mem_asym) 70 71(*Finally we reach this result. Surely there's a simpler proof?*) 72lemma Un_lepoll_Inf_Ord: 73 "[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<lesssim> i" 74apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE]) 75apply (erule conjE) 76apply (drule lepoll_trans) 77apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) 78apply (rule Un_lepoll_Un [THEN lepoll_trans], (assumption+)) 79apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll) 80done 81 82lemma Least_in_Ord: "[| P(i); i \<in> j; Ord(j) |] ==> (\<mu> i. P(i)) \<in> j" 83apply (erule Least_le [THEN leE]) 84apply (erule Ord_in_Ord, assumption) 85apply (erule ltE) 86apply (fast dest: OrdmemD) 87apply (erule subst_elem, assumption) 88done 89 90lemma Diff_first_lepoll: 91 "[| well_ord(x,r); y \<subseteq> x; y \<lesssim> succ(n); n \<in> nat |] 92 ==> y - {THE b. first(b,y,r)} \<lesssim> n" 93apply (case_tac "y=0", simp add: empty_lepollI) 94apply (fast intro!: Diff_sing_lepoll the_first_in) 95done 96 97lemma UN_subset_split: 98 "(\<Union>x \<in> X. P(x)) \<subseteq> (\<Union>x \<in> X. P(x)-Q(x)) \<union> (\<Union>x \<in> X. Q(x))" 99by blast 100 101lemma UN_sing_lepoll: "Ord(a) ==> (\<Union>x \<in> a. {P(x)}) \<lesssim> a" 102apply (unfold lepoll_def) 103apply (rule_tac x = "\<lambda>z \<in> (\<Union>x \<in> a. {P (x) }) . (\<mu> i. P (i) =z) " in exI) 104apply (rule_tac d = "%z. P (z) " in lam_injective) 105apply (fast intro!: Least_in_Ord) 106apply (fast intro: LeastI elim!: Ord_in_Ord) 107done 108 109lemma UN_fun_lepoll_lemma [rule_format]: 110 "[| well_ord(T, R); ~Finite(a); Ord(a); n \<in> nat |] 111 ==> \<forall>f. (\<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T) \<longrightarrow> (\<Union>b \<in> a. f`b) \<lesssim> a" 112apply (induct_tac "n") 113apply (rule allI) 114apply (rule impI) 115apply (rule_tac b = "\<Union>b \<in> a. f`b" in subst) 116apply (rule_tac [2] empty_lepollI) 117apply (rule equals0I [symmetric], clarify) 118apply (fast dest: lepoll_0_is_0 [THEN subst]) 119apply (rule allI) 120apply (rule impI) 121apply (erule_tac x = "\<lambda>x \<in> a. f`x - {THE b. first (b,f`x,R) }" in allE) 122apply (erule impE, simp) 123apply (fast intro!: Diff_first_lepoll, simp) 124apply (rule UN_subset_split [THEN subset_imp_lepoll, THEN lepoll_trans]) 125apply (fast intro: Un_lepoll_Inf_Ord UN_sing_lepoll) 126done 127 128lemma UN_fun_lepoll: 129 "[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R); 130 ~Finite(a); Ord(a); n \<in> nat |] ==> (\<Union>b \<in> a. f`b) \<lesssim> a" 131by (blast intro: UN_fun_lepoll_lemma) 132 133lemma UN_lepoll: 134 "[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R); 135 ~Finite(a); Ord(a); n \<in> nat |] 136 ==> (\<Union>b \<in> a. F(b)) \<lesssim> a" 137apply (rule rev_mp) 138apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll) 139apply auto 140done 141 142lemma UN_eq_UN_Diffs: 143 "Ord(a) ==> (\<Union>b \<in> a. F(b)) = (\<Union>b \<in> a. F(b) - (\<Union>c \<in> b. F(c)))" 144apply (rule equalityI) 145 prefer 2 apply fast 146apply (rule subsetI) 147apply (erule UN_E) 148apply (rule UN_I) 149 apply (rule_tac P = "%z. x \<in> F (z) " in Least_in_Ord, (assumption+)) 150apply (rule DiffI, best intro: Ord_in_Ord LeastI, clarify) 151apply (erule_tac P = "%z. x \<in> F (z) " and i = c in less_LeastE) 152apply (blast intro: Ord_Least ltI) 153done 154 155lemma lepoll_imp_eqpoll_subset: 156 "a \<lesssim> X ==> \<exists>Y. Y \<subseteq> X & a \<approx> Y" 157apply (unfold lepoll_def eqpoll_def, clarify) 158apply (blast intro: restrict_bij 159 dest: inj_is_fun [THEN fun_is_rel, THEN image_subset]) 160done 161 162(* ********************************************************************** *) 163(* Diff_lesspoll_eqpoll_Card *) 164(* ********************************************************************** *) 165 166lemma Diff_lesspoll_eqpoll_Card_lemma: 167 "[| A\<approx>a; ~Finite(a); Card(a); B \<prec> a; A-B \<prec> a |] ==> P" 168apply (elim lesspoll_imp_ex_lt_eqpoll [THEN exE] Card_is_Ord conjE) 169apply (frule_tac j=xa in Un_upper1_le [OF lt_Ord lt_Ord], assumption) 170apply (frule_tac j=xa in Un_upper2_le [OF lt_Ord lt_Ord], assumption) 171apply (drule Un_least_lt, assumption) 172apply (drule eqpoll_imp_lepoll [THEN lepoll_trans], 173 rule le_imp_lepoll, assumption)+ 174apply (case_tac "Finite(x \<union> xa)") 175txt\<open>finite case\<close> 176 apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+) 177 apply (drule subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_Finite]) 178 apply (fast dest: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_Finite]) 179txt\<open>infinite case\<close> 180apply (drule Un_lepoll_Inf_Ord, (assumption+)) 181apply (blast intro: le_Ord2) 182apply (drule lesspoll_trans1 183 [OF subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_trans] 184 lt_Card_imp_lesspoll], assumption+) 185apply (simp add: lesspoll_def) 186done 187 188lemma Diff_lesspoll_eqpoll_Card: 189 "[| A \<approx> a; ~Finite(a); Card(a); B \<prec> a |] ==> A - B \<approx> a" 190apply (rule ccontr) 191apply (rule Diff_lesspoll_eqpoll_Card_lemma, (assumption+)) 192apply (blast intro: lesspoll_def [THEN def_imp_iff, THEN iffD2] 193 subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans) 194done 195 196end 197