57 (* Axioms of Choice *) |
57 (* Axioms of Choice *) |
58 definition |
58 definition |
59 "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)" |
59 "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)" |
60 |
60 |
61 definition |
61 definition |
62 "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))" |
62 "AC1 == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))" |
63 |
63 |
64 definition |
64 definition |
65 "AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A) |
65 "AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A) |
66 --> (\<exists>C. \<forall>B \<in> A. \<exists>y. B Int C = {y})" |
66 \<longrightarrow> (\<exists>C. \<forall>B \<in> A. \<exists>y. B \<inter> C = {y})" |
67 definition |
67 definition |
68 "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)" |
68 "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)" |
69 |
69 |
70 definition |
70 definition |
71 "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))" |
71 "AC4 == \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))" |
72 |
72 |
73 definition |
73 definition |
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" |
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 |
75 |
76 definition |
76 definition |
77 "AC6 == \<forall>A. 0\<notin>A --> (\<Pi> B \<in> A. B)\<noteq>0" |
77 "AC6 == \<forall>A. 0\<notin>A \<longrightarrow> (\<Pi> B \<in> A. B)\<noteq>0" |
78 |
78 |
79 definition |
79 definition |
80 "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi> B \<in> A. B) \<noteq> 0" |
80 "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Pi> B \<in> A. B) \<noteq> 0" |
81 |
81 |
82 definition |
82 definition |
83 "AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2) |
83 "AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2) |
84 --> (\<exists>f. \<forall>B \<in> A. f`B \<in> bij(fst(B),snd(B)))" |
84 \<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B \<in> bij(fst(B),snd(B)))" |
85 |
85 |
86 definition |
86 definition |
87 "AC9 == \<forall>A. (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> |
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))" |
88 (\<exists>f. \<forall>B1 \<in> A. \<forall>B2 \<in> A. f`<B1,B2> \<in> bij(B1,B2))" |
89 |
89 |
90 definition |
90 definition |
91 "AC10(n) == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) --> |
91 "AC10(n) == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) \<longrightarrow> |
92 (\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) & |
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))" |
93 sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B))" |
94 |
94 |
95 definition |
95 definition |
96 "AC11 == \<exists>n \<in> nat. 1\<le>n & AC10(n)" |
96 "AC11 == \<exists>n \<in> nat. 1\<le>n & AC10(n)" |
97 |
97 |
98 definition |
98 definition |
99 "AC12 == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) --> |
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) & |
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)))" |
101 sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B)))" |
102 |
102 |
103 definition |
103 definition |
104 "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)" |
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 |
105 |
106 definition |
106 definition |
107 "AC14 == \<exists>m \<in> nat. 1\<le>m & AC13(m)" |
107 "AC14 == \<exists>m \<in> nat. 1\<le>m & AC13(m)" |
108 |
108 |
109 definition |
109 definition |
110 "AC15 == \<forall>A. 0\<notin>A --> |
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))" |
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 |
112 |
113 definition |
113 definition |
114 "AC16(n, k) == |
114 "AC16(n, k) == |
115 \<forall>A. ~Finite(A) --> |
115 \<forall>A. ~Finite(A) \<longrightarrow> |
116 (\<exists>T. T \<subseteq> {X \<in> Pow(A). X\<approx>succ(n)} & |
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))" |
117 (\<forall>X \<in> {X \<in> Pow(A). X\<approx>succ(k)}. \<exists>! Y. Y \<in> T & X \<subseteq> Y))" |
118 |
118 |
119 definition |
119 definition |
120 "AC17 == \<forall>A. \<forall>g \<in> (Pow(A)-{0} -> A) -> Pow(A)-{0}. |
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" |
121 \<exists>f \<in> Pow(A)-{0} -> A. f`(g`f) \<in> g`f" |
122 |
122 |
123 locale AC18 = |
123 locale AC18 = |
124 assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) --> |
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)) = |
125 ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) = |
126 (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))" |
126 (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))" |
127 --"AC18 cannot be expressed within the object-logic" |
127 --"AC18 cannot be expressed within the object-logic" |
128 |
128 |
129 definition |
129 definition |
130 "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A --> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) = |
130 "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) = |
131 (\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))" |
131 (\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))" |
132 |
132 |
133 |
133 |
134 |
134 |
135 (* ********************************************************************** *) |
135 (* ********************************************************************** *) |
136 (* Theorems concerning ordinals *) |
136 (* Theorems concerning ordinals *) |
137 (* ********************************************************************** *) |
137 (* ********************************************************************** *) |
138 |
138 |
139 (* lemma for ordertype_Int *) |
139 (* lemma for ordertype_Int *) |
140 lemma rvimage_id: "rvimage(A,id(A),r) = r Int A*A" |
140 lemma rvimage_id: "rvimage(A,id(A),r) = r \<inter> A*A" |
141 apply (unfold rvimage_def) |
141 apply (unfold rvimage_def) |
142 apply (rule equalityI, safe) |
142 apply (rule equalityI, safe) |
143 apply (drule_tac P = "%a. <id (A) `xb,a>:r" in id_conv [THEN subst], |
143 apply (drule_tac P = "%a. <id (A) `xb,a>:r" in id_conv [THEN subst], |
144 assumption) |
144 assumption) |
145 apply (drule_tac P = "%a. <a,ya>:r" in id_conv [THEN subst], (assumption+)) |
145 apply (drule_tac P = "%a. <a,ya>:r" in id_conv [THEN subst], (assumption+)) |
146 apply (fast intro: id_conv [THEN ssubst]) |
146 apply (fast intro: id_conv [THEN ssubst]) |
147 done |
147 done |
148 |
148 |
149 (* used only in Hartog.ML *) |
149 (* used only in Hartog.ML *) |
150 lemma ordertype_Int: |
150 lemma ordertype_Int: |
151 "well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)" |
151 "well_ord(A,r) ==> ordertype(A, r \<inter> A*A) = ordertype(A,r)" |
152 apply (rule_tac P = "%a. ordertype (A,a) =ordertype (A,r) " in rvimage_id [THEN subst]) |
152 apply (rule_tac P = "%a. ordertype (A,a) =ordertype (A,r) " in rvimage_id [THEN subst]) |
153 apply (erule id_bij [THEN bij_ordertype_vimage]) |
153 apply (erule id_bij [THEN bij_ordertype_vimage]) |
154 done |
154 done |
155 |
155 |
156 lemma lam_sing_bij: "(\<lambda>x \<in> A. {x}) \<in> bij(A, {{x}. x \<in> A})" |
156 lemma lam_sing_bij: "(\<lambda>x \<in> A. {x}) \<in> bij(A, {{x}. x \<in> A})" |
189 (* ********************************************************************** *) |
189 (* ********************************************************************** *) |
190 (* Lemmas used in the proofs like WO? ==> AC? *) |
190 (* Lemmas used in the proofs like WO? ==> AC? *) |
191 (* ********************************************************************** *) |
191 (* ********************************************************************** *) |
192 |
192 |
193 lemma first_in_B: |
193 lemma first_in_B: |
194 "[| well_ord(Union(A),r); 0\<notin>A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B" |
194 "[| well_ord(\<Union>(A),r); 0\<notin>A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B" |
195 by (blast dest!: well_ord_imp_ex1_first |
195 by (blast dest!: well_ord_imp_ex1_first |
196 [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]]) |
196 [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]]) |
197 |
197 |
198 lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)" |
198 lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)" |
199 by (fast elim!: first_in_B intro!: lam_type) |
199 by (fast elim!: first_in_B intro!: lam_type) |
200 |
200 |
201 lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)" |
201 lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)" |
202 by (fast elim!: well_ord_subset [THEN ex_choice_fun]) |
202 by (fast elim!: well_ord_subset [THEN ex_choice_fun]) |
203 |
203 |