1 (* Title: ZF/AC/WO6_WO1.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Grabczewski |
|
4 |
|
5 Proofs needed to state that formulations WO1,...,WO6 are all equivalent. |
|
6 The only hard one is WO6 ==> WO1. |
|
7 |
|
8 Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear" |
|
9 by Rubin & Rubin (page 2). |
|
10 They refer reader to a book by Gödel to see the proof WO1 ==> WO2. |
|
11 Fortunately order types made this proof also very easy. |
|
12 *) |
|
13 |
|
14 (* ********************************************************************** *) |
|
15 |
|
16 Goalw WO_defs "WO2 ==> WO3"; |
|
17 by (Fast_tac 1); |
|
18 qed "WO2_WO3"; |
|
19 |
|
20 (* ********************************************************************** *) |
|
21 |
|
22 Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1"; |
|
23 by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, |
|
24 well_ord_Memrel RS well_ord_subset]) 1); |
|
25 qed "WO3_WO1"; |
|
26 |
|
27 (* ********************************************************************** *) |
|
28 |
|
29 Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2"; |
|
30 by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); |
|
31 qed "WO1_WO2"; |
|
32 |
|
33 (* ********************************************************************** *) |
|
34 |
|
35 Goal "f \\<in> A->B ==> (\\<lambda>x \\<in> A. {f`x}): A -> {{b}. b \\<in> B}"; |
|
36 by (fast_tac (claset() addSIs [lam_type, apply_type]) 1); |
|
37 qed "lam_sets"; |
|
38 |
|
39 Goalw [surj_def] "f \\<in> surj(A,B) ==> (\\<Union>a \\<in> A. {f`a}) = B"; |
|
40 by (fast_tac (claset() addSEs [apply_type]) 1); |
|
41 qed "surj_imp_eq_"; |
|
42 |
|
43 Goal "[| f \\<in> surj(A,B); Ord(A) |] ==> (\\<Union>a<A. {f`a}) = B"; |
|
44 by (fast_tac (claset() addSDs [surj_imp_eq_] |
|
45 addSIs [ltI] addSEs [ltE]) 1); |
|
46 qed "surj_imp_eq"; |
|
47 |
|
48 Goalw WO_defs "WO1 ==> WO4(1)"; |
|
49 by (rtac allI 1); |
|
50 by (eres_inst_tac [("x","A")] allE 1); |
|
51 by (etac exE 1); |
|
52 by (REPEAT (resolve_tac [exI, conjI] 1)); |
|
53 by (etac Ord_ordertype 1); |
|
54 by (rtac conjI 1); |
|
55 by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS |
|
56 lam_sets RS domain_of_fun] 1); |
|
57 by (asm_simp_tac (simpset() addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll, |
|
58 Ord_ordertype RSN (2, ordermap_bij RS bij_converse_bij RS |
|
59 bij_is_surj RS surj_imp_eq)]) 1); |
|
60 qed "WO1_WO4"; |
|
61 |
|
62 (* ********************************************************************** *) |
|
63 |
|
64 Goalw WO_defs "[| m le n; WO4(m) |] ==> WO4(n)"; |
|
65 by (blast_tac (claset() addSDs [spec] |
|
66 addIs [le_imp_lepoll RSN (2, lepoll_trans)]) 1); |
|
67 qed "WO4_mono"; |
|
68 |
|
69 (* ********************************************************************** *) |
|
70 |
|
71 Goalw WO_defs "[| m \\<in> nat; 1 le m; WO4(m) |] ==> WO5"; |
|
72 by (Blast_tac 1); |
|
73 qed "WO4_WO5"; |
|
74 |
|
75 (* ********************************************************************** *) |
|
76 |
|
77 Goalw WO_defs "WO5 ==> WO6"; |
|
78 by (Blast_tac 1); |
|
79 qed "WO5_WO6"; |
|
80 |
|
81 |
|
82 (* ********************************************************************** |
|
83 The proof of "WO6 ==> WO1". Simplified by L C Paulson. |
|
84 |
|
85 From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin, |
|
86 pages 2-5 |
|
87 ************************************************************************* *) |
|
88 |
|
89 goal OrderType.thy |
|
90 "!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==> \ |
|
91 \ k < i | (~ k<i & k = i ++ (k--i) & (k--i)<j)"; |
|
92 by (res_inst_tac [("i","k"),("j","i")] Ord_linear2 1); |
|
93 by (dtac odiff_lt_mono2 4 THEN assume_tac 4); |
|
94 by (asm_full_simp_tac |
|
95 (simpset() addsimps [oadd_odiff_inverse, odiff_oadd_inverse]) 4); |
|
96 by (safe_tac (claset() addSEs [lt_Ord])); |
|
97 qed "lt_oadd_odiff_disj"; |
|
98 |
|
99 (*The corresponding elimination rule*) |
|
100 val lt_oadd_odiff_cases = rule_by_tactic Safe_tac |
|
101 (lt_oadd_odiff_disj RS disjE); |
|
102 |
|
103 (* ********************************************************************** *) |
|
104 (* The most complicated part of the proof - lemma ii - p. 2-4 *) |
|
105 (* ********************************************************************** *) |
|
106 |
|
107 (* ********************************************************************** *) |
|
108 (* some properties of relation uu(beta, gamma, delta) - p. 2 *) |
|
109 (* ********************************************************************** *) |
|
110 |
|
111 Goalw [uu_def] "domain(uu(f,b,g,d)) \\<subseteq> f`b"; |
|
112 by (Blast_tac 1); |
|
113 qed "domain_uu_subset"; |
|
114 |
|
115 Goal "\\<forall>b<a. f`b lepoll m ==> \ |
|
116 \ \\<forall>b<a. \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) lepoll m"; |
|
117 by (fast_tac (claset() addSEs |
|
118 [domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1); |
|
119 qed "quant_domain_uu_lepoll_m"; |
|
120 |
|
121 Goalw [uu_def] "uu(f,b,g,d) \\<subseteq> f`b * f`g"; |
|
122 by (Blast_tac 1); |
|
123 qed "uu_subset1"; |
|
124 |
|
125 Goalw [uu_def] "uu(f,b,g,d) \\<subseteq> f`d"; |
|
126 by (Blast_tac 1); |
|
127 qed "uu_subset2"; |
|
128 |
|
129 Goal "[| \\<forall>b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m"; |
|
130 by (fast_tac (claset() |
|
131 addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1); |
|
132 qed "uu_lepoll_m"; |
|
133 |
|
134 (* ********************************************************************** *) |
|
135 (* Two cases for lemma ii *) |
|
136 (* ********************************************************************** *) |
|
137 Goalw [lesspoll_def] |
|
138 "\\<forall>b<a. \\<forall>g<a. \\<forall>d<a. u(f,b,g,d) lepoll m \ |
|
139 \ ==> (\\<forall>b<a. f`b \\<noteq> 0 --> \ |
|
140 \ (\\<exists>g<a. \\<exists>d<a. u(f,b,g,d) \\<noteq> 0 & u(f,b,g,d) lesspoll m)) \ |
|
141 \ | (\\<exists>b<a. f`b \\<noteq> 0 & (\\<forall>g<a. \\<forall>d<a. u(f,b,g,d) \\<noteq> 0 --> \ |
|
142 \ u(f,b,g,d) eqpoll m))"; |
|
143 by (Asm_simp_tac 1); |
|
144 by (blast_tac (claset() delrules [equalityI]) 1); |
|
145 qed "cases"; |
|
146 |
|
147 (* ********************************************************************** *) |
|
148 (* Lemmas used in both cases *) |
|
149 (* ********************************************************************** *) |
|
150 Goal "Ord(a) ==> (\\<Union>b<a++a. C(b)) = (\\<Union>b<a. C(b) Un C(a++b))"; |
|
151 by (fast_tac (claset() addSIs [equalityI] addIs [ltI] |
|
152 addSDs [lt_oadd_disj] |
|
153 addSEs [lt_oadd1, oadd_lt_mono2]) 1); |
|
154 qed "UN_oadd"; |
|
155 |
|
156 |
|
157 (* ********************************************************************** *) |
|
158 (* Case 1 \\<in> lemmas *) |
|
159 (* ********************************************************************** *) |
|
160 |
|
161 Goalw [vv1_def] "vv1(f,m,b) \\<subseteq> f`b"; |
|
162 by (rtac (LetI RS LetI) 1); |
|
163 by (simp_tac (simpset() addsimps [domain_uu_subset]) 1); |
|
164 qed "vv1_subset"; |
|
165 |
|
166 (* ********************************************************************** *) |
|
167 (* Case 1 \\<in> Union of images is the whole "y" *) |
|
168 (* ********************************************************************** *) |
|
169 Goalw [gg1_def] |
|
170 "!! a f y. [| Ord(a); m \\<in> nat |] ==> \ |
|
171 \ (\\<Union>b<a++a. gg1(f,a,m)`b) = (\\<Union>b<a. f`b)"; |
|
172 by (asm_simp_tac |
|
173 (simpset() addsimps [UN_oadd, lt_oadd1, |
|
174 oadd_le_self RS le_imp_not_lt, lt_Ord, |
|
175 odiff_oadd_inverse, ltD, |
|
176 vv1_subset RS Diff_partition, ww1_def]) 1); |
|
177 qed "UN_gg1_eq"; |
|
178 |
|
179 Goal "domain(gg1(f,a,m)) = a++a"; |
|
180 by (simp_tac (simpset() addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1); |
|
181 qed "domain_gg1"; |
|
182 |
|
183 (* ********************************************************************** *) |
|
184 (* every value of defined function is less than or equipollent to m *) |
|
185 (* ********************************************************************** *) |
|
186 Goal "[| P(a, b); Ord(a); Ord(b); \ |
|
187 \ Least_a = (LEAST a. \\<exists>x. Ord(x) & P(a, x)) |] \ |
|
188 \ ==> P(Least_a, LEAST b. P(Least_a, b))"; |
|
189 by (etac ssubst 1); |
|
190 by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1); |
|
191 by (REPEAT (fast_tac (claset() addSEs [LeastI]) 1)); |
|
192 qed "nested_LeastI"; |
|
193 |
|
194 bind_thm ("nested_Least_instance", |
|
195 inst "P" |
|
196 "%g d. domain(uu(f,b,g,d)) \\<noteq> 0 & domain(uu(f,b,g,d)) lepoll m" |
|
197 nested_LeastI); |
|
198 |
|
199 Goalw [gg1_def] |
|
200 "!!a. [| Ord(a); m \\<in> nat; \ |
|
201 \ \\<forall>b<a. f`b \\<noteq>0 --> \ |
|
202 \ (\\<exists>g<a. \\<exists>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 & \ |
|
203 \ domain(uu(f,b,g,d)) lepoll m); \ |
|
204 \ \\<forall>b<a. f`b lepoll succ(m); b<a++a \ |
|
205 \ |] ==> gg1(f,a,m)`b lepoll m"; |
|
206 by (Asm_simp_tac 1); |
|
207 by (safe_tac (claset() addSEs [lt_oadd_odiff_cases])); |
|
208 (*Case b<a \\<in> show vv1(f,m,b) lepoll m *) |
|
209 by (asm_simp_tac (simpset() addsimps [vv1_def, Let_def]) 1); |
|
210 by (fast_tac (claset() addIs [nested_Least_instance RS conjunct2] |
|
211 addSEs [lt_Ord] |
|
212 addSIs [empty_lepollI]) 1); |
|
213 (*Case a le b \\<in> show ww1(f,m,b--a) lepoll m *) |
|
214 by (asm_simp_tac (simpset() addsimps [ww1_def]) 1); |
|
215 by (excluded_middle_tac "f`(b--a) = 0" 1); |
|
216 by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2); |
|
217 by (rtac Diff_lepoll 1); |
|
218 by (Blast_tac 1); |
|
219 by (rtac vv1_subset 1); |
|
220 by (dtac (ospec RS mp) 1); |
|
221 by (REPEAT (eresolve_tac [asm_rl, oexE, conjE] 1)); |
|
222 by (asm_simp_tac (simpset() |
|
223 addsimps [vv1_def, Let_def, lt_Ord, |
|
224 nested_Least_instance RS conjunct1]) 1); |
|
225 qed "gg1_lepoll_m"; |
|
226 |
|
227 (* ********************************************************************** *) |
|
228 (* Case 2 \\<in> lemmas *) |
|
229 (* ********************************************************************** *) |
|
230 |
|
231 (* ********************************************************************** *) |
|
232 (* Case 2 \\<in> vv2_subset *) |
|
233 (* ********************************************************************** *) |
|
234 |
|
235 Goalw [uu_def] "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \ |
|
236 \ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y \ |
|
237 \ |] ==> \\<exists>d<a. uu(f,b,g,d) \\<noteq> 0"; |
|
238 by (fast_tac (claset() addSIs [not_emptyI] |
|
239 addSDs [SigmaI RSN (2, subsetD)] |
|
240 addSEs [not_emptyE]) 1); |
|
241 qed "ex_d_uu_not_empty"; |
|
242 |
|
243 Goal "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \ |
|
244 \ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y |] \ |
|
245 \ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) \\<noteq> 0)) \\<noteq> 0"; |
|
246 by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1)); |
|
247 by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1); |
|
248 qed "uu_not_empty"; |
|
249 |
|
250 Goal "[| r \\<subseteq> A*B; r\\<noteq>0 |] ==> domain(r)\\<noteq>0"; |
|
251 by (Blast_tac 1); |
|
252 qed "not_empty_rel_imp_domain"; |
|
253 |
|
254 Goal "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \ |
|
255 \ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y |] \ |
|
256 \ ==> (LEAST d. uu(f,b,g,d) \\<noteq> 0) < a"; |
|
257 by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1 |
|
258 THEN REPEAT (assume_tac 1)); |
|
259 by (resolve_tac [Least_le RS lt_trans1] 1 |
|
260 THEN (REPEAT (ares_tac [lt_Ord] 1))); |
|
261 qed "Least_uu_not_empty_lt_a"; |
|
262 |
|
263 Goal "[| B \\<subseteq> A; a\\<notin>B |] ==> B \\<subseteq> A-{a}"; |
|
264 by (Blast_tac 1); |
|
265 qed "subset_Diff_sing"; |
|
266 |
|
267 (*Could this be proved more directly?*) |
|
268 Goal "[| A lepoll m; m lepoll B; B \\<subseteq> A; m \\<in> nat |] ==> A=B"; |
|
269 by (etac natE 1); |
|
270 by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [equalityI]) 1); |
|
271 by (safe_tac (claset() addSIs [equalityI])); |
|
272 by (rtac ccontr 1); |
|
273 by (etac (subset_Diff_sing RS subset_imp_lepoll |
|
274 RSN (2, Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS |
|
275 succ_lepoll_natE) 1 |
|
276 THEN REPEAT (assume_tac 1)); |
|
277 qed "supset_lepoll_imp_eq"; |
|
278 |
|
279 Goal "[| \\<forall>g<a. \\<forall>d<a. domain(uu(f, b, g, d))\\<noteq>0 --> \ |
|
280 \ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
|
281 \ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \ |
|
282 \ (\\<Union>b<a. f`b)=y; b<a; g<a; d<a; \ |
|
283 \ f`b\\<noteq>0; f`g\\<noteq>0; m \\<in> nat; s \\<in> f`b \ |
|
284 \ |] ==> uu(f, b, g, LEAST d. uu(f,b,g,d)\\<noteq>0) \\<in> f`b -> f`g"; |
|
285 by (dres_inst_tac [("x2","g")] (ospec RS ospec RS mp) 1); |
|
286 by (rtac ([uu_subset1, uu_not_empty] MRS not_empty_rel_imp_domain) 3); |
|
287 by (rtac Least_uu_not_empty_lt_a 2 THEN TRYALL assume_tac); |
|
288 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS |
|
289 (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2, |
|
290 uu_subset1 RSN (4, rel_is_fun)))] 1 |
|
291 THEN TRYALL assume_tac); |
|
292 by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1); |
|
293 by (REPEAT_FIRST assume_tac); |
|
294 by (REPEAT (fast_tac (claset() addSIs [domain_uu_subset]) 1)); |
|
295 qed "uu_Least_is_fun"; |
|
296 |
|
297 Goalw [vv2_def] |
|
298 "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f, b, g, d))\\<noteq>0 --> \ |
|
299 \ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
|
300 \ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \ |
|
301 \ (\\<Union>b<a. f`b)=y; b<a; g<a; m \\<in> nat; s \\<in> f`b \ |
|
302 \ |] ==> vv2(f,b,g,s) \\<subseteq> f`g"; |
|
303 by (split_tac [split_if] 1); |
|
304 by Safe_tac; |
|
305 by (etac (uu_Least_is_fun RS apply_type) 1); |
|
306 by (REPEAT_SOME (fast_tac (claset() addSIs [not_emptyI, singleton_subsetI]))); |
|
307 qed "vv2_subset"; |
|
308 |
|
309 (* ********************************************************************** *) |
|
310 (* Case 2 \\<in> Union of images is the whole "y" *) |
|
311 (* ********************************************************************** *) |
|
312 Goalw [gg2_def] |
|
313 "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 --> \ |
|
314 \ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
|
315 \ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \ |
|
316 \ (\\<Union>b<a. f`b)=y; Ord(a); m \\<in> nat; s \\<in> f`b; b<a \ |
|
317 \ |] ==> (\\<Union>g<a++a. gg2(f,a,b,s) ` g) = y"; |
|
318 by (dtac sym 1); |
|
319 by (asm_simp_tac |
|
320 (simpset() addsimps [UN_oadd, lt_oadd1, |
|
321 oadd_le_self RS le_imp_not_lt, lt_Ord, |
|
322 odiff_oadd_inverse, ww2_def, |
|
323 vv2_subset RS Diff_partition]) 1); |
|
324 qed "UN_gg2_eq"; |
|
325 |
|
326 Goal "domain(gg2(f,a,b,s)) = a++a"; |
|
327 by (simp_tac (simpset() addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1); |
|
328 qed "domain_gg2"; |
|
329 |
|
330 (* ********************************************************************** *) |
|
331 (* every value of defined function is less than or equipollent to m *) |
|
332 (* ********************************************************************** *) |
|
333 |
|
334 Goalw [vv2_def] "[| m \\<in> nat; m\\<noteq>0 |] ==> vv2(f,b,g,s) lepoll m"; |
|
335 by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 1); |
|
336 by (fast_tac (claset() |
|
337 addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0] |
|
338 addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
|
339 not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll, |
|
340 nat_into_Ord, nat_1I]) 1); |
|
341 qed "vv2_lepoll"; |
|
342 |
|
343 Goalw [ww2_def] |
|
344 "[| \\<forall>b<a. f`b lepoll succ(m); g<a; m \\<in> nat; vv2(f,b,g,d) \\<subseteq> f`g |] \ |
|
345 \ ==> ww2(f,b,g,d) lepoll m"; |
|
346 by (excluded_middle_tac "f`g = 0" 1); |
|
347 by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2); |
|
348 by (dtac ospec 1 THEN (assume_tac 1)); |
|
349 by (rtac Diff_lepoll 1 THEN (TRYALL assume_tac)); |
|
350 by (asm_simp_tac (simpset() addsimps [vv2_def, not_emptyI]) 1); |
|
351 qed "ww2_lepoll"; |
|
352 |
|
353 Goalw [gg2_def] |
|
354 "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 --> \ |
|
355 \ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
|
356 \ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \ |
|
357 \ (\\<Union>b<a. f`b)=y; b<a; s \\<in> f`b; m \\<in> nat; m\\<noteq> 0; g<a++a \ |
|
358 \ |] ==> gg2(f,a,b,s) ` g lepoll m"; |
|
359 by (Asm_simp_tac 1); |
|
360 by (safe_tac (claset() addSEs [lt_oadd_odiff_cases, lt_Ord2])); |
|
361 by (asm_simp_tac (simpset() addsimps [vv2_lepoll]) 1); |
|
362 by (asm_simp_tac (simpset() addsimps [ww2_lepoll, vv2_subset]) 1); |
|
363 qed "gg2_lepoll_m"; |
|
364 |
|
365 (* ********************************************************************** *) |
|
366 (* lemma ii *) |
|
367 (* ********************************************************************** *) |
|
368 Goalw [NN_def] "[| succ(m) \\<in> NN(y); y*y \\<subseteq> y; m \\<in> nat; m\\<noteq>0 |] ==> m \\<in> NN(y)"; |
|
369 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1)); |
|
370 by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1 |
|
371 THEN (assume_tac 1)); |
|
372 (* case 1 *) |
|
373 by (asm_full_simp_tac (simpset() addsimps [lesspoll_succ_iff]) 1); |
|
374 by (res_inst_tac [("x","a++a")] exI 1); |
|
375 by (fast_tac (claset() addSIs [Ord_oadd, domain_gg1, UN_gg1_eq, |
|
376 gg1_lepoll_m]) 1); |
|
377 (* case 2 *) |
|
378 by (REPEAT (eresolve_tac [oexE, conjE] 1)); |
|
379 by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (assume_tac 1)); |
|
380 by (rtac CollectI 1); |
|
381 by (etac succ_natD 1); |
|
382 by (res_inst_tac [("x","a++a")] exI 1); |
|
383 by (res_inst_tac [("x","gg2(f,a,b,x)")] exI 1); |
|
384 (*Calling fast_tac might get rid of the res_inst_tac calls, but it |
|
385 is just too slow.*) |
|
386 by (asm_simp_tac (simpset() addsimps |
|
387 [Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1); |
|
388 qed "lemma_ii"; |
|
389 |
|
390 |
|
391 (* ********************************************************************** *) |
|
392 (* lemma iv - p. 4 \\<in> *) |
|
393 (* For every set x there is a set y such that x Un (y * y) \\<subseteq> y *) |
|
394 (* ********************************************************************** *) |
|
395 |
|
396 (* the quantifier \\<forall>looks inelegant but makes the proofs shorter *) |
|
397 (* (used only in the following two lemmas) *) |
|
398 |
|
399 Goal "\\<forall>n \\<in> nat. rec(n, x, %k r. r Un r*r) \\<subseteq> \ |
|
400 \ rec(succ(n), x, %k r. r Un r*r)"; |
|
401 by (fast_tac (claset() addIs [rec_succ RS ssubst]) 1); |
|
402 qed "z_n_subset_z_succ_n"; |
|
403 |
|
404 Goal "[| \\<forall>n \\<in> nat. f(n)<=f(succ(n)); n le m; n \\<in> nat; m \\<in> nat |] \ |
|
405 \ ==> f(n)<=f(m)"; |
|
406 by (eres_inst_tac [("P","n le m")] rev_mp 1); |
|
407 by (res_inst_tac [("P","%z. n le z --> f(n) \\<subseteq> f(z)")] nat_induct 1); |
|
408 by (REPEAT (fast_tac le_cs 1)); |
|
409 qed "le_subsets"; |
|
410 |
|
411 Goal "[| n le m; m \\<in> nat |] ==> \ |
|
412 \ rec(n, x, %k r. r Un r*r) \\<subseteq> rec(m, x, %k r. r Un r*r)"; |
|
413 by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1 |
|
414 THEN (TRYALL assume_tac)); |
|
415 by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1 |
|
416 THEN (assume_tac 1)); |
|
417 qed "le_imp_rec_subset"; |
|
418 |
|
419 Goal "\\<exists>y. x Un y*y \\<subseteq> y"; |
|
420 by (res_inst_tac [("x","\\<Union>n \\<in> nat. rec(n, x, %k r. r Un r*r)")] exI 1); |
|
421 by Safe_tac; |
|
422 by (rtac (nat_0I RS UN_I) 1); |
|
423 by (Asm_simp_tac 1); |
|
424 by (res_inst_tac [("a","succ(n Un na)")] UN_I 1); |
|
425 by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (assume_tac 1)); |
|
426 by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD] |
|
427 addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type] |
|
428 addSEs [nat_into_Ord] addss (simpset())) 1); |
|
429 qed "lemma_iv"; |
|
430 |
|
431 (* ********************************************************************** *) |
|
432 (* Rubin & Rubin wrote \\<in> *) |
|
433 (* "It follows from (ii) and mathematical induction that if y*y \\<subseteq> y then *) |
|
434 (* y can be well-ordered" *) |
|
435 |
|
436 (* In fact we have to prove \\<in> *) |
|
437 (* * WO6 ==> NN(y) \\<noteq> 0 *) |
|
438 (* * reverse induction which lets us infer that 1 \\<in> NN(y) *) |
|
439 (* * 1 \\<in> NN(y) ==> y can be well-ordered *) |
|
440 (* ********************************************************************** *) |
|
441 |
|
442 (* ********************************************************************** *) |
|
443 (* WO6 ==> NN(y) \\<noteq> 0 *) |
|
444 (* ********************************************************************** *) |
|
445 |
|
446 Goalw [WO6_def, NN_def] "WO6 ==> NN(y) \\<noteq> 0"; |
|
447 by (fast_tac ZF_cs 1); (*SLOW if current claset is used*) |
|
448 qed "WO6_imp_NN_not_empty"; |
|
449 |
|
450 (* ********************************************************************** *) |
|
451 (* 1 \\<in> NN(y) ==> y can be well-ordered *) |
|
452 (* ********************************************************************** *) |
|
453 |
|
454 Goal "[| (\\<Union>b<a. f`b)=y; x \\<in> y; \\<forall>b<a. f`b lepoll 1; Ord(a) |] \ |
|
455 \ ==> \\<exists>c<a. f`c = {x}"; |
|
456 by (fast_tac (claset() addSEs [lepoll_1_is_sing]) 1); |
|
457 val lemma1 = result(); |
|
458 |
|
459 Goal "[| (\\<Union>b<a. f`b)=y; x \\<in> y; \\<forall>b<a. f`b lepoll 1; Ord(a) |] \ |
|
460 \ ==> f` (LEAST i. f`i = {x}) = {x}"; |
|
461 by (dtac lemma1 1 THEN REPEAT (assume_tac 1)); |
|
462 by (fast_tac (claset() addSEs [lt_Ord] addIs [LeastI]) 1); |
|
463 val lemma2 = result(); |
|
464 |
|
465 Goalw [NN_def] "1 \\<in> NN(y) ==> \\<exists>a f. Ord(a) & f \\<in> inj(y, a)"; |
|
466 by (etac CollectE 1); |
|
467 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
|
468 by (res_inst_tac [("x","a")] exI 1); |
|
469 by (res_inst_tac [("x","\\<lambda>x \\<in> y. LEAST i. f`i = {x}")] exI 1); |
|
470 by (rtac conjI 1 THEN (assume_tac 1)); |
|
471 by (res_inst_tac [("d","%i. THE x. x \\<in> f`i")] lam_injective 1); |
|
472 by (dtac lemma1 1 THEN REPEAT (assume_tac 1)); |
|
473 by (fast_tac (claset() addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1); |
|
474 by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1)); |
|
475 by (Blast_tac 1); |
|
476 qed "NN_imp_ex_inj"; |
|
477 |
|
478 Goal "[| y*y \\<subseteq> y; 1 \\<in> NN(y) |] ==> \\<exists>r. well_ord(y, r)"; |
|
479 by (dtac NN_imp_ex_inj 1); |
|
480 by (fast_tac (claset() addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1); |
|
481 qed "y_well_ord"; |
|
482 |
|
483 (* ********************************************************************** *) |
|
484 (* reverse induction which lets us infer that 1 \\<in> NN(y) *) |
|
485 (* ********************************************************************** *) |
|
486 |
|
487 val [prem1, prem2] = goal thy |
|
488 "[| n \\<in> nat; !!m. [| m \\<in> nat; m\\<noteq>0; P(succ(m)) |] ==> P(m) |] \ |
|
489 \ ==> n\\<noteq>0 --> P(n) --> P(1)"; |
|
490 by (rtac (prem1 RS nat_induct) 1); |
|
491 by (Blast_tac 1); |
|
492 by (excluded_middle_tac "x=0" 1); |
|
493 by (Blast_tac 2); |
|
494 by (fast_tac (claset() addSIs [prem2]) 1); |
|
495 qed "rev_induct_lemma"; |
|
496 |
|
497 val prems = |
|
498 Goal "[| P(n); n \\<in> nat; n\\<noteq>0; \ |
|
499 \ !!m. [| m \\<in> nat; m\\<noteq>0; P(succ(m)) |] ==> P(m) |] \ |
|
500 \ ==> P(1)"; |
|
501 by (resolve_tac [rev_induct_lemma RS impE] 1); |
|
502 by (etac impE 4 THEN (assume_tac 5)); |
|
503 by (REPEAT (ares_tac prems 1)); |
|
504 qed "rev_induct"; |
|
505 |
|
506 Goalw [NN_def] "n \\<in> NN(y) ==> n \\<in> nat"; |
|
507 by (etac CollectD1 1); |
|
508 qed "NN_into_nat"; |
|
509 |
|
510 Goal "[| n \\<in> NN(y); y*y \\<subseteq> y; n\\<noteq>0 |] ==> 1 \\<in> NN(y)"; |
|
511 by (rtac rev_induct 1 THEN REPEAT (ares_tac [NN_into_nat] 1)); |
|
512 by (rtac lemma_ii 1 THEN REPEAT (assume_tac 1)); |
|
513 val lemma3 = result(); |
|
514 |
|
515 (* ********************************************************************** *) |
|
516 (* Main theorem "WO6 ==> WO1" *) |
|
517 (* ********************************************************************** *) |
|
518 |
|
519 (* another helpful lemma *) |
|
520 Goalw [NN_def] "0 \\<in> NN(y) ==> y=0"; |
|
521 by (fast_tac (claset() addSIs [equalityI] |
|
522 addSDs [lepoll_0_is_0] addEs [subst]) 1); |
|
523 qed "NN_y_0"; |
|
524 |
|
525 Goalw [WO1_def] "WO6 ==> WO1"; |
|
526 by (rtac allI 1); |
|
527 by (excluded_middle_tac "A=0" 1); |
|
528 by (fast_tac (claset() addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2); |
|
529 by (res_inst_tac [("x1","A")] (lemma_iv RS revcut_rl) 1); |
|
530 by (etac exE 1); |
|
531 by (dtac WO6_imp_NN_not_empty 1); |
|
532 by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1); |
|
533 by (eres_inst_tac [("A","NN(y)")] not_emptyE 1); |
|
534 by (ftac y_well_ord 1); |
|
535 by (fast_tac (claset() addEs [well_ord_subset]) 2); |
|
536 by (fast_tac (claset() addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1); |
|
537 qed "WO6_imp_WO1"; |
|
538 |
|