author | paulson <lp15@cam.ac.uk> |
Tue, 27 Sep 2022 17:46:52 +0100 | |
changeset 76215 | a642599ffdea |
parent 76214 | 0c18df79b1c8 |
child 76216 | 9fc34f76b4e8 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/AC/AC_Equiv.thy |
2 |
Author: Krzysztof Grabczewski |
|
991 | 3 |
|
4 |
Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II" |
|
5 |
by H. Rubin and J.E. Rubin, 1985. |
|
6 |
||
7 |
Axiom AC0 comes from "Axiomatic Set Theory" by P. Suppes, 1972. |
|
8 |
||
9 |
Some Isabelle proofs of equivalences of these axioms are formalizations of |
|
1123 | 10 |
proofs presented by the Rubins. The others are based on the Rubins' proofs, |
11 |
but slightly changed. |
|
991 | 12 |
*) |
13 |
||
27678 | 14 |
theory AC_Equiv |
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
61980
diff
changeset
|
15 |
imports ZF |
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
61980
diff
changeset
|
16 |
begin (*obviously not ZFC*) |
8123 | 17 |
|
991 | 18 |
(* Well Ordering Theorems *) |
24893 | 19 |
|
20 |
definition |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
21 |
"WO1 \<equiv> \<forall>A. \<exists>R. well_ord(A,R)" |
12776 | 22 |
|
24893 | 23 |
definition |
76214 | 24 |
"WO2 \<equiv> \<forall>A. \<exists>a. Ord(a) \<and> A\<approx>a" |
991 | 25 |
|
24893 | 26 |
definition |
76214 | 27 |
"WO3 \<equiv> \<forall>A. \<exists>a. Ord(a) \<and> (\<exists>b. b \<subseteq> a \<and> A\<approx>b)" |
1123 | 28 |
|
24893 | 29 |
definition |
76214 | 30 |
"WO4(m) \<equiv> \<forall>A. \<exists>a f. Ord(a) \<and> domain(f)=a \<and> |
31 |
(\<Union>b<a. f`b) = A \<and> (\<forall>b<a. f`b \<lesssim> m)" |
|
991 | 32 |
|
24893 | 33 |
definition |
76214 | 34 |
"WO5 \<equiv> \<exists>m \<in> nat. 1\<le>m \<and> WO4(m)" |
991 | 35 |
|
24893 | 36 |
definition |
76214 | 37 |
"WO6 \<equiv> \<forall>A. \<exists>m \<in> nat. 1\<le>m \<and> (\<exists>a f. Ord(a) \<and> domain(f)=a |
38 |
\<and> (\<Union>b<a. f`b) = A \<and> (\<forall>b<a. f`b \<lesssim> m))" |
|
991 | 39 |
|
24893 | 40 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
41 |
"WO7 \<equiv> \<forall>A. Finite(A) \<longleftrightarrow> (\<forall>R. well_ord(A,R) \<longrightarrow> well_ord(A,converse(R)))" |
991 | 42 |
|
24893 | 43 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
44 |
"WO8 \<equiv> \<forall>A. (\<exists>f. f \<in> (\<Prod>X \<in> A. X)) \<longrightarrow> (\<exists>R. well_ord(A,R))" |
991 | 45 |
|
46 |
||
24893 | 47 |
definition |
12776 | 48 |
(* Auxiliary concepts needed below *) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
49 |
pairwise_disjoint :: "i \<Rightarrow> o" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
50 |
"pairwise_disjoint(A) \<equiv> \<forall>A1 \<in> A. \<forall>A2 \<in> A. A1 \<inter> A2 \<noteq> 0 \<longrightarrow> A1=A2" |
991 | 51 |
|
24893 | 52 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
53 |
sets_of_size_between :: "[i, i, i] \<Rightarrow> o" where |
76214 | 54 |
"sets_of_size_between(A,m,n) \<equiv> \<forall>B \<in> A. m \<lesssim> B \<and> B \<lesssim> n" |
12776 | 55 |
|
991 | 56 |
|
57 |
(* Axioms of Choice *) |
|
24893 | 58 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
59 |
"AC0 \<equiv> \<forall>A. \<exists>f. f \<in> (\<Prod>X \<in> Pow(A)-{0}. X)" |
991 | 60 |
|
24893 | 61 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
62 |
"AC1 \<equiv> \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Prod>X \<in> A. X))" |
12776 | 63 |
|
24893 | 64 |
definition |
76214 | 65 |
"AC2 \<equiv> \<forall>A. 0\<notin>A \<and> pairwise_disjoint(A) |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
66 |
\<longrightarrow> (\<exists>C. \<forall>B \<in> A. \<exists>y. B \<inter> C = {y})" |
24893 | 67 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
68 |
"AC3 \<equiv> \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Prod>x \<in> {a \<in> A. f`a\<noteq>0}. f`x)" |
991 | 69 |
|
24893 | 70 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
71 |
"AC4 \<equiv> \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Prod>x \<in> domain(R). R``{x})))" |
12776 | 72 |
|
24893 | 73 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
74 |
"AC5 \<equiv> \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x" |
12776 | 75 |
|
24893 | 76 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
77 |
"AC6 \<equiv> \<forall>A. 0\<notin>A \<longrightarrow> (\<Prod>B \<in> A. B)\<noteq>0" |
991 | 78 |
|
24893 | 79 |
definition |
76214 | 80 |
"AC7 \<equiv> \<forall>A. 0\<notin>A \<and> (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Prod>B \<in> A. B) \<noteq> 0" |
991 | 81 |
|
24893 | 82 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
83 |
"AC8 \<equiv> \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=\<langle>B1,B2\<rangle> \<and> B1\<approx>B2) |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
84 |
\<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B \<in> bij(fst(B),snd(B)))" |
12776 | 85 |
|
24893 | 86 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
87 |
"AC9 \<equiv> \<forall>A. (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
88 |
(\<exists>f. \<forall>B1 \<in> A. \<forall>B2 \<in> A. f`\<langle>B1,B2\<rangle> \<in> bij(B1,B2))" |
991 | 89 |
|
24893 | 90 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
91 |
"AC10(n) \<equiv> \<forall>A. (\<forall>B \<in> A. \<not>Finite(B)) \<longrightarrow> |
76214 | 92 |
(\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) \<and> |
93 |
sets_of_size_between(f`B, 2, succ(n)) \<and> \<Union>(f`B)=B))" |
|
991 | 94 |
|
24893 | 95 |
definition |
76214 | 96 |
"AC11 \<equiv> \<exists>n \<in> nat. 1\<le>n \<and> AC10(n)" |
12776 | 97 |
|
24893 | 98 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
99 |
"AC12 \<equiv> \<forall>A. (\<forall>B \<in> A. \<not>Finite(B)) \<longrightarrow> |
76214 | 100 |
(\<exists>n \<in> nat. 1\<le>n \<and> (\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) \<and> |
101 |
sets_of_size_between(f`B, 2, succ(n)) \<and> \<Union>(f`B)=B)))" |
|
991 | 102 |
|
24893 | 103 |
definition |
76214 | 104 |
"AC13(m) \<equiv> \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 \<and> f`B \<subseteq> B \<and> f`B \<lesssim> m)" |
12776 | 105 |
|
24893 | 106 |
definition |
76214 | 107 |
"AC14 \<equiv> \<exists>m \<in> nat. 1\<le>m \<and> AC13(m)" |
12776 | 108 |
|
24893 | 109 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
110 |
"AC15 \<equiv> \<forall>A. 0\<notin>A \<longrightarrow> |
76214 | 111 |
(\<exists>m \<in> nat. 1\<le>m \<and> (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 \<and> f`B \<subseteq> B \<and> f`B \<lesssim> m))" |
991 | 112 |
|
24893 | 113 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
114 |
"AC16(n, k) \<equiv> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
115 |
\<forall>A. \<not>Finite(A) \<longrightarrow> |
76214 | 116 |
(\<exists>T. T \<subseteq> {X \<in> Pow(A). X\<approx>succ(n)} \<and> |
117 |
(\<forall>X \<in> {X \<in> Pow(A). X\<approx>succ(k)}. \<exists>! Y. Y \<in> T \<and> X \<subseteq> Y))" |
|
991 | 118 |
|
24893 | 119 |
definition |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
120 |
"AC17 \<equiv> \<forall>A. \<forall>g \<in> (Pow(A)-{0} -> A) -> Pow(A)-{0}. |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
121 |
\<exists>f \<in> Pow(A)-{0} -> A. f`(g`f) \<in> g`f" |
991 | 122 |
|
13416 | 123 |
locale AC18 = |
76214 | 124 |
assumes AC18: "A\<noteq>0 \<and> (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow> |
13416 | 125 |
((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) = |
61980 | 126 |
(\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
65449
diff
changeset
|
127 |
\<comment> \<open>AC18 cannot be expressed within the object-logic\<close> |
12776 | 128 |
|
24893 | 129 |
definition |
76214 | 130 |
"AC19 \<equiv> \<forall>A. A\<noteq>0 \<and> 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) = |
61980 | 131 |
(\<Union>f \<in> (\<Prod>B \<in> A. B). \<Inter>a \<in> A. f`a))" |
12776 | 132 |
|
133 |
||
991 | 134 |
|
12776 | 135 |
(* ********************************************************************** *) |
136 |
(* Theorems concerning ordinals *) |
|
137 |
(* ********************************************************************** *) |
|
991 | 138 |
|
12776 | 139 |
(* lemma for ordertype_Int *) |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
140 |
lemma rvimage_id: "rvimage(A,id(A),r) = r \<inter> A*A" |
12776 | 141 |
apply (unfold rvimage_def) |
142 |
apply (rule equalityI, safe) |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
143 |
apply (drule_tac P = "\<lambda>a. <id (A) `xb,a>:r" in id_conv [THEN subst], |
12820 | 144 |
assumption) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
145 |
apply (drule_tac P = "\<lambda>a. \<langle>a,ya\<rangle>:r" in id_conv [THEN subst], (assumption+)) |
12776 | 146 |
apply (fast intro: id_conv [THEN ssubst]) |
147 |
done |
|
991 | 148 |
|
12776 | 149 |
(* used only in Hartog.ML *) |
150 |
lemma ordertype_Int: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
151 |
"well_ord(A,r) \<Longrightarrow> ordertype(A, r \<inter> A*A) = ordertype(A,r)" |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
152 |
apply (rule_tac P = "\<lambda>a. ordertype (A,a) =ordertype (A,r) " in rvimage_id [THEN subst]) |
12776 | 153 |
apply (erule id_bij [THEN bij_ordertype_vimage]) |
154 |
done |
|
155 |
||
156 |
lemma lam_sing_bij: "(\<lambda>x \<in> A. {x}) \<in> bij(A, {{x}. x \<in> A})" |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
157 |
apply (rule_tac d = "\<lambda>z. THE x. z={x}" in lam_bijective) |
12814 | 158 |
apply (auto simp add: the_equality) |
12776 | 159 |
done |
160 |
||
161 |
lemma inj_strengthen_type: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
162 |
"\<lbrakk>f \<in> inj(A, B); \<And>a. a \<in> A \<Longrightarrow> f`a \<in> C\<rbrakk> \<Longrightarrow> f \<in> inj(A,C)" |
12776 | 163 |
by (unfold inj_def, blast intro: Pi_type) |
164 |
||
165 |
(* ********************************************************************** *) |
|
166 |
(* Another elimination rule for \<exists>! *) |
|
167 |
(* ********************************************************************** *) |
|
168 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
169 |
lemma ex1_two_eq: "\<lbrakk>\<exists>! x. P(x); P(x); P(y)\<rbrakk> \<Longrightarrow> x=y" |
12776 | 170 |
by blast |
991 | 171 |
|
12776 | 172 |
(* ********************************************************************** *) |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
173 |
(* Lemmas used in the proofs like WO? \<Longrightarrow> AC? *) |
12776 | 174 |
(* ********************************************************************** *) |
991 | 175 |
|
12776 | 176 |
lemma first_in_B: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
177 |
"\<lbrakk>well_ord(\<Union>(A),r); 0 \<notin> A; B \<in> A\<rbrakk> \<Longrightarrow> (THE b. first(b,B,r)) \<in> B" |
12776 | 178 |
by (blast dest!: well_ord_imp_ex1_first |
179 |
[THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]]) |
|
180 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
181 |
lemma ex_choice_fun: "\<lbrakk>well_ord(\<Union>(A), R); 0 \<notin> A\<rbrakk> \<Longrightarrow> \<exists>f. f \<in> (\<Prod>X \<in> A. X)" |
12776 | 182 |
by (fast elim!: first_in_B intro!: lam_type) |
991 | 183 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
184 |
lemma ex_choice_fun_Pow: "well_ord(A, R) \<Longrightarrow> \<exists>f. f \<in> (\<Prod>X \<in> Pow(A)-{0}. X)" |
12776 | 185 |
by (fast elim!: well_ord_subset [THEN ex_choice_fun]) |
186 |
||
991 | 187 |
|
12776 | 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 |
(* ********************************************************************** *) |
|
991 | 193 |
|
12776 | 194 |
(*Using AC we could trivially prove, for all u, domain(u) \<lesssim> u*) |
195 |
lemma lepoll_m_imp_domain_lepoll_m: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
196 |
"\<lbrakk>m \<in> nat; u \<lesssim> m\<rbrakk> \<Longrightarrow> domain(u) \<lesssim> m" |
12776 | 197 |
apply (unfold lepoll_def) |
198 |
apply (erule exE) |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
199 |
apply (rule_tac x = "\<lambda>x \<in> domain(u). \<mu> i. \<exists>y. \<langle>x,y\<rangle> \<in> u \<and> f`\<langle>x,y\<rangle> = i" |
12776 | 200 |
in exI) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
201 |
apply (rule_tac d = "\<lambda>y. fst (converse(f) ` y) " in lam_injective) |
12776 | 202 |
apply (fast intro: LeastI2 nat_into_Ord [THEN Ord_in_Ord] |
203 |
inj_is_fun [THEN apply_type]) |
|
204 |
apply (erule domainE) |
|
12820 | 205 |
apply (frule inj_is_fun [THEN apply_type], assumption) |
12776 | 206 |
apply (rule LeastI2) |
207 |
apply (auto elim!: nat_into_Ord [THEN Ord_in_Ord]) |
|
208 |
done |
|
991 | 209 |
|
12776 | 210 |
lemma rel_domain_ex1: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
211 |
"\<lbrakk>succ(m) \<lesssim> domain(r); r \<lesssim> succ(m); m \<in> nat\<rbrakk> \<Longrightarrow> function(r)" |
12776 | 212 |
apply (unfold function_def, safe) |
213 |
apply (rule ccontr) |
|
214 |
apply (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]) |
|
217 |
done |
|
218 |
||
219 |
lemma rel_is_fun: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
220 |
"\<lbrakk>succ(m) \<lesssim> domain(r); r \<lesssim> succ(m); m \<in> nat; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
221 |
r \<subseteq> A*B; A=domain(r)\<rbrakk> \<Longrightarrow> r \<in> A->B" |
12776 | 222 |
by (simp add: Pi_iff rel_domain_ex1) |
223 |
||
991 | 224 |
end |