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