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