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