1 (* Title: ZF/AC/AC16_WO4.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Grabczewski |
|
4 |
|
5 The proof of AC16(n, k) ==> WO4(n-k) |
|
6 *) |
|
7 |
|
8 (* ********************************************************************** *) |
|
9 (* The case of finite set *) |
|
10 (* ********************************************************************** *) |
|
11 |
|
12 Goalw [Finite_def] "[| Finite(A); 0<m; m \\<in> nat |] ==> \ |
|
13 \ \\<exists>a f. Ord(a) & domain(f) = a & \ |
|
14 \ (\\<Union>b<a. f`b) = A & (\\<forall>b<a. f`b lepoll m)"; |
|
15 by (etac bexE 1); |
|
16 by (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1); |
|
17 by (etac exE 1); |
|
18 by (res_inst_tac [("x","n")] exI 1); |
|
19 by (res_inst_tac [("x","\\<lambda>i \\<in> n. {f`i}")] exI 1); |
|
20 by (Asm_full_simp_tac 1); |
|
21 by (rewrite_goals_tac [bij_def, surj_def]); |
|
22 by (fast_tac (claset() addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun, |
|
23 equalityI, singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
|
24 nat_1_lepoll_iff RS iffD2] |
|
25 addSEs [apply_type, ltE]) 1); |
|
26 val lemma1 = result(); |
|
27 |
|
28 (* ********************************************************************** *) |
|
29 (* The case of infinite set *) |
|
30 (* ********************************************************************** *) |
|
31 |
|
32 (* well_ord(x,r) ==> well_ord({{y,z}. y \\<in> x}, Something(x,z)) **) |
|
33 bind_thm ("well_ord_paired", (paired_bij RS bij_is_inj RS well_ord_rvimage)); |
|
34 |
|
35 Goal "[| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C"; |
|
36 by (fast_tac (claset() addEs [notE, lepoll_trans]) 1); |
|
37 qed "lepoll_trans1"; |
|
38 |
|
39 (* ********************************************************************** *) |
|
40 (* There exists a well ordered set y such that ... *) |
|
41 (* ********************************************************************** *) |
|
42 |
|
43 val lepoll_paired = paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll; |
|
44 |
|
45 Goal "\\<exists>y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)"; |
|
46 by (res_inst_tac [("x","{{a,x}. a \\<in> nat Un Hartog(z)}")] exI 1); |
|
47 by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS |
|
48 (Ord_Hartog RS |
|
49 well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); |
|
50 by (fast_tac |
|
51 (claset() addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, |
|
52 HartogI RSN (2, lepoll_trans1), |
|
53 subset_imp_lepoll RS (lepoll_paired RSN (2, lepoll_trans))] |
|
54 addSEs [nat_not_Finite RS notE] addEs [mem_asym] |
|
55 addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite, |
|
56 lepoll_paired RS lepoll_Finite]) 1); |
|
57 val lemma2 = result(); |
|
58 |
|
59 Goal "~Finite(B) ==> ~Finite(A Un B)"; |
|
60 by (blast_tac (claset() addIs [subset_Finite]) 1); |
|
61 qed "infinite_Un"; |
|
62 |
|
63 (* ********************************************************************** *) |
|
64 (* There is a v \\<in> s(u) such that k lepoll x Int y (in our case succ(k)) *) |
|
65 (* The idea of the proof is the following \\<in> *) |
|
66 (* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y *) |
|
67 (* Thence y is less than or equipollent to {v \\<in> Pow(x). v eqpoll n#-k} *) |
|
68 (* We have obtained this result in two steps \\<in> *) |
|
69 (* 1. y is less than or equipollent to {v \\<in> s(u). a \\<subseteq> v} *) |
|
70 (* where a is certain k-2 element subset of y *) |
|
71 (* 2. {v \\<in> s(u). a \\<subseteq> v} is less than or equipollent *) |
|
72 (* to {v \\<in> Pow(x). v eqpoll n-k} *) |
|
73 (* ********************************************************************** *) |
|
74 |
|
75 (*Proof simplified by LCP*) |
|
76 Goal "[| ~(\\<exists>x \\<in> A. f`x=y); f \\<in> inj(A, B); y \\<in> B |] \ |
|
77 \ ==> (\\<lambda>a \\<in> succ(A). if(a=A, y, f`a)) \\<in> inj(succ(A), B)"; |
|
78 by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); |
|
79 by (force_tac (claset(), simpset() addsimps [inj_is_fun RS apply_type]) 1); |
|
80 (*this preliminary simplification prevents looping somehow*) |
|
81 by (Asm_simp_tac 1); |
|
82 by (force_tac (claset(), simpset() addsimps []) 1); |
|
83 qed "succ_not_lepoll_lemma"; |
|
84 |
|
85 Goalw [lepoll_def, eqpoll_def, bij_def, surj_def] |
|
86 "[| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; |
|
87 by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |
|
88 qed "succ_not_lepoll_imp_eqpoll"; |
|
89 |
|
90 |
|
91 (* ********************************************************************** *) |
|
92 (* There is a k-2 element subset of y *) |
|
93 (* ********************************************************************** *) |
|
94 |
|
95 val ordertype_eqpoll = |
|
96 ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2)); |
|
97 |
|
98 Goal "[| a \\<subseteq> y; b \\<in> y-a; u \\<in> x |] ==> cons(b, cons(u, a)) \\<in> Pow(x Un y)"; |
|
99 by (Fast_tac 1); |
|
100 qed "cons_cons_subset"; |
|
101 |
|
102 Goal "[| a eqpoll k; a \\<subseteq> y; b \\<in> y-a; u \\<in> x; x Int y = 0 |] \ |
|
103 \ ==> cons(b, cons(u, a)) eqpoll succ(succ(k))"; |
|
104 by (fast_tac (claset() addSIs [cons_eqpoll_succ]) 1); |
|
105 qed "cons_cons_eqpoll"; |
|
106 |
|
107 Goal "[| succ(k) eqpoll A; k eqpoll B; B \\<subseteq> A; a \\<in> A-B; k \\<in> nat |] \ |
|
108 \ ==> A = cons(a, B)"; |
|
109 by (rtac equalityI 1); |
|
110 by (Fast_tac 2); |
|
111 by (resolve_tac [Diff_eq_0_iff RS iffD1] 1); |
|
112 by (rtac equals0I 1); |
|
113 by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1); |
|
114 by (dresolve_tac [eqpoll_sym RS cons_eqpoll_succ] 1); |
|
115 by (Fast_tac 1); |
|
116 by (dtac cons_eqpoll_succ 1); |
|
117 by (Fast_tac 1); |
|
118 by (fast_tac |
|
119 (claset() |
|
120 addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS |
|
121 (lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1); |
|
122 qed "set_eq_cons"; |
|
123 |
|
124 Goal "[| cons(x,a) = cons(y,a); x\\<notin> a |] ==> x = y "; |
|
125 by (fast_tac (claset() addSEs [equalityE]) 1); |
|
126 qed "cons_eqE"; |
|
127 |
|
128 Goal "A = B ==> A Int C = B Int C"; |
|
129 by (Asm_simp_tac 1); |
|
130 qed "eq_imp_Int_eq"; |
|
131 |
|
132 (* ********************************************************************** *) |
|
133 (* some arithmetic *) |
|
134 (* ********************************************************************** *) |
|
135 |
|
136 Goal "[| k \\<in> nat; m \\<in> nat |] ==> \ |
|
137 \ \\<forall>A B. A eqpoll k #+ m & k lepoll B & B \\<subseteq> A --> A-B lepoll m"; |
|
138 by (induct_tac "k" 1); |
|
139 by (asm_simp_tac (simpset() addsimps [add_0]) 1); |
|
140 by (fast_tac (claset() addIs [eqpoll_imp_lepoll RS |
|
141 (Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1); |
|
142 by (REPEAT (resolve_tac [allI,impI] 1)); |
|
143 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
|
144 by (Fast_tac 1); |
|
145 by (eres_inst_tac [("x","A - {xa}")] allE 1); |
|
146 by (eres_inst_tac [("x","B - {xa}")] allE 1); |
|
147 by (etac impE 1); |
|
148 by (asm_full_simp_tac (simpset() addsimps [add_succ]) 1); |
|
149 by (fast_tac (claset() addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1); |
|
150 by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2)); |
|
151 by (Fast_tac 1); |
|
152 qed "eqpoll_sum_imp_Diff_lepoll_lemma"; |
|
153 |
|
154 Goal "[| A eqpoll succ(k #+ m); B \\<subseteq> A; succ(k) lepoll B; k \\<in> nat; m \\<in> nat |] \ |
|
155 \ ==> A-B lepoll m"; |
|
156 by (dresolve_tac [add_succ RS ssubst] 1); |
|
157 by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_lepoll_lemma] 1 |
|
158 THEN (REPEAT (assume_tac 1))); |
|
159 by (Fast_tac 1); |
|
160 qed "eqpoll_sum_imp_Diff_lepoll"; |
|
161 |
|
162 (* ********************************************************************** *) |
|
163 (* similar properties for eqpoll *) |
|
164 (* ********************************************************************** *) |
|
165 |
|
166 Goal "[| k \\<in> nat; m \\<in> nat |] ==> \ |
|
167 \ \\<forall>A B. A eqpoll k #+ m & k eqpoll B & B \\<subseteq> A --> A-B eqpoll m"; |
|
168 by (induct_tac "k" 1); |
|
169 by (fast_tac (claset() addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] |
|
170 addss (simpset() addsimps [add_0])) 1); |
|
171 by (REPEAT (resolve_tac [allI,impI] 1)); |
|
172 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
|
173 by (fast_tac (claset() addSEs [eqpoll_imp_lepoll]) 1); |
|
174 by (eres_inst_tac [("x","A - {xa}")] allE 1); |
|
175 by (eres_inst_tac [("x","B - {xa}")] allE 1); |
|
176 by (etac impE 1); |
|
177 by (fast_tac (claset() addSIs [Diff_sing_eqpoll, |
|
178 eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym] |
|
179 addss (simpset() addsimps [add_succ])) 1); |
|
180 by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2)); |
|
181 by (Fast_tac 1); |
|
182 qed "eqpoll_sum_imp_Diff_eqpoll_lemma"; |
|
183 |
|
184 Goal "[| A eqpoll succ(k #+ m); B \\<subseteq> A; succ(k) eqpoll B; k \\<in> nat; m \\<in> nat |] \ |
|
185 \ ==> A-B eqpoll m"; |
|
186 by (dresolve_tac [add_succ RS ssubst] 1); |
|
187 by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_eqpoll_lemma] 1 |
|
188 THEN (REPEAT (assume_tac 1))); |
|
189 by (Fast_tac 1); |
|
190 qed "eqpoll_sum_imp_Diff_eqpoll"; |
|
191 |
|
192 |
|
193 (* ********************************************************************** *) |
|
194 (* LL can be well ordered *) |
|
195 (* ********************************************************************** *) |
|
196 |
|
197 Goal "{x \\<in> Pow(X). x lepoll 0} = {0}"; |
|
198 by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [lepoll_refl]) 1); |
|
199 qed "subsets_lepoll_0_eq_unit"; |
|
200 |
|
201 Goal "n \\<in> nat ==> {z \\<in> Pow(y). z lepoll succ(n)} = \ |
|
202 \ {z \\<in> Pow(y). z lepoll n} Un {z \\<in> Pow(y). z eqpoll succ(n)}"; |
|
203 by (fast_tac (claset() addIs [le_refl, leI, le_imp_lepoll] |
|
204 addSDs [lepoll_succ_disj] |
|
205 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
|
206 qed "subsets_lepoll_succ"; |
|
207 |
|
208 Goal "n \\<in> nat ==> {z \\<in> Pow(y). z lepoll n} Int {z \\<in> Pow(y). z eqpoll succ(n)} = 0"; |
|
209 by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_imp_lepoll |
|
210 RS lepoll_trans RS succ_lepoll_natE] |
|
211 addSIs [equals0I]) 1); |
|
212 qed "Int_empty"; |
|
213 |
|
214 |
|
215 Open_locale "AC16"; |
|
216 |
|
217 val all_ex = thm "all_ex"; |
|
218 val disjoint = thm "disjoint"; |
|
219 val includes = thm "includes"; |
|
220 val WO_R = thm "WO_R"; |
|
221 val k_def = thm "k_def"; |
|
222 val lnat = thm "lnat"; |
|
223 val mnat = thm "mnat"; |
|
224 val mpos = thm "mpos"; |
|
225 val Infinite = thm "Infinite"; |
|
226 val noLepoll = thm "noLepoll"; |
|
227 |
|
228 val LL_def = thm "LL_def"; |
|
229 val MM_def = thm "MM_def"; |
|
230 val GG_def = thm "GG_def"; |
|
231 val s_def = thm "s_def"; |
|
232 |
|
233 Addsimps [disjoint, WO_R, lnat, mnat, mpos, Infinite]; |
|
234 AddSIs [disjoint, WO_R, lnat, mnat, mpos]; |
|
235 |
|
236 Goalw [k_def] "k \\<in> nat"; |
|
237 by Auto_tac; |
|
238 qed "knat"; |
|
239 Addsimps [knat]; AddSIs [knat]; |
|
240 |
|
241 AddSIs [Infinite]; (*if notI is removed!*) |
|
242 AddSEs [Infinite RS notE]; |
|
243 |
|
244 AddEs [[disjoint, IntI] MRS (equals0D RS notE)]; |
|
245 |
|
246 (*use k = succ(l) *) |
|
247 val includes_l = simplify (FOL_ss addsimps [k_def]) includes; |
|
248 val all_ex_l = simplify (FOL_ss addsimps [k_def]) all_ex; |
|
249 |
|
250 (* ********************************************************************** *) |
|
251 (* 1. y is less than or equipollent to {v \\<in> s(u). a \\<subseteq> v} *) |
|
252 (* where a is certain k-2 element subset of y *) |
|
253 (* ********************************************************************** *) |
|
254 |
|
255 Goal "[| l eqpoll a; a \\<subseteq> y |] ==> y - a eqpoll y"; |
|
256 by (cut_facts_tac [WO_R, Infinite, lnat] 1); |
|
257 by (fast_tac (empty_cs addIs [lesspoll_trans1] |
|
258 addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans, |
|
259 Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord |
|
260 RS le_imp_lepoll] |
|
261 addSEs [well_ord_cardinal_eqpoll, |
|
262 well_ord_cardinal_eqpoll RS eqpoll_sym, |
|
263 eqpoll_sym RS eqpoll_imp_lepoll, |
|
264 n_lesspoll_nat RS lesspoll_trans2, |
|
265 well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
|
266 RS lepoll_infinite]) 1); |
|
267 qed "Diff_Finite_eqpoll"; |
|
268 |
|
269 Goalw [s_def] "s(u) \\<subseteq> t_n"; |
|
270 by (Fast_tac 1); |
|
271 qed "s_subset"; |
|
272 |
|
273 Goalw [s_def, succ_def, k_def] |
|
274 "[| w \\<in> t_n; cons(b,cons(u,a)) \\<subseteq> w; a \\<subseteq> y; b \\<in> y-a; l eqpoll a \ |
|
275 \ |] ==> w \\<in> s(u)"; |
|
276 by (fast_tac (claset() addDs [eqpoll_imp_lepoll RS cons_lepoll_cong] |
|
277 addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); |
|
278 qed "sI"; |
|
279 |
|
280 Goalw [s_def] "v \\<in> s(u) ==> u \\<in> v"; |
|
281 by (Fast_tac 1); |
|
282 qed "in_s_imp_u_in"; |
|
283 |
|
284 |
|
285 Goal "[| l eqpoll a; a \\<subseteq> y; b \\<in> y - a; u \\<in> x |] \ |
|
286 \ ==> \\<exists>! c. c \\<in> s(u) & a \\<subseteq> c & b \\<in> c"; |
|
287 by (rtac (all_ex_l RS ballE) 1); |
|
288 by (blast_tac (claset() delrules [PowI] |
|
289 addSIs [cons_cons_subset, |
|
290 eqpoll_sym RS cons_cons_eqpoll]) 2); |
|
291 by (etac ex1E 1); |
|
292 by (res_inst_tac [("a","w")] ex1I 1); |
|
293 by (blast_tac (claset() addIs [sI]) 1); |
|
294 by (etac allE 1); |
|
295 by (etac impE 1); |
|
296 by (assume_tac 2); |
|
297 by (fast_tac (claset() addSEs [s_subset RS subsetD, in_s_imp_u_in]) 1); |
|
298 qed "ex1_superset_a"; |
|
299 |
|
300 Goal "[| \\<forall>v \\<in> s(u). succ(l) eqpoll v Int y; \ |
|
301 \ l eqpoll a; a \\<subseteq> y; b \\<in> y - a; u \\<in> x |] \ |
|
302 \ ==> (THE c. c \\<in> s(u) & a \\<subseteq> c & b \\<in> c) \ |
|
303 \ Int y = cons(b, a)"; |
|
304 by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1)); |
|
305 by (rtac set_eq_cons 1); |
|
306 by (REPEAT (Fast_tac 1)); |
|
307 qed "the_eq_cons"; |
|
308 |
|
309 Goal "[| \\<forall>v \\<in> s(u). succ(l) eqpoll v Int y; \ |
|
310 \ l eqpoll a; a \\<subseteq> y; u \\<in> x |] \ |
|
311 \ ==> y lepoll {v \\<in> s(u). a \\<subseteq> v}"; |
|
312 by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS |
|
313 eqpoll_imp_lepoll RS lepoll_trans] 1 |
|
314 THEN REPEAT (Fast_tac 1)); |
|
315 by (res_inst_tac |
|
316 [("f3", "\\<lambda>b \\<in> y-a. THE c. c \\<in> s(u) & a \\<subseteq> c & b \\<in> c")] |
|
317 (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
|
318 by (simp_tac (simpset() addsimps [inj_def]) 1); |
|
319 by (rtac conjI 1); |
|
320 by (rtac lam_type 1); |
|
321 by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (Fast_tac 1)); |
|
322 by (Asm_simp_tac 1); |
|
323 by (Clarify_tac 1); |
|
324 by (rtac cons_eqE 1); |
|
325 by (Fast_tac 2); |
|
326 by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1); |
|
327 by (asm_full_simp_tac (simpset() addsimps [the_eq_cons]) 1); |
|
328 qed "y_lepoll_subset_s"; |
|
329 |
|
330 |
|
331 (* ********************************************************************** *) |
|
332 (* back to the second part *) |
|
333 (* ********************************************************************** *) |
|
334 |
|
335 Goal "w \\<subseteq> x Un y ==> w Int (x - {u}) = w - cons(u, w Int y)"; |
|
336 by (Fast_tac 1); |
|
337 qed "w_Int_eq_w_Diff"; |
|
338 |
|
339 Goal "[| w \\<in> {v \\<in> s(u). a \\<subseteq> v}; \ |
|
340 \ l eqpoll a; u \\<in> x; \ |
|
341 \ \\<forall>v \\<in> s(u). succ(l) eqpoll v Int y \ |
|
342 \ |] ==> w Int (x - {u}) eqpoll m"; |
|
343 by (etac CollectE 1); |
|
344 by (stac w_Int_eq_w_Diff 1); |
|
345 by (fast_tac (claset() addSDs [s_subset RS subsetD, |
|
346 includes_l RS subsetD]) 1); |
|
347 by (fast_tac (claset() addSDs [bspec] |
|
348 addDs [s_subset RS subsetD, includes_l RS subsetD] |
|
349 addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_imp_u_in] |
|
350 addSIs [eqpoll_sum_imp_Diff_eqpoll]) 1); |
|
351 qed "w_Int_eqpoll_m"; |
|
352 |
|
353 (* ********************************************************************** *) |
|
354 (* 2. {v \\<in> s(u). a \\<subseteq> v} is less than or equipollent *) |
|
355 (* to {v \\<in> Pow(x). v eqpoll n-k} *) |
|
356 (* ********************************************************************** *) |
|
357 |
|
358 Goal "x eqpoll m ==> x \\<noteq> 0"; |
|
359 by (cut_facts_tac [mpos] 1); |
|
360 by (fast_tac (claset() addSEs [zero_lt_natE] |
|
361 addSDs [eqpoll_succ_imp_not_empty]) 1); |
|
362 qed "eqpoll_m_not_empty"; |
|
363 |
|
364 Goal "[| z \\<in> xa Int (x - {u}); l eqpoll a; a \\<subseteq> y; u \\<in> x |] \ |
|
365 \ ==> \\<exists>! w. w \\<in> t_n & cons(z, cons(u, a)) \\<subseteq> w"; |
|
366 by (rtac (all_ex RS bspec) 1); |
|
367 by (rewtac k_def); |
|
368 by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [eqpoll_sym]) 1); |
|
369 qed "cons_cons_in"; |
|
370 |
|
371 Goal "[| \\<forall>v \\<in> s(u). succ(l) eqpoll v Int y; \ |
|
372 \ a \\<subseteq> y; l eqpoll a; u \\<in> x |] \ |
|
373 \ ==> {v \\<in> s(u). a \\<subseteq> v} lepoll {v \\<in> Pow(x). v eqpoll m}"; |
|
374 by (res_inst_tac [("f3","\\<lambda>w \\<in> {v \\<in> s(u). a \\<subseteq> v}. w Int (x - {u})")] |
|
375 (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
|
376 by (simp_tac (simpset() addsimps [inj_def]) 1); |
|
377 by (rtac conjI 1); |
|
378 by (rtac lam_type 1); |
|
379 by (rtac CollectI 1); |
|
380 by (Fast_tac 1); |
|
381 by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1)); |
|
382 by (REPEAT (resolve_tac [ballI, impI] 1)); |
|
383 (** LEVEL 8 **) |
|
384 by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1); |
|
385 by (EVERY (map Blast_tac [4,3,2,1])); |
|
386 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); |
|
387 by (ftac cons_cons_in 1 THEN REPEAT (assume_tac 1)); |
|
388 by (etac ex1_two_eq 1); |
|
389 by (REPEAT (blast_tac |
|
390 (claset() addDs [s_subset RS subsetD, in_s_imp_u_in]) 1)); |
|
391 qed "subset_s_lepoll_w"; |
|
392 |
|
393 |
|
394 (* ********************************************************************** *) |
|
395 (* well_ord_subsets_lepoll_n *) |
|
396 (* ********************************************************************** *) |
|
397 |
|
398 Goal "n \\<in> nat ==> \\<exists>S. well_ord({z \\<in> Pow(y) . z eqpoll succ(n)}, S)"; |
|
399 by (resolve_tac [WO_R RS well_ord_infinite_subsets_eqpoll_X |
|
400 RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
|
401 by (REPEAT (fast_tac (claset() addIs [bij_is_inj RS well_ord_rvimage]) 1)); |
|
402 qed "well_ord_subsets_eqpoll_n"; |
|
403 |
|
404 Goal "n \\<in> nat ==> \\<exists>R. well_ord({z \\<in> Pow(y). z lepoll n}, R)"; |
|
405 by (induct_tac "n" 1); |
|
406 by (force_tac (claset() addSIs [well_ord_unit], |
|
407 simpset() addsimps [subsets_lepoll_0_eq_unit]) 1); |
|
408 by (etac exE 1); |
|
409 by (resolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 THEN assume_tac 1); |
|
410 by (asm_simp_tac (simpset() addsimps [subsets_lepoll_succ]) 1); |
|
411 by (dtac well_ord_radd 1 THEN (assume_tac 1)); |
|
412 by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS |
|
413 (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
|
414 by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
|
415 qed "well_ord_subsets_lepoll_n"; |
|
416 |
|
417 |
|
418 Goalw [LL_def, MM_def] "LL \\<subseteq> {z \\<in> Pow(y). z lepoll succ(k #+ m)}"; |
|
419 by (cut_facts_tac [includes] 1); |
|
420 by (fast_tac (claset() addIs [subset_imp_lepoll |
|
421 RS (eqpoll_imp_lepoll |
|
422 RSN (2, lepoll_trans))]) 1); |
|
423 qed "LL_subset"; |
|
424 |
|
425 Goal "\\<exists>S. well_ord(LL,S)"; |
|
426 by (rtac (well_ord_subsets_lepoll_n RS exE) 1); |
|
427 by (blast_tac (claset() addIs [LL_subset RSN (2, well_ord_subset)]) 2); |
|
428 by Auto_tac; |
|
429 qed "well_ord_LL"; |
|
430 |
|
431 (* ********************************************************************** *) |
|
432 (* every element of LL is a contained in exactly one element of MM *) |
|
433 (* ********************************************************************** *) |
|
434 |
|
435 Goalw [MM_def, LL_def] "v \\<in> LL ==> \\<exists>! w. w \\<in> MM & v \\<subseteq> w"; |
|
436 by Safe_tac; |
|
437 by (Fast_tac 1); |
|
438 by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1)); |
|
439 by (res_inst_tac [("x","x")] (all_ex RS ballE) 1); |
|
440 by (fast_tac (claset() addSEs [eqpoll_sym]) 2); |
|
441 by (Blast_tac 1); |
|
442 qed "unique_superset_in_MM"; |
|
443 |
|
444 val unique_superset1 = unique_superset_in_MM RS theI RS conjunct1; |
|
445 val unique_superset2 = unique_superset_in_MM RS the_equality2; |
|
446 |
|
447 |
|
448 (* ********************************************************************** *) |
|
449 (* The function GG satisfies the conditions of WO4 *) |
|
450 (* ********************************************************************** *) |
|
451 |
|
452 (* ********************************************************************** *) |
|
453 (* The union of appropriate values is the whole x *) |
|
454 (* ********************************************************************** *) |
|
455 |
|
456 Goalw [LL_def] "w \\<in> MM ==> w Int y \\<in> LL"; |
|
457 by (Fast_tac 1); |
|
458 qed "Int_in_LL"; |
|
459 |
|
460 Goalw [LL_def] |
|
461 "v \\<in> LL ==> v = (THE x. x \\<in> MM & v \\<subseteq> x) Int y"; |
|
462 by (Clarify_tac 1); |
|
463 by (stac unique_superset2 1); |
|
464 by (auto_tac (claset(), simpset() addsimps [Int_in_LL])); |
|
465 qed "in_LL_eq_Int"; |
|
466 |
|
467 Goal "v \\<in> LL ==> (THE x. x \\<in> MM & v \\<subseteq> x) \\<subseteq> x Un y"; |
|
468 by (dtac unique_superset1 1); |
|
469 by (rewtac MM_def); |
|
470 by (fast_tac (claset() addSDs [unique_superset1, includes RS subsetD]) 1); |
|
471 qed "the_in_MM_subset"; |
|
472 |
|
473 Goalw [GG_def] "v \\<in> LL ==> GG ` v \\<subseteq> x"; |
|
474 by (ftac the_in_MM_subset 1); |
|
475 by (ftac in_LL_eq_Int 1); |
|
476 by (force_tac (claset() addEs [equalityE], simpset()) 1); |
|
477 qed "GG_subset"; |
|
478 |
|
479 |
|
480 Goal "n \\<in> nat ==> \\<exists>z. z \\<subseteq> y & n eqpoll z"; |
|
481 by (etac nat_lepoll_imp_ex_eqpoll_n 1); |
|
482 by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
|
483 RSN (2, lepoll_trans)] 1); |
|
484 by (rtac WO_R 2); |
|
485 by (fast_tac |
|
486 (claset() delrules [notI] |
|
487 addSIs [nat_le_infinite_Ord RS le_imp_lepoll] |
|
488 addIs [Ord_ordertype, |
|
489 ordertype_eqpoll RS eqpoll_imp_lepoll |
|
490 RS lepoll_infinite]) 1); |
|
491 qed "ex_subset_eqpoll_n"; |
|
492 |
|
493 |
|
494 Goal "u \\<in> x ==> \\<exists>v \\<in> s(u). succ(k) lepoll v Int y"; |
|
495 by (rtac ccontr 1); |
|
496 by (subgoal_tac "\\<forall>v \\<in> s(u). k eqpoll v Int y" 1); |
|
497 by (full_simp_tac (simpset() addsimps [s_def]) 2); |
|
498 by (blast_tac (claset() addIs [succ_not_lepoll_imp_eqpoll]) 2); |
|
499 by (rewtac k_def); |
|
500 by (cut_facts_tac [all_ex, includes, lnat] 1); |
|
501 by (rtac (ex_subset_eqpoll_n RS exE) 1 THEN assume_tac 1); |
|
502 by (rtac (noLepoll RS notE) 1); |
|
503 by (blast_tac (claset() addIs |
|
504 [[y_lepoll_subset_s, subset_s_lepoll_w] MRS lepoll_trans]) 1); |
|
505 qed "exists_proper_in_s"; |
|
506 |
|
507 Goal "u \\<in> x ==> \\<exists>w \\<in> MM. u \\<in> w"; |
|
508 by (eresolve_tac [exists_proper_in_s RS bexE] 1); |
|
509 by (rewrite_goals_tac [MM_def, s_def]); |
|
510 by (Fast_tac 1); |
|
511 qed "exists_in_MM"; |
|
512 |
|
513 Goal "u \\<in> x ==> \\<exists>w \\<in> LL. u \\<in> GG`w"; |
|
514 by (rtac (exists_in_MM RS bexE) 1); |
|
515 by (assume_tac 1); |
|
516 by (rtac bexI 1); |
|
517 by (etac Int_in_LL 2); |
|
518 by (rewtac GG_def); |
|
519 by (asm_simp_tac (simpset() addsimps [Int_in_LL]) 1); |
|
520 by (stac unique_superset2 1); |
|
521 by (REPEAT (fast_tac (claset() addSEs [Int_in_LL]) 1)); |
|
522 qed "exists_in_LL"; |
|
523 |
|
524 |
|
525 Goal "well_ord(LL,S) ==> \ |
|
526 \ (\\<Union>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x"; |
|
527 by (rtac equalityI 1); |
|
528 by (rtac subsetI 1); |
|
529 by (etac OUN_E 1); |
|
530 by (resolve_tac [GG_subset RS subsetD] 1); |
|
531 by (assume_tac 2); |
|
532 by (blast_tac (claset() addIs [ordermap_bij RS bij_converse_bij RS |
|
533 bij_is_fun RS apply_type, ltD]) 1); |
|
534 by (rtac subsetI 1); |
|
535 by (eresolve_tac [exists_in_LL RS bexE] 1); |
|
536 by (force_tac (claset() addIs [Ord_ordertype RSN (2, ltI), |
|
537 ordermap_type RS apply_type], |
|
538 simpset() addsimps [ordermap_bij RS bij_is_inj RS left_inverse]) 1); |
|
539 qed "OUN_eq_x"; |
|
540 |
|
541 (* ********************************************************************** *) |
|
542 (* Every element of the family is less than or equipollent to n-k (m) *) |
|
543 (* ********************************************************************** *) |
|
544 |
|
545 Goalw [MM_def] "w \\<in> MM ==> w eqpoll succ(k #+ m)"; |
|
546 by (fast_tac (claset() addDs [includes RS subsetD]) 1); |
|
547 qed "in_MM_eqpoll_n"; |
|
548 |
|
549 Goalw [LL_def, MM_def] "w \\<in> LL ==> succ(k) lepoll w"; |
|
550 by (Fast_tac 1); |
|
551 qed "in_LL_eqpoll_n"; |
|
552 |
|
553 val in_LL = in_LL_eq_Int RS equalityD1 RS (Int_lower1 RSN (2, subset_trans)); |
|
554 |
|
555 Goalw [GG_def] |
|
556 "well_ord(LL,S) ==> \ |
|
557 \ \\<forall>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) lepoll m"; |
|
558 by (rtac oallI 1); |
|
559 by (asm_simp_tac |
|
560 (simpset() addsimps [ltD, |
|
561 ordermap_bij RS bij_converse_bij RS |
|
562 bij_is_fun RS apply_type]) 1); |
|
563 by (cut_facts_tac [includes] 1); |
|
564 by (rtac eqpoll_sum_imp_Diff_lepoll 1); |
|
565 by (REPEAT |
|
566 (fast_tac (claset() delrules [subsetI] |
|
567 addSDs [ltD] |
|
568 addSIs [eqpoll_sum_imp_Diff_lepoll, in_LL_eqpoll_n] |
|
569 addIs [unique_superset1 RS in_MM_eqpoll_n, in_LL, |
|
570 ordermap_bij RS bij_converse_bij RS |
|
571 bij_is_fun RS apply_type]) 1 )); |
|
572 qed "all_in_lepoll_m"; |
|
573 |
|
574 |
|
575 Goal "\\<exists>a f. Ord(a) & domain(f) = a & \ |
|
576 \ (\\<Union>b<a. f ` b) = x & (\\<forall>b<a. f ` b lepoll m)"; |
|
577 by (resolve_tac [well_ord_LL RS exE] 1 THEN REPEAT (assume_tac 1)); |
|
578 by (rename_tac "S" 1); |
|
579 by (res_inst_tac [("x","ordertype(LL,S)")] exI 1); |
|
580 by (res_inst_tac [("x", |
|
581 "\\<lambda>b \\<in> ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)")] |
|
582 exI 1); |
|
583 by (Simp_tac 1); |
|
584 by (REPEAT (ares_tac [conjI, lam_funtype RS domain_of_fun, |
|
585 Ord_ordertype, |
|
586 all_in_lepoll_m, OUN_eq_x] 1)); |
|
587 qed "conclusion"; |
|
588 |
|
589 Close_locale "AC16"; |
|
590 |
|
591 |
|
592 |
|
593 (* ********************************************************************** *) |
|
594 (* The main theorem AC16(n, k) ==> WO4(n-k) *) |
|
595 (* ********************************************************************** *) |
|
596 |
|
597 Goalw [AC16_def,WO4_def] |
|
598 "[| AC16(k #+ m, k); 0 < k; 0 < m; k \\<in> nat; m \\<in> nat |] ==> WO4(m)"; |
|
599 by (rtac allI 1); |
|
600 by (case_tac "Finite(A)" 1); |
|
601 by (rtac lemma1 1 THEN REPEAT (assume_tac 1)); |
|
602 by (cut_facts_tac [lemma2] 1); |
|
603 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
|
604 by (eres_inst_tac [("x","A Un y")] allE 1); |
|
605 by (ftac infinite_Un 1 THEN (mp_tac 1)); |
|
606 by (etac zero_lt_natE 1); |
|
607 by (assume_tac 1); |
|
608 by (Clarify_tac 1); |
|
609 by (DEPTH_SOLVE (ares_tac [export conclusion] 1)); |
|
610 qed "AC16_WO4"; |
|
611 |
|