1(* Title: ZF/AC/AC_Equiv.thy 2 Author: Krzysztof Grabczewski 3 4Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II" 5by H. Rubin and J.E. Rubin, 1985. 6 7Axiom AC0 comes from "Axiomatic Set Theory" by P. Suppes, 1972. 8 9Some Isabelle proofs of equivalences of these axioms are formalizations of 10proofs presented by the Rubins. The others are based on the Rubins' proofs, 11but slightly changed. 12*) 13 14theory AC_Equiv 15imports ZF 16begin (*obviously not ZFC*) 17 18(* Well Ordering Theorems *) 19 20definition 21 "WO1 == \<forall>A. \<exists>R. well_ord(A,R)" 22 23definition 24 "WO2 == \<forall>A. \<exists>a. Ord(a) & A\<approx>a" 25 26definition 27 "WO3 == \<forall>A. \<exists>a. Ord(a) & (\<exists>b. b \<subseteq> a & A\<approx>b)" 28 29definition 30 "WO4(m) == \<forall>A. \<exists>a f. Ord(a) & domain(f)=a & 31 (\<Union>b<a. f`b) = A & (\<forall>b<a. f`b \<lesssim> m)" 32 33definition 34 "WO5 == \<exists>m \<in> nat. 1\<le>m & WO4(m)" 35 36definition 37 "WO6 == \<forall>A. \<exists>m \<in> nat. 1\<le>m & (\<exists>a f. Ord(a) & domain(f)=a 38 & (\<Union>b<a. f`b) = A & (\<forall>b<a. f`b \<lesssim> m))" 39 40definition 41 "WO7 == \<forall>A. Finite(A) \<longleftrightarrow> (\<forall>R. well_ord(A,R) \<longrightarrow> well_ord(A,converse(R)))" 42 43definition 44 "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Prod>X \<in> A. X)) \<longrightarrow> (\<exists>R. well_ord(A,R))" 45 46 47definition 48(* Auxiliary concepts needed below *) 49 pairwise_disjoint :: "i => o" where 50 "pairwise_disjoint(A) == \<forall>A1 \<in> A. \<forall>A2 \<in> A. A1 \<inter> A2 \<noteq> 0 \<longrightarrow> A1=A2" 51 52definition 53 sets_of_size_between :: "[i, i, i] => o" where 54 "sets_of_size_between(A,m,n) == \<forall>B \<in> A. m \<lesssim> B & B \<lesssim> n" 55 56 57(* Axioms of Choice *) 58definition 59 "AC0 == \<forall>A. \<exists>f. f \<in> (\<Prod>X \<in> Pow(A)-{0}. X)" 60 61definition 62 "AC1 == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Prod>X \<in> A. X))" 63 64definition 65 "AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A) 66 \<longrightarrow> (\<exists>C. \<forall>B \<in> A. \<exists>y. B \<inter> C = {y})" 67definition 68 "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Prod>x \<in> {a \<in> A. f`a\<noteq>0}. f`x)" 69 70definition 71 "AC4 == \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Prod>x \<in> domain(R). R``{x})))" 72 73definition 74 "AC5 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x" 75 76definition 77 "AC6 == \<forall>A. 0\<notin>A \<longrightarrow> (\<Prod>B \<in> A. B)\<noteq>0" 78 79definition 80 "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Prod>B \<in> A. B) \<noteq> 0" 81 82definition 83 "AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2) 84 \<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B \<in> bij(fst(B),snd(B)))" 85 86definition 87 "AC9 == \<forall>A. (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> 88 (\<exists>f. \<forall>B1 \<in> A. \<forall>B2 \<in> A. f`<B1,B2> \<in> bij(B1,B2))" 89 90definition 91 "AC10(n) == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) \<longrightarrow> 92 (\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) & 93 sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B))" 94 95definition 96 "AC11 == \<exists>n \<in> nat. 1\<le>n & AC10(n)" 97 98definition 99 "AC12 == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) \<longrightarrow> 100 (\<exists>n \<in> nat. 1\<le>n & (\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) & 101 sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B)))" 102 103definition 104 "AC13(m) == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 & f`B \<subseteq> B & f`B \<lesssim> m)" 105 106definition 107 "AC14 == \<exists>m \<in> nat. 1\<le>m & AC13(m)" 108 109definition 110 "AC15 == \<forall>A. 0\<notin>A \<longrightarrow> 111 (\<exists>m \<in> nat. 1\<le>m & (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 & f`B \<subseteq> B & f`B \<lesssim> m))" 112 113definition 114 "AC16(n, k) == 115 \<forall>A. ~Finite(A) \<longrightarrow> 116 (\<exists>T. T \<subseteq> {X \<in> Pow(A). X\<approx>succ(n)} & 117 (\<forall>X \<in> {X \<in> Pow(A). X\<approx>succ(k)}. \<exists>! Y. Y \<in> T & X \<subseteq> Y))" 118 119definition 120 "AC17 == \<forall>A. \<forall>g \<in> (Pow(A)-{0} -> A) -> Pow(A)-{0}. 121 \<exists>f \<in> Pow(A)-{0} -> A. f`(g`f) \<in> g`f" 122 123locale AC18 = 124 assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow> 125 ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) = 126 (\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))" 127 \<comment> \<open>AC18 cannot be expressed within the object-logic\<close> 128 129definition 130 "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) = 131 (\<Union>f \<in> (\<Prod>B \<in> A. B). \<Inter>a \<in> A. f`a))" 132 133 134 135(* ********************************************************************** *) 136(* Theorems concerning ordinals *) 137(* ********************************************************************** *) 138 139(* lemma for ordertype_Int *) 140lemma rvimage_id: "rvimage(A,id(A),r) = r \<inter> A*A" 141apply (unfold rvimage_def) 142apply (rule equalityI, safe) 143apply (drule_tac P = "%a. <id (A) `xb,a>:r" in id_conv [THEN subst], 144 assumption) 145apply (drule_tac P = "%a. <a,ya>:r" in id_conv [THEN subst], (assumption+)) 146apply (fast intro: id_conv [THEN ssubst]) 147done 148 149(* used only in Hartog.ML *) 150lemma ordertype_Int: 151 "well_ord(A,r) ==> ordertype(A, r \<inter> A*A) = ordertype(A,r)" 152apply (rule_tac P = "%a. ordertype (A,a) =ordertype (A,r) " in rvimage_id [THEN subst]) 153apply (erule id_bij [THEN bij_ordertype_vimage]) 154done 155 156lemma lam_sing_bij: "(\<lambda>x \<in> A. {x}) \<in> bij(A, {{x}. x \<in> A})" 157apply (rule_tac d = "%z. THE x. z={x}" in lam_bijective) 158apply (auto simp add: the_equality) 159done 160 161lemma inj_strengthen_type: 162 "[| f \<in> inj(A, B); !!a. a \<in> A ==> f`a \<in> C |] ==> f \<in> inj(A,C)" 163by (unfold inj_def, blast intro: Pi_type) 164 165(* ********************************************************************** *) 166(* Another elimination rule for \<exists>! *) 167(* ********************************************************************** *) 168 169lemma ex1_two_eq: "[| \<exists>! x. P(x); P(x); P(y) |] ==> x=y" 170by blast 171 172(* ********************************************************************** *) 173(* Lemmas used in the proofs like WO? ==> AC? *) 174(* ********************************************************************** *) 175 176lemma first_in_B: 177 "[| well_ord(\<Union>(A),r); 0 \<notin> A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B" 178by (blast dest!: well_ord_imp_ex1_first 179 [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]]) 180 181lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0 \<notin> A |] ==> \<exists>f. f \<in> (\<Prod>X \<in> A. X)" 182by (fast elim!: first_in_B intro!: lam_type) 183 184lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f \<in> (\<Prod>X \<in> Pow(A)-{0}. X)" 185by (fast elim!: well_ord_subset [THEN ex_choice_fun]) 186 187 188(* ********************************************************************** *) 189(* Lemmas needed to state when a finite relation is a function. *) 190(* The criteria are cardinalities of the relation and its domain. *) 191(* Used in WO6WO1.ML *) 192(* ********************************************************************** *) 193 194(*Using AC we could trivially prove, for all u, domain(u) \<lesssim> u*) 195lemma lepoll_m_imp_domain_lepoll_m: 196 "[| m \<in> nat; u \<lesssim> m |] ==> domain(u) \<lesssim> m" 197apply (unfold lepoll_def) 198apply (erule exE) 199apply (rule_tac x = "\<lambda>x \<in> domain(u). \<mu> i. \<exists>y. <x,y> \<in> u & f`<x,y> = i" 200 in exI) 201apply (rule_tac d = "%y. fst (converse(f) ` y) " in lam_injective) 202apply (fast intro: LeastI2 nat_into_Ord [THEN Ord_in_Ord] 203 inj_is_fun [THEN apply_type]) 204apply (erule domainE) 205apply (frule inj_is_fun [THEN apply_type], assumption) 206apply (rule LeastI2) 207apply (auto elim!: nat_into_Ord [THEN Ord_in_Ord]) 208done 209 210lemma rel_domain_ex1: 211 "[| succ(m) \<lesssim> domain(r); r \<lesssim> succ(m); m \<in> nat |] ==> function(r)" 212apply (unfold function_def, safe) 213apply (rule ccontr) 214apply (fast elim!: lepoll_trans [THEN succ_lepoll_natE] 215 lepoll_m_imp_domain_lepoll_m [OF _ Diff_sing_lepoll] 216 elim: domain_Diff_eq [OF _ not_sym, THEN subst]) 217done 218 219lemma rel_is_fun: 220 "[| succ(m) \<lesssim> domain(r); r \<lesssim> succ(m); m \<in> nat; 221 r \<subseteq> A*B; A=domain(r) |] ==> r \<in> A->B" 222by (simp add: Pi_iff rel_domain_ex1) 223 224end 225