|
1 (* Title: ZF/AC/WO6_WO1.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Gr`abczewski |
|
4 |
|
5 The proof of "WO6 ==> WO1". |
|
6 |
|
7 From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin, |
|
8 pages 2-5 |
|
9 *) |
|
10 |
|
11 (* ********************************************************************** *) |
|
12 (* The most complicated part of the proof - lemma ii - p. 2-4 *) |
|
13 (* ********************************************************************** *) |
|
14 |
|
15 (* ********************************************************************** *) |
|
16 (* some properties of relation uu(beta, gamma, delta) - p. 2 *) |
|
17 (* ********************************************************************** *) |
|
18 |
|
19 goalw thy [uu_def] "domain(uu(f,b,g,d)) <= f`b"; |
|
20 by (fast_tac ZF_cs 1); |
|
21 val domain_uu_subset = result(); |
|
22 |
|
23 goal thy "!!a. [| ALL b<a. f`b lepoll m; b<a |] \ |
|
24 \ ==> domain(uu(f, b, g, d)) lepoll m"; |
|
25 by (fast_tac (AC_cs addSEs |
|
26 [domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1); |
|
27 val domain_uu_lepoll_m = result(); |
|
28 |
|
29 goal thy "!! a. ALL b<a. f`b lepoll m ==> \ |
|
30 \ ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m"; |
|
31 by (fast_tac (AC_cs addEs [domain_uu_lepoll_m]) 1); |
|
32 val quant_domain_uu_lepoll_m = result(); |
|
33 |
|
34 (* used in case 2 *) |
|
35 goalw thy [uu_def] "uu(f,b,g,d) <= f`b * f`g"; |
|
36 by (fast_tac ZF_cs 1); |
|
37 val uu_subset1 = result(); |
|
38 |
|
39 goalw thy [uu_def] "uu(f,b,g,d) <= f`d"; |
|
40 by (fast_tac ZF_cs 1); |
|
41 val uu_subset2 = result(); |
|
42 |
|
43 goal thy "!! a. [| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m"; |
|
44 by (fast_tac (AC_cs |
|
45 addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1); |
|
46 val uu_lepoll_m = result(); |
|
47 |
|
48 (* ********************************************************************** *) |
|
49 (* Two cases for lemma ii *) |
|
50 (* ********************************************************************** *) |
|
51 goalw thy [lesspoll_def] |
|
52 "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==> \ |
|
53 \ (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & \ |
|
54 \ u(f,b,g,d) lesspoll m)) | \ |
|
55 \ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \ |
|
56 \ u(f,b,g,d) eqpoll m))"; |
|
57 by (fast_tac AC_cs 1); |
|
58 val cases = result(); |
|
59 |
|
60 (* ********************************************************************** *) |
|
61 (* Lemmas used in both cases *) |
|
62 (* ********************************************************************** *) |
|
63 goal thy "!!a f. Ord(a) ==> (UN b<a++a. f`b) = (UN b<a. f`b Un f`(a++b))"; |
|
64 by (resolve_tac [equalityI] 1); |
|
65 by (fast_tac (AC_cs addIs [ltI, OUN_I] addSEs [OUN_E] |
|
66 addSDs [lt_oadd_disj]) 1); |
|
67 by (fast_tac (AC_cs addSEs [lt_oadd1, oadd_lt_mono2, OUN_E] |
|
68 addSIs [OUN_I]) 1); |
|
69 val UN_oadd = result(); |
|
70 |
|
71 val [prem] = goal thy |
|
72 "(!!b. b<a ==> P(b)=Q(b)) ==> (UN b<a. P(b)) = (UN b<a. Q(b))"; |
|
73 by (fast_tac (ZF_cs addSIs [OUN_I, equalityI] |
|
74 addSEs [OUN_E, prem RS equalityD1 RS subsetD, |
|
75 prem RS sym RS equalityD1 RS subsetD]) 1); |
|
76 val UN_eq = result(); |
|
77 |
|
78 goal thy "!!a. b<a ==> b = (THE l. l<a & a ++ b = a ++ l)"; |
|
79 by (fast_tac (ZF_cs addSIs [the_equality RS sym] |
|
80 addIs [lt_Ord2, lt_Ord] |
|
81 addSEs [oadd_inject RS sym]) 1); |
|
82 val the_only_b = result(); |
|
83 |
|
84 goal thy "!!A. B <= A ==> B Un (A-B) = A"; |
|
85 by (fast_tac (ZF_cs addSIs [equalityI]) 1); |
|
86 val subset_imp_Un_Diff_eq = result(); |
|
87 |
|
88 (* ********************************************************************** *) |
|
89 (* Case 1 : lemmas *) |
|
90 (* ********************************************************************** *) |
|
91 |
|
92 goalw thy [vv1_def] "vv1(f,b,succ(m)) <= f`b"; |
|
93 by (resolve_tac [expand_if RS iffD2] 1); |
|
94 by (fast_tac (ZF_cs addSIs [domain_uu_subset]) 1); |
|
95 val vv1_subset = result(); |
|
96 |
|
97 (* ********************************************************************** *) |
|
98 (* Case 1 : Union of images is the whole "y" *) |
|
99 (* ********************************************************************** *) |
|
100 goal thy "!! a f y. [| (UN b<a. f`b) = y; Ord(a); m:nat |] ==> \ |
|
101 \ (UN b<a++a. (lam b:a++a. if(b<a, vv1(f,b,succ(m)), \ |
|
102 \ ww1(f, THE l. l<a & b=a++l, succ(m)))) ` b) = y"; |
|
103 by (resolve_tac [UN_oadd RS ssubst] 1 THEN (atac 1)); |
|
104 by (eresolve_tac [subst] 1); |
|
105 by (resolve_tac [UN_eq] 1); |
|
106 by (forw_inst_tac [("i","a")] lt_oadd1 1 |
|
107 THEN (REPEAT (atac 1))); |
|
108 by (forw_inst_tac [("j","a")] oadd_lt_mono2 1 |
|
109 THEN (REPEAT (atac 1))); |
|
110 by (asm_simp_tac (ZF_ss addsimps [ltD RS beta, |
|
111 oadd_le_self RS le_imp_not_lt RS if_not_P, lt_Ord]) 1); |
|
112 by (resolve_tac [the_only_b RS subst] 1 THEN (atac 1)); |
|
113 by (asm_simp_tac (ZF_ss |
|
114 addsimps [vv1_subset RS subset_imp_Un_Diff_eq, ltD, ww1_def]) 1); |
|
115 val UN_eq_y = result(); |
|
116 |
|
117 (* ********************************************************************** *) |
|
118 (* every value of defined function is less than or equipollent to m *) |
|
119 (* ********************************************************************** *) |
|
120 goal thy "!!a b. [| P(a, b); Ord(a); Ord(b); \ |
|
121 \ Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |] \ |
|
122 \ ==> P(Least_a, LEAST b. P(Least_a, b))"; |
|
123 by (eresolve_tac [ssubst] 1); |
|
124 by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1); |
|
125 by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1)); |
|
126 val nested_LeastI = result(); |
|
127 |
|
128 val nested_Least_instance = read_instantiate |
|
129 [("P","%g d. domain(uu(f,b,g,d)) ~= 0 & \ |
|
130 \ domain(uu(f,b,g,d)) lesspoll succ(m)")] nested_LeastI; |
|
131 |
|
132 goalw thy [vv1_def] "!!a. [| ALL b<a. f`b ~=0 --> \ |
|
133 \ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \ |
|
134 \ domain(uu(f,b,g,d)) lesspoll succ(m)); m:nat; b<a |] \ |
|
135 \ ==> vv1(f,b,succ(m)) lesspoll succ(m)"; |
|
136 by (resolve_tac [expand_if RS iffD2] 1); |
|
137 by (fast_tac (AC_cs addIs [nested_Least_instance RS conjunct2] |
|
138 addSEs [lt_Ord] |
|
139 addSIs [empty_lepollI RS lepoll_imp_lesspoll_succ]) 1); |
|
140 val vv1_lesspoll_succ = result(); |
|
141 |
|
142 goalw thy [vv1_def] "!!a. [| ALL b<a. f`b ~=0 --> \ |
|
143 \ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \ |
|
144 \ domain(uu(f,b,g,d)) lesspoll succ(m)); m:nat; b<a; f`b ~= 0 |] \ |
|
145 \ ==> vv1(f,b,succ(m)) ~= 0"; |
|
146 by (resolve_tac [expand_if RS iffD2] 1); |
|
147 by (resolve_tac [conjI] 1); |
|
148 by (fast_tac ZF_cs 2); |
|
149 by (resolve_tac [impI] 1); |
|
150 by (eresolve_tac [oallE] 1); |
|
151 by (mp_tac 1); |
|
152 by (contr_tac 2); |
|
153 by (REPEAT (eresolve_tac [oexE] 1)); |
|
154 by (asm_simp_tac (ZF_ss |
|
155 addsimps [lt_Ord, nested_Least_instance RS conjunct1]) 1); |
|
156 val vv1_not_0 = result(); |
|
157 |
|
158 goalw thy [ww1_def] "!!a. [| ALL b<a. f`b ~=0 --> \ |
|
159 \ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \ |
|
160 \ domain(uu(f,b,g,d)) lesspoll succ(m)); \ |
|
161 \ ALL b<a. f`b lepoll succ(m); m:nat; b<a |] \ |
|
162 \ ==> ww1(f,b,succ(m)) lesspoll succ(m)"; |
|
163 by (excluded_middle_tac "f`b = 0" 1); |
|
164 by (asm_full_simp_tac (AC_ss |
|
165 addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2); |
|
166 by (resolve_tac [Diff_lepoll RS lepoll_imp_lesspoll_succ] 1); |
|
167 by (fast_tac AC_cs 1); |
|
168 by (REPEAT (ares_tac [vv1_subset, vv1_not_0] 1)); |
|
169 val ww1_lesspoll_succ = result(); |
|
170 |
|
171 goal thy "!!a. [| Ord(a); m:nat; \ |
|
172 \ ALL b<a. f`b ~=0 --> (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \ |
|
173 \ domain(uu(f,b,g,d)) lesspoll succ(m)); \ |
|
174 \ ALL b<a. f`b lepoll succ(m) |] \ |
|
175 \ ==> ALL b<a++a. (lam b:a++a. if(b<a, vv1(f,b,succ(m)), \ |
|
176 \ ww1(f,THE l. l<a & b = a ++ l,succ(m))))`b lepoll m"; |
|
177 by (resolve_tac [oallI] 1); |
|
178 by (asm_full_simp_tac (ZF_ss addsimps [ltD RS beta]) 1); |
|
179 by (resolve_tac [lesspoll_succ_imp_lepoll] 1 THEN (atac 2)); |
|
180 by (resolve_tac [expand_if RS iffD2] 1); |
|
181 by (resolve_tac [conjI] 1); |
|
182 by (resolve_tac [impI] 1); |
|
183 by (forward_tac [lt_oadd_disj1] 2 THEN (REPEAT (atac 2))); |
|
184 by (resolve_tac [impI] 2); |
|
185 by (eresolve_tac [disjE] 2 THEN (fast_tac (ZF_cs addSEs [ltE]) 2)); |
|
186 by (asm_full_simp_tac (ZF_ss addsimps [vv1_lesspoll_succ]) 1); |
|
187 by (dresolve_tac [theI] 1); |
|
188 by (eresolve_tac [conjE] 1); |
|
189 by (resolve_tac [ww1_lesspoll_succ] 1 THEN (REPEAT (atac 1))); |
|
190 val all_sum_lepoll_m = result(); |
|
191 |
|
192 (* ********************************************************************** *) |
|
193 (* Case 2 : lemmas *) |
|
194 (* ********************************************************************** *) |
|
195 |
|
196 (* ********************************************************************** *) |
|
197 (* Case 2 : vv2_subset *) |
|
198 (* ********************************************************************** *) |
|
199 |
|
200 goalw thy [uu_def] "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
|
201 \ y*y <= y; (UN b<a. f`b)=y |] \ |
|
202 \ ==> EX d<a. uu(f,b,g,d)~=0"; |
|
203 by (fast_tac (AC_cs addSIs [not_emptyI] |
|
204 addSDs [SigmaI RSN (2, subsetD)] |
|
205 addSEs [not_emptyE]) 1); |
|
206 val ex_d_uu_not_empty = result(); |
|
207 |
|
208 goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
|
209 \ y*y<=y; (UN b<a. f`b)=y |] \ |
|
210 \ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0"; |
|
211 by (dresolve_tac [ex_d_uu_not_empty] 1 THEN (REPEAT (atac 1))); |
|
212 by (fast_tac (AC_cs addSEs [LeastI, lt_Ord]) 1); |
|
213 val uu_not_empty = result(); |
|
214 |
|
215 (* moved from ZF_aux.ML *) |
|
216 goal thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0"; |
|
217 by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, |
|
218 sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1)); |
|
219 val not_empty_rel_imp_domain = result(); |
|
220 |
|
221 goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
|
222 \ y*y <= y; (UN b<a. f`b)=y |] \ |
|
223 \ ==> (LEAST d. uu(f,b,g,d) ~= 0) < a"; |
|
224 by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1 |
|
225 THEN (REPEAT (atac 1))); |
|
226 by (resolve_tac [Least_le RS lt_trans1] 1 |
|
227 THEN (REPEAT (ares_tac [lt_Ord] 1))); |
|
228 val Least_uu_not_empty_lt_a = result(); |
|
229 |
|
230 goal thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}"; |
|
231 by (fast_tac ZF_cs 1); |
|
232 val subset_Diff_sing = result(); |
|
233 |
|
234 goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B"; |
|
235 by (eresolve_tac [natE] 1); |
|
236 by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1); |
|
237 by (hyp_subst_tac 1); |
|
238 by (resolve_tac [equalityI] 1); |
|
239 by (atac 2); |
|
240 by (resolve_tac [subsetI] 1); |
|
241 by (excluded_middle_tac "?P" 1 THEN (atac 2)); |
|
242 by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2, |
|
243 diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS |
|
244 succ_lepoll_natE] 1 |
|
245 THEN (REPEAT (atac 1))); |
|
246 val supset_lepoll_imp_eq = result(); |
|
247 |
|
248 goalw thy [vv2_def] |
|
249 "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \ |
|
250 \ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
|
251 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
|
252 \ (UN b<a. f`b)=y; b<a; g<a; d<a; f`b~=0; f`g~=0; m:nat; aa:f`b |] \ |
|
253 \ ==> uu(f,b,g,LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g"; |
|
254 by (eres_inst_tac [("x","g")] oallE 1 THEN (contr_tac 2)); |
|
255 by (eres_inst_tac [("P","%z. ?QQ(z) ~= 0 --> ?RR(z)")] oallE 1); |
|
256 by (eresolve_tac [impE] 1); |
|
257 by (eresolve_tac [uu_not_empty RS (uu_subset1 RS |
|
258 not_empty_rel_imp_domain)] 1 |
|
259 THEN (REPEAT (atac 1))); |
|
260 by (eresolve_tac [Least_uu_not_empty_lt_a RSN (2, notE)] 2 |
|
261 THEN (TRYALL atac)); |
|
262 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS |
|
263 (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2, |
|
264 uu_subset1 RSN (4, rel_is_fun)))] 1 |
|
265 THEN (TRYALL atac)); |
|
266 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, |
|
267 supset_lepoll_imp_eq)] 1); |
|
268 by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1)); |
|
269 val uu_Least_is_fun = result(); |
|
270 |
|
271 goalw thy [vv2_def] |
|
272 "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \ |
|
273 \ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
|
274 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
|
275 \ (UN b<a. f`b)=y; b<a; g<a; m:nat; aa:f`b |] \ |
|
276 \ ==> vv2(f,b,g,aa) <= f`g"; |
|
277 by (fast_tac (FOL_cs addIs [expand_if RS iffD2] |
|
278 addSEs [uu_Least_is_fun] |
|
279 addSIs [empty_subsetI, not_emptyI, |
|
280 singleton_subsetI, apply_type]) 1); |
|
281 val vv2_subset = result(); |
|
282 |
|
283 (* ********************************************************************** *) |
|
284 (* Case 2 : Union of images is the whole "y" *) |
|
285 (* ********************************************************************** *) |
|
286 goal thy "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \ |
|
287 \ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
|
288 \ ALL b<a. f`b lepoll succ(m); y*y<=y; \ |
|
289 \ (UN b<a.f`b)=y; Ord(a); m:nat; aa:f`b; b<a |] \ |
|
290 \ ==> (UN g<a++a. (lam g:a++a. if(g<a, vv2(f,b,g,aa), \ |
|
291 \ ww2(f,b,THE l. l<a & g=a++l,aa)))`g) = y"; |
|
292 by (resolve_tac [UN_oadd RS ssubst] 1 THEN (atac 1)); |
|
293 by (resolve_tac [subst] 1 THEN (atac 1)); |
|
294 by (resolve_tac [UN_eq] 1); |
|
295 by (forw_inst_tac [("i","a"),("k","ba")] lt_oadd1 1 |
|
296 THEN (REPEAT (atac 1))); |
|
297 by (forw_inst_tac [("j","a"),("k","ba")] oadd_lt_mono2 1 |
|
298 THEN (REPEAT (atac 1))); |
|
299 by (asm_simp_tac (ZF_ss addsimps [ltD RS beta, |
|
300 oadd_le_self RS le_imp_not_lt RS if_not_P, lt_Ord]) 1); |
|
301 by (resolve_tac [the_only_b RS subst] 1 THEN (atac 1)); |
|
302 by (asm_simp_tac (ZF_ss |
|
303 addsimps [vv2_subset RS subset_imp_Un_Diff_eq, ltI, ww2_def]) 1); |
|
304 val UN_eq_y_2 = result(); |
|
305 |
|
306 (* ********************************************************************** *) |
|
307 (* every value of defined function is less than or equipollent to m *) |
|
308 (* ********************************************************************** *) |
|
309 |
|
310 goalw thy [vv2_def] |
|
311 "!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,aa) lesspoll succ(m)"; |
|
312 by (resolve_tac [conjI RS (expand_if RS iffD2)] 1); |
|
313 by (asm_simp_tac (AC_ss |
|
314 addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2); |
|
315 by (fast_tac (AC_cs |
|
316 addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0] |
|
317 addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS |
|
318 lepoll_trans RS lepoll_imp_lesspoll_succ, |
|
319 not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll, |
|
320 nat_into_Ord, nat_1I]) 1); |
|
321 val vv2_lesspoll_succ = result(); |
|
322 |
|
323 goalw thy [ww2_def] "!!m. [| ALL b<a. f`b lepoll succ(m); g<a; m:nat; \ |
|
324 \ vv2(f,b,g,d) <= f`g |] \ |
|
325 \ ==> ww2(f,b,g,d) lesspoll succ(m)"; |
|
326 by (excluded_middle_tac "f`g = 0" 1); |
|
327 by (asm_simp_tac (AC_ss |
|
328 addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2); |
|
329 by (dresolve_tac [ospec] 1 THEN (atac 1)); |
|
330 by (resolve_tac [Diff_lepoll RS lepoll_imp_lesspoll_succ] 1 |
|
331 THEN (TRYALL atac)); |
|
332 by (asm_simp_tac (AC_ss addsimps [vv2_def, expand_if, not_emptyI]) 1); |
|
333 val ww2_lesspoll_succ = result(); |
|
334 |
|
335 goal thy "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \ |
|
336 \ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
|
337 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
|
338 \ (UN b<a. f`b)=y; b<a; aa:f`b; m:nat; m~= 0 |] \ |
|
339 \ ==> ALL ba<a++a. (lam g:a++a. if(g<a, vv2(f,b,g,aa), \ |
|
340 \ ww2(f,b,THE l. l<a & g=a++l,aa)))`ba lepoll m"; |
|
341 by (resolve_tac [oallI] 1); |
|
342 by (asm_full_simp_tac AC_ss 1); |
|
343 by (resolve_tac [lesspoll_succ_imp_lepoll] 1 THEN (atac 2)); |
|
344 by (resolve_tac [conjI RS (expand_if RS iffD2)] 1); |
|
345 by (asm_simp_tac (AC_ss addsimps [vv2_lesspoll_succ]) 1); |
|
346 by (forward_tac [lt_oadd_disj1] 1 THEN (REPEAT (ares_tac [lt_Ord2] 1))); |
|
347 by (fast_tac (FOL_cs addSIs [ww2_lesspoll_succ, vv2_subset] |
|
348 addSDs [theI]) 1); |
|
349 val all_sum_lepoll_m_2 = result(); |
|
350 |
|
351 (* ********************************************************************** *) |
|
352 (* lemma ii *) |
|
353 (* ********************************************************************** *) |
|
354 goalw thy [NN_def] |
|
355 "!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)"; |
|
356 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1)); |
|
357 by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1 |
|
358 THEN (atac 1)); |
|
359 (* case 1 *) |
|
360 by (resolve_tac [CollectI] 1); |
|
361 by (atac 1); |
|
362 by (res_inst_tac [("x","a ++ a")] exI 1); |
|
363 by (res_inst_tac [("x","lam b:a++a. if (b<a, vv1(f,b,succ(m)), \ |
|
364 \ ww1(f,THE l. l<a & b=a++l,succ(m)))")] exI 1); |
|
365 by (fast_tac (FOL_cs addSIs [Ord_oadd, lam_funtype RS domain_of_fun, |
|
366 UN_eq_y, all_sum_lepoll_m]) 1); |
|
367 (* case 2 *) |
|
368 by (REPEAT (eresolve_tac [oexE, conjE] 1)); |
|
369 by (resolve_tac [CollectI] 1); |
|
370 by (eresolve_tac [succ_natD] 1); |
|
371 by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (atac 1)); |
|
372 by (res_inst_tac [("x","a++a")] exI 1); |
|
373 by (res_inst_tac [("x","lam g:a++a. if (g<a, vv2(f,b,g,x), \ |
|
374 \ ww2(f,b,THE l. l<a & g=a++l,x))")] exI 1); |
|
375 by (fast_tac (FOL_cs addSIs [Ord_oadd, lam_funtype RS domain_of_fun, |
|
376 UN_eq_y_2, all_sum_lepoll_m_2]) 1); |
|
377 val lemma_ii = result(); |
|
378 |
|
379 |
|
380 (* ********************************************************************** *) |
|
381 (* lemma iv - p. 4 : *) |
|
382 (* For every set x there is a set y such that x Un (y * y) <= y *) |
|
383 (* ********************************************************************** *) |
|
384 |
|
385 (* the quantifier ALL looks inelegant but makes the proofs shorter *) |
|
386 (* (used only in the following two lemmas) *) |
|
387 |
|
388 goal thy "ALL n:nat. rec(n, x, %k r. r Un r*r) <= \ |
|
389 \ rec(succ(n), x, %k r. r Un r*r)"; |
|
390 by (fast_tac (ZF_cs addIs [rec_succ RS ssubst]) 1); |
|
391 val z_n_subset_z_succ_n = result(); |
|
392 |
|
393 goal thy "!!n. [| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |] \ |
|
394 \ ==> f(n)<=f(m)"; |
|
395 by (res_inst_tac [("P","n le m")] impE 1 THEN (REPEAT (atac 2))); |
|
396 by (res_inst_tac [("P","%z. n le z --> f(n) <= f(z)")] nat_induct 1); |
|
397 by (REPEAT (fast_tac lt_cs 1)); |
|
398 val le_subsets = result(); |
|
399 |
|
400 goal thy "!!n m. [| n le m; m:nat |] ==> \ |
|
401 \ rec(n, x, %k r. r Un r*r) <= rec(m, x, %k r. r Un r*r)"; |
|
402 by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1 |
|
403 THEN (TRYALL atac)); |
|
404 by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1 |
|
405 THEN (atac 1)); |
|
406 val le_imp_rec_subset = result(); |
|
407 |
|
408 goal thy "!!x. EX y. x Un y*y <= y"; |
|
409 by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1); |
|
410 by (resolve_tac [subsetI] 1); |
|
411 by (eresolve_tac [UnE] 1); |
|
412 by (resolve_tac [UN_I] 1); |
|
413 by (eresolve_tac [rec_0 RS ssubst] 2); |
|
414 by (resolve_tac [nat_0I] 1); |
|
415 by (eresolve_tac [SigmaE] 1); |
|
416 by (REPEAT (eresolve_tac [UN_E] 1)); |
|
417 by (res_inst_tac [("a","succ(n Un na)")] UN_I 1); |
|
418 by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (atac 1)); |
|
419 by (resolve_tac [rec_succ RS ssubst] 1); |
|
420 by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD] |
|
421 addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type] |
|
422 addSEs [nat_into_Ord]) 1); |
|
423 val lemma_iv = result(); |
|
424 |
|
425 (* ********************************************************************** *) |
|
426 (* Rubin & Rubin wrote : *) |
|
427 (* "It follows from (ii) and mathematical induction that if y*y <= y then *) |
|
428 (* y can be well-ordered" *) |
|
429 |
|
430 (* In fact we have to prove : *) |
|
431 (* * WO6 ==> NN(y) ~= 0 *) |
|
432 (* * reverse induction which lets us infer that 1 : NN(y) *) |
|
433 (* * 1 : NN(y) ==> y can be well-ordered *) |
|
434 (* ********************************************************************** *) |
|
435 |
|
436 (* ********************************************************************** *) |
|
437 (* WO6 ==> NN(y) ~= 0 *) |
|
438 (* ********************************************************************** *) |
|
439 |
|
440 goalw thy [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0"; |
|
441 by (eresolve_tac [allE] 1); |
|
442 by (fast_tac (ZF_cs addSIs [not_emptyI]) 1); |
|
443 val WO6_imp_NN_not_empty = result(); |
|
444 |
|
445 (* ********************************************************************** *) |
|
446 (* 1 : NN(y) ==> y can be well-ordered *) |
|
447 (* ********************************************************************** *) |
|
448 |
|
449 goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \ |
|
450 \ ==> EX c<a. f`c = {x}"; |
|
451 by (fast_tac (AC_cs addSEs [lepoll_1_is_sing]) 1); |
|
452 val lemma1 = result(); |
|
453 |
|
454 goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \ |
|
455 \ ==> f` (LEAST i. f`i = {x}) = {x}"; |
|
456 by (dresolve_tac [lemma1] 1 THEN (REPEAT (atac 1))); |
|
457 by (fast_tac (AC_cs addSEs [lt_Ord] addIs [LeastI]) 1); |
|
458 val lemma2 = result(); |
|
459 |
|
460 goalw thy [NN_def] "!!y. 1 : NN(y) ==> EX a f. Ord(a) & f:inj(y, a)"; |
|
461 by (eresolve_tac [CollectE] 1); |
|
462 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
|
463 by (res_inst_tac [("x","a")] exI 1); |
|
464 by (res_inst_tac [("x","lam x:y. LEAST i. f`i = {x}")] exI 1); |
|
465 by (resolve_tac [conjI] 1 THEN (atac 1)); |
|
466 by (res_inst_tac [("d","%i. THE x. x:f`i")] lam_injective 1); |
|
467 by (dresolve_tac [lemma1] 1 THEN (REPEAT (atac 1))); |
|
468 by (fast_tac (AC_cs addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1); |
|
469 by (resolve_tac [lemma2 RS ssubst] 1 THEN (REPEAT (atac 1))); |
|
470 by (fast_tac (ZF_cs addSIs [the_equality]) 1); |
|
471 val NN_imp_ex_inj = result(); |
|
472 |
|
473 goal thy "!!y. [| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)"; |
|
474 by (dresolve_tac [NN_imp_ex_inj] 1); |
|
475 by (fast_tac (ZF_cs addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1); |
|
476 val y_well_ord = result(); |
|
477 |
|
478 (* ********************************************************************** *) |
|
479 (* reverse induction which lets us infer that 1 : NN(y) *) |
|
480 (* ********************************************************************** *) |
|
481 |
|
482 val [prem1, prem2] = goal thy |
|
483 "[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \ |
|
484 \ ==> n~=0 --> P(n) --> P(1)"; |
|
485 by (res_inst_tac [("n","n")] nat_induct 1); |
|
486 by (resolve_tac [prem1] 1); |
|
487 by (fast_tac ZF_cs 1); |
|
488 by (excluded_middle_tac "x=0" 1); |
|
489 by (fast_tac ZF_cs 2); |
|
490 by (fast_tac (ZF_cs addSIs [prem2]) 1); |
|
491 val rev_induct_lemma = result(); |
|
492 |
|
493 val prems = goal thy |
|
494 "[| P(n); n:nat; n~=0; \ |
|
495 \ !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \ |
|
496 \ ==> P(1)"; |
|
497 by (resolve_tac [rev_induct_lemma RS impE] 1); |
|
498 by (eresolve_tac [impE] 4 THEN (atac 5)); |
|
499 by (REPEAT (ares_tac prems 1)); |
|
500 val rev_induct = result(); |
|
501 |
|
502 goalw thy [NN_def] "!!n. n:NN(y) ==> n:nat"; |
|
503 by (fast_tac ZF_cs 1); |
|
504 val NN_into_nat = result(); |
|
505 |
|
506 goal thy "!!n. [| n:NN(y); y*y <= y; n~=0 |] ==> 1:NN(y)"; |
|
507 by (resolve_tac [rev_induct] 1 THEN (REPEAT (ares_tac [NN_into_nat] 1))); |
|
508 by (resolve_tac [lemma_ii] 1 THEN (REPEAT (atac 1))); |
|
509 val lemma3 = result(); |
|
510 |
|
511 (* ********************************************************************** *) |
|
512 (* Main theorem "WO6 ==> WO1" *) |
|
513 (* ********************************************************************** *) |
|
514 |
|
515 (* another helpful lemma *) |
|
516 goalw thy [NN_def] "!!y. 0:NN(y) ==> y=0"; |
|
517 by (fast_tac (AC_cs addSIs [equalityI] |
|
518 addSDs [lepoll_0_is_0] addEs [subst]) 1); |
|
519 val NN_y_0 = result(); |
|
520 |
|
521 goalw thy [WO1_def] "!!Z. WO6 ==> WO1"; |
|
522 by (resolve_tac [allI] 1); |
|
523 by (excluded_middle_tac "A=0" 1); |
|
524 by (fast_tac (ZF_cs addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2); |
|
525 by (res_inst_tac [("x1","A")] (lemma_iv RS revcut_rl) 1); |
|
526 by (eresolve_tac [exE] 1); |
|
527 by (dresolve_tac [WO6_imp_NN_not_empty] 1); |
|
528 by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1); |
|
529 by (eres_inst_tac [("A","NN(y)")] not_emptyE 1); |
|
530 by (forward_tac [y_well_ord] 1); |
|
531 by (fast_tac (ZF_cs addEs [well_ord_subset]) 2); |
|
532 by (fast_tac (ZF_cs addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1); |
|
533 qed "WO6_imp_WO1"; |
|
534 |