12776
|
1 |
(* Title: ZF/AC/AC15_WO6.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Krzysztof Grabczewski
|
|
4 |
|
|
5 |
The proofs needed to state that AC10, ..., AC15 are equivalent to the rest.
|
|
6 |
We need the following:
|
|
7 |
|
|
8 |
WO1 ==> AC10(n) ==> AC11 ==> AC12 ==> AC15 ==> WO6
|
|
9 |
|
|
10 |
In order to add the formulations AC13 and AC14 we need:
|
|
11 |
|
|
12 |
AC10(succ(n)) ==> AC13(n) ==> AC14 ==> AC15
|
|
13 |
|
|
14 |
or
|
|
15 |
|
|
16 |
AC1 ==> AC13(1); AC13(m) ==> AC13(n) ==> AC14 ==> AC15 (m\<le>n)
|
|
17 |
|
|
18 |
So we don't have to prove all implications of both cases.
|
|
19 |
Moreover we don't need to prove AC13(1) ==> AC1 and AC11 ==> AC14 as
|
|
20 |
Rubin & Rubin do.
|
|
21 |
*)
|
|
22 |
|
|
23 |
theory AC15_WO6 = HH + Cardinal_aux:
|
|
24 |
|
|
25 |
|
|
26 |
(* ********************************************************************** *)
|
|
27 |
(* Lemmas used in the proofs in which the conclusion is AC13, AC14 *)
|
|
28 |
(* or AC15 *)
|
|
29 |
(* - cons_times_nat_not_Finite *)
|
|
30 |
(* - ex_fun_AC13_AC15 *)
|
|
31 |
(* ********************************************************************** *)
|
|
32 |
|
|
33 |
lemma lepoll_Sigma: "A\<noteq>0 ==> B \<lesssim> A*B"
|
|
34 |
apply (unfold lepoll_def)
|
|
35 |
apply (erule not_emptyE)
|
|
36 |
apply (rule_tac x = "\<lambda>z \<in> B. <x,z>" in exI)
|
|
37 |
apply (fast intro!: snd_conv lam_injective)
|
|
38 |
done
|
|
39 |
|
|
40 |
lemma cons_times_nat_not_Finite:
|
|
41 |
"0\<notin>A ==> \<forall>B \<in> {cons(0,x*nat). x \<in> A}. ~Finite(B)"
|
|
42 |
apply clarify
|
|
43 |
apply (drule subset_consI [THEN subset_imp_lepoll, THEN lepoll_Finite])
|
|
44 |
apply (rule nat_not_Finite [THEN notE] )
|
|
45 |
apply (subgoal_tac "x ~= 0")
|
|
46 |
apply (blast intro: lepoll_Sigma [THEN lepoll_Finite] , blast)
|
|
47 |
done
|
|
48 |
|
|
49 |
lemma lemma1: "[| Union(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
|
|
50 |
by fast
|
|
51 |
|
|
52 |
lemma lemma2:
|
|
53 |
"[| pairwise_disjoint(A); B \<in> A; C \<in> A; a \<in> B; a \<in> C |] ==> B=C"
|
|
54 |
by (unfold pairwise_disjoint_def, blast)
|
|
55 |
|
|
56 |
lemma lemma3:
|
12788
|
57 |
"\<forall>B \<in> {cons(0, x*nat). x \<in> A}. pairwise_disjoint(f`B) &
|
|
58 |
sets_of_size_between(f`B, 2, n) & Union(f`B)=B
|
|
59 |
==> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) & u \<subseteq> cons(0, B*nat) &
|
|
60 |
0 \<in> u & 2 \<lesssim> u & u \<lesssim> n"
|
12776
|
61 |
apply (unfold sets_of_size_between_def)
|
|
62 |
apply (rule ballI)
|
12788
|
63 |
apply (erule_tac x="cons(0, B*nat)" in ballE)
|
|
64 |
apply (blast dest: lemma1 intro!: lemma2)
|
|
65 |
apply blast
|
12776
|
66 |
done
|
|
67 |
|
|
68 |
lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i"
|
|
69 |
apply (unfold lepoll_def)
|
|
70 |
apply (erule exE)
|
|
71 |
apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). LEAST j. \<exists>a\<in>A. x=P(a) & f`a=j"
|
|
72 |
in exI)
|
|
73 |
apply (rule_tac d = "%y. P (converse (f) `y) " in lam_injective)
|
|
74 |
apply (erule RepFunE)
|
|
75 |
apply (frule inj_is_fun [THEN apply_type], assumption)
|
|
76 |
apply (fast intro: LeastI2 elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
|
|
77 |
apply (erule RepFunE)
|
|
78 |
apply (rule LeastI2)
|
|
79 |
apply fast
|
|
80 |
apply (fast elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
|
|
81 |
apply (fast elim: sym left_inverse [THEN ssubst])
|
|
82 |
done
|
|
83 |
|
|
84 |
lemma lemma5_1:
|
|
85 |
"[| B \<in> A; 2 \<lesssim> u(B) |] ==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<noteq> 0"
|
|
86 |
apply simp
|
|
87 |
apply (fast dest: lepoll_Diff_sing
|
|
88 |
elim: lepoll_trans [THEN succ_lepoll_natE] ssubst
|
|
89 |
intro!: lepoll_refl)
|
|
90 |
done
|
|
91 |
|
|
92 |
lemma lemma5_2:
|
|
93 |
"[| B \<in> A; u(B) \<subseteq> cons(0, B*nat) |]
|
|
94 |
==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<subseteq> B"
|
|
95 |
apply auto
|
|
96 |
done
|
|
97 |
|
|
98 |
lemma lemma5_3:
|
|
99 |
"[| n \<in> nat; B \<in> A; 0 \<in> u(B); u(B) \<lesssim> succ(n) |]
|
|
100 |
==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<lesssim> n"
|
|
101 |
apply simp
|
|
102 |
apply (fast elim!: Diff_lepoll [THEN lemma4 [OF _ nat_into_Ord]])
|
|
103 |
done
|
|
104 |
|
|
105 |
lemma ex_fun_AC13_AC15:
|
|
106 |
"[| \<forall>B \<in> {cons(0, x*nat). x \<in> A}.
|
|
107 |
pairwise_disjoint(f`B) &
|
|
108 |
sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B;
|
|
109 |
n \<in> nat |]
|
|
110 |
==> \<exists>f. \<forall>B \<in> A. f`B \<noteq> 0 & f`B \<subseteq> B & f`B \<lesssim> n"
|
|
111 |
by (fast del: subsetI notI
|
|
112 |
dest!: lemma3 theI intro!: lemma5_1 lemma5_2 lemma5_3)
|
|
113 |
|
|
114 |
|
|
115 |
(* ********************************************************************** *)
|
|
116 |
(* The target proofs *)
|
|
117 |
(* ********************************************************************** *)
|
|
118 |
|
|
119 |
(* ********************************************************************** *)
|
|
120 |
(* AC10(n) ==> AC11 *)
|
|
121 |
(* ********************************************************************** *)
|
|
122 |
|
12788
|
123 |
theorem AC10_AC11: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC11"
|
12776
|
124 |
by (unfold AC10_def AC11_def, blast)
|
|
125 |
|
|
126 |
(* ********************************************************************** *)
|
|
127 |
(* AC11 ==> AC12 *)
|
|
128 |
(* ********************************************************************** *)
|
|
129 |
|
12788
|
130 |
theorem AC11_AC12: "AC11 ==> AC12"
|
12776
|
131 |
by (unfold AC10_def AC11_def AC11_def AC12_def, blast)
|
|
132 |
|
|
133 |
(* ********************************************************************** *)
|
|
134 |
(* AC12 ==> AC15 *)
|
|
135 |
(* ********************************************************************** *)
|
|
136 |
|
12788
|
137 |
theorem AC12_AC15: "AC12 ==> AC15"
|
12776
|
138 |
apply (unfold AC12_def AC15_def)
|
|
139 |
apply (blast del: ballI
|
|
140 |
intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15)
|
|
141 |
done
|
1123
|
142 |
|
12776
|
143 |
(* ********************************************************************** *)
|
|
144 |
(* AC15 ==> WO6 *)
|
|
145 |
(* ********************************************************************** *)
|
|
146 |
|
|
147 |
lemma OUN_eq_UN: "Ord(x) ==> (\<Union>a<x. F(a)) = (\<Union>a \<in> x. F(a))"
|
|
148 |
by (fast intro!: ltI dest!: ltD)
|
|
149 |
|
|
150 |
lemma lemma1:
|
|
151 |
"\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m
|
|
152 |
==> (\<Union>i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A"
|
|
153 |
apply (simp add: Ord_Least [THEN OUN_eq_UN])
|
|
154 |
apply (rule equalityI)
|
|
155 |
apply (fast dest!: less_Least_subset_x)
|
|
156 |
apply (blast del: subsetI
|
|
157 |
intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]])
|
|
158 |
done
|
|
159 |
|
|
160 |
lemma lemma2:
|
|
161 |
"\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m
|
|
162 |
==> \<forall>x < (LEAST x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
|
|
163 |
apply (rule oallI)
|
|
164 |
apply (drule ltD [THEN less_Least_subset_x])
|
|
165 |
apply (frule HH_subset_imp_eq)
|
|
166 |
apply (erule ssubst)
|
|
167 |
apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2])
|
|
168 |
(*but can't use del: DiffE despite the obvious conflictc*)
|
|
169 |
done
|
|
170 |
|
12788
|
171 |
theorem AC15_WO6: "AC15 ==> WO6"
|
12776
|
172 |
apply (unfold AC15_def WO6_def)
|
|
173 |
apply (rule allI)
|
|
174 |
apply (erule_tac x = "Pow (A) -{0}" in allE)
|
|
175 |
apply (erule impE, fast)
|
|
176 |
apply (elim bexE conjE exE)
|
|
177 |
apply (rule bexI)
|
|
178 |
apply (rule conjI, assumption)
|
|
179 |
apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI)
|
|
180 |
apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
|
|
181 |
apply simp
|
|
182 |
apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
|
|
183 |
elim!: less_Least_subset_x lemma1 lemma2, assumption);
|
|
184 |
done
|
|
185 |
|
|
186 |
|
|
187 |
(* ********************************************************************** *)
|
|
188 |
(* The proof needed in the first case, not in the second *)
|
|
189 |
(* ********************************************************************** *)
|
|
190 |
|
|
191 |
(* ********************************************************************** *)
|
|
192 |
(* AC10(n) ==> AC13(n-1) if 2\<le>n *)
|
|
193 |
(* *)
|
|
194 |
(* Because of the change to the formal definition of AC10(n) we prove *)
|
|
195 |
(* the following obviously equivalent theorem \<in> *)
|
|
196 |
(* AC10(n) implies AC13(n) for (1\<le>n) *)
|
|
197 |
(* ********************************************************************** *)
|
|
198 |
|
12788
|
199 |
theorem AC10_AC13: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC13(n)"
|
12776
|
200 |
apply (unfold AC10_def AC13_def, safe)
|
|
201 |
apply (erule allE)
|
|
202 |
apply (erule impE [OF _ cons_times_nat_not_Finite], assumption);
|
|
203 |
apply (fast elim!: impE [OF _ cons_times_nat_not_Finite]
|
|
204 |
dest!: ex_fun_AC13_AC15)
|
|
205 |
done
|
|
206 |
|
|
207 |
(* ********************************************************************** *)
|
|
208 |
(* The proofs needed in the second case, not in the first *)
|
|
209 |
(* ********************************************************************** *)
|
|
210 |
|
|
211 |
(* ********************************************************************** *)
|
|
212 |
(* AC1 ==> AC13(1) *)
|
|
213 |
(* ********************************************************************** *)
|
|
214 |
|
|
215 |
lemma AC1_AC13: "AC1 ==> AC13(1)"
|
|
216 |
apply (unfold AC1_def AC13_def)
|
|
217 |
apply (rule allI)
|
|
218 |
apply (erule allE)
|
|
219 |
apply (rule impI)
|
|
220 |
apply (drule mp, assumption)
|
|
221 |
apply (elim exE)
|
|
222 |
apply (rule_tac x = "\<lambda>x \<in> A. {f`x}" in exI)
|
|
223 |
apply (simp add: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll])
|
|
224 |
done
|
|
225 |
|
|
226 |
(* ********************************************************************** *)
|
|
227 |
(* AC13(m) ==> AC13(n) for m \<subseteq> n *)
|
|
228 |
(* ********************************************************************** *)
|
|
229 |
|
|
230 |
lemma AC13_mono: "[| m\<le>n; AC13(m) |] ==> AC13(n)"
|
|
231 |
apply (unfold AC13_def)
|
|
232 |
apply (drule le_imp_lepoll)
|
|
233 |
apply (fast elim!: lepoll_trans)
|
|
234 |
done
|
|
235 |
|
|
236 |
(* ********************************************************************** *)
|
|
237 |
(* The proofs necessary for both cases *)
|
|
238 |
(* ********************************************************************** *)
|
|
239 |
|
|
240 |
(* ********************************************************************** *)
|
|
241 |
(* AC13(n) ==> AC14 if 1 \<subseteq> n *)
|
|
242 |
(* ********************************************************************** *)
|
|
243 |
|
12788
|
244 |
theorem AC13_AC14: "[| n \<in> nat; 1\<le>n; AC13(n) |] ==> AC14"
|
12776
|
245 |
by (unfold AC13_def AC14_def, auto)
|
|
246 |
|
|
247 |
(* ********************************************************************** *)
|
|
248 |
(* AC14 ==> AC15 *)
|
|
249 |
(* ********************************************************************** *)
|
|
250 |
|
12788
|
251 |
theorem AC14_AC15: "AC14 ==> AC15"
|
12776
|
252 |
by (unfold AC13_def AC14_def AC15_def, fast)
|
|
253 |
|
|
254 |
(* ********************************************************************** *)
|
|
255 |
(* The redundant proofs; however cited by Rubin & Rubin *)
|
|
256 |
(* ********************************************************************** *)
|
|
257 |
|
|
258 |
(* ********************************************************************** *)
|
|
259 |
(* AC13(1) ==> AC1 *)
|
|
260 |
(* ********************************************************************** *)
|
|
261 |
|
|
262 |
lemma lemma_aux: "[| A\<noteq>0; A \<lesssim> 1 |] ==> \<exists>a. A={a}"
|
|
263 |
by (fast elim!: not_emptyE lepoll_1_is_sing)
|
|
264 |
|
|
265 |
lemma AC13_AC1_lemma:
|
|
266 |
"\<forall>B \<in> A. f(B)\<noteq>0 & f(B)<=B & f(B) \<lesssim> 1
|
|
267 |
==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Pi>X \<in> A. X)"
|
|
268 |
apply (rule lam_type)
|
|
269 |
apply (drule bspec, assumption)
|
|
270 |
apply (elim conjE)
|
|
271 |
apply (erule lemma_aux [THEN exE], assumption)
|
|
272 |
apply (simp add: the_element)
|
|
273 |
done
|
|
274 |
|
12788
|
275 |
theorem AC13_AC1: "AC13(1) ==> AC1"
|
12776
|
276 |
apply (unfold AC13_def AC1_def)
|
|
277 |
apply (fast elim!: AC13_AC1_lemma)
|
|
278 |
done
|
|
279 |
|
|
280 |
(* ********************************************************************** *)
|
|
281 |
(* AC11 ==> AC14 *)
|
|
282 |
(* ********************************************************************** *)
|
|
283 |
|
12788
|
284 |
theorem AC11_AC14: "AC11 ==> AC14"
|
12776
|
285 |
apply (unfold AC11_def AC14_def)
|
|
286 |
apply (fast intro!: AC10_AC13)
|
|
287 |
done
|
|
288 |
|
|
289 |
end
|
|
290 |
|