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