author | paulson |
Tue, 08 Jan 2002 16:09:09 +0100 | |
changeset 12667 | 7e6eaaa125f2 |
parent 11380 | e76366922751 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/WO6_WO1.ML |
992 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
992 | 4 |
|
11380 | 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_"; |
|
992 | 42 |
|
11380 | 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 |
************************************************************************* *) |
|
992 | 88 |
|
1041 | 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 |
|
4091 | 95 |
(simpset() addsimps [oadd_odiff_inverse, odiff_oadd_inverse]) 4); |
96 |
by (safe_tac (claset() addSEs [lt_Ord])); |
|
3731 | 97 |
qed "lt_oadd_odiff_disj"; |
1041 | 98 |
|
99 |
(*The corresponding elimination rule*) |
|
4152 | 100 |
val lt_oadd_odiff_cases = rule_by_tactic Safe_tac |
1041 | 101 |
(lt_oadd_odiff_disj RS disjE); |
102 |
||
992 | 103 |
(* ********************************************************************** *) |
1461 | 104 |
(* The most complicated part of the proof - lemma ii - p. 2-4 *) |
992 | 105 |
(* ********************************************************************** *) |
106 |
||
107 |
(* ********************************************************************** *) |
|
1461 | 108 |
(* some properties of relation uu(beta, gamma, delta) - p. 2 *) |
992 | 109 |
(* ********************************************************************** *) |
110 |
||
11317 | 111 |
Goalw [uu_def] "domain(uu(f,b,g,d)) \\<subseteq> f`b"; |
3731 | 112 |
by (Blast_tac 1); |
113 |
qed "domain_uu_subset"; |
|
992 | 114 |
|
11317 | 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"; |
|
4091 | 117 |
by (fast_tac (claset() addSEs |
1461 | 118 |
[domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1); |
3731 | 119 |
qed "quant_domain_uu_lepoll_m"; |
992 | 120 |
|
11317 | 121 |
Goalw [uu_def] "uu(f,b,g,d) \\<subseteq> f`b * f`g"; |
3731 | 122 |
by (Blast_tac 1); |
123 |
qed "uu_subset1"; |
|
992 | 124 |
|
11317 | 125 |
Goalw [uu_def] "uu(f,b,g,d) \\<subseteq> f`d"; |
3731 | 126 |
by (Blast_tac 1); |
127 |
qed "uu_subset2"; |
|
992 | 128 |
|
11317 | 129 |
Goal "[| \\<forall>b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m"; |
4091 | 130 |
by (fast_tac (claset() |
1461 | 131 |
addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1); |
3731 | 132 |
qed "uu_lepoll_m"; |
992 | 133 |
|
134 |
(* ********************************************************************** *) |
|
1461 | 135 |
(* Two cases for lemma ii *) |
992 | 136 |
(* ********************************************************************** *) |
5068 | 137 |
Goalw [lesspoll_def] |
11317 | 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 --> \ |
|
1461 | 142 |
\ u(f,b,g,d) eqpoll m))"; |
2469 | 143 |
by (Asm_simp_tac 1); |
4091 | 144 |
by (blast_tac (claset() delrules [equalityI]) 1); |
3731 | 145 |
qed "cases"; |
992 | 146 |
|
147 |
(* ********************************************************************** *) |
|
1461 | 148 |
(* Lemmas used in both cases *) |
992 | 149 |
(* ********************************************************************** *) |
11317 | 150 |
Goal "Ord(a) ==> (\\<Union>b<a++a. C(b)) = (\\<Union>b<a. C(b) Un C(a++b))"; |
4091 | 151 |
by (fast_tac (claset() addSIs [equalityI] addIs [ltI] |
1041 | 152 |
addSDs [lt_oadd_disj] |
153 |
addSEs [lt_oadd1, oadd_lt_mono2]) 1); |
|
3731 | 154 |
qed "UN_oadd"; |
992 | 155 |
|
156 |
||
157 |
(* ********************************************************************** *) |
|
11317 | 158 |
(* Case 1 \\<in> lemmas *) |
992 | 159 |
(* ********************************************************************** *) |
160 |
||
11317 | 161 |
Goalw [vv1_def] "vv1(f,m,b) \\<subseteq> f`b"; |
1450 | 162 |
by (rtac (LetI RS LetI) 1); |
4091 | 163 |
by (simp_tac (simpset() addsimps [domain_uu_subset]) 1); |
3731 | 164 |
qed "vv1_subset"; |
992 | 165 |
|
166 |
(* ********************************************************************** *) |
|
11317 | 167 |
(* Case 1 \\<in> Union of images is the whole "y" *) |
992 | 168 |
(* ********************************************************************** *) |
5068 | 169 |
Goalw [gg1_def] |
11317 | 170 |
"!! a f y. [| Ord(a); m \\<in> nat |] ==> \ |
171 |
\ (\\<Union>b<a++a. gg1(f,a,m)`b) = (\\<Union>b<a. f`b)"; |
|
1041 | 172 |
by (asm_simp_tac |
4091 | 173 |
(simpset() addsimps [UN_oadd, lt_oadd1, |
1461 | 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); |
|
3731 | 177 |
qed "UN_gg1_eq"; |
1041 | 178 |
|
5068 | 179 |
Goal "domain(gg1(f,a,m)) = a++a"; |
4091 | 180 |
by (simp_tac (simpset() addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1); |
3731 | 181 |
qed "domain_gg1"; |
992 | 182 |
|
183 |
(* ********************************************************************** *) |
|
1461 | 184 |
(* every value of defined function is less than or equipollent to m *) |
992 | 185 |
(* ********************************************************************** *) |
5137 | 186 |
Goal "[| P(a, b); Ord(a); Ord(b); \ |
11317 | 187 |
\ Least_a = (LEAST a. \\<exists>x. Ord(x) & P(a, x)) |] \ |
1461 | 188 |
\ ==> P(Least_a, LEAST b. P(Least_a, b))"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
189 |
by (etac ssubst 1); |
992 | 190 |
by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1); |
4091 | 191 |
by (REPEAT (fast_tac (claset() addSEs [LeastI]) 1)); |
3731 | 192 |
qed "nested_LeastI"; |
992 | 193 |
|
8551 | 194 |
bind_thm ("nested_Least_instance", |
195 |
inst "P" |
|
11317 | 196 |
"%g d. domain(uu(f,b,g,d)) \\<noteq> 0 & domain(uu(f,b,g,d)) lepoll m" |
8551 | 197 |
nested_LeastI); |
992 | 198 |
|
5068 | 199 |
Goalw [gg1_def] |
11317 | 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 & \ |
|
1461 | 203 |
\ domain(uu(f,b,g,d)) lepoll m); \ |
11317 | 204 |
\ \\<forall>b<a. f`b lepoll succ(m); b<a++a \ |
1461 | 205 |
\ |] ==> gg1(f,a,m)`b lepoll m"; |
2469 | 206 |
by (Asm_simp_tac 1); |
4091 | 207 |
by (safe_tac (claset() addSEs [lt_oadd_odiff_cases])); |
11317 | 208 |
(*Case b<a \\<in> show vv1(f,m,b) lepoll m *) |
5137 | 209 |
by (asm_simp_tac (simpset() addsimps [vv1_def, Let_def]) 1); |
4091 | 210 |
by (fast_tac (claset() addIs [nested_Least_instance RS conjunct2] |
1461 | 211 |
addSEs [lt_Ord] |
212 |
addSIs [empty_lepollI]) 1); |
|
11317 | 213 |
(*Case a le b \\<in> show ww1(f,m,b--a) lepoll m *) |
4091 | 214 |
by (asm_simp_tac (simpset() addsimps [ww1_def]) 1); |
1041 | 215 |
by (excluded_middle_tac "f`(b--a) = 0" 1); |
4091 | 216 |
by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
217 |
by (rtac Diff_lepoll 1); |
3731 | 218 |
by (Blast_tac 1); |
1041 | 219 |
by (rtac vv1_subset 1); |
220 |
by (dtac (ospec RS mp) 1); |
|
6153 | 221 |
by (REPEAT (eresolve_tac [asm_rl, oexE, conjE] 1)); |
4091 | 222 |
by (asm_simp_tac (simpset() |
1461 | 223 |
addsimps [vv1_def, Let_def, lt_Ord, |
224 |
nested_Least_instance RS conjunct1]) 1); |
|
3731 | 225 |
qed "gg1_lepoll_m"; |
992 | 226 |
|
227 |
(* ********************************************************************** *) |
|
11317 | 228 |
(* Case 2 \\<in> lemmas *) |
992 | 229 |
(* ********************************************************************** *) |
230 |
||
231 |
(* ********************************************************************** *) |
|
11317 | 232 |
(* Case 2 \\<in> vv2_subset *) |
992 | 233 |
(* ********************************************************************** *) |
234 |
||
11317 | 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"; |
|
4091 | 238 |
by (fast_tac (claset() addSIs [not_emptyI] |
1461 | 239 |
addSDs [SigmaI RSN (2, subsetD)] |
240 |
addSEs [not_emptyE]) 1); |
|
3731 | 241 |
qed "ex_d_uu_not_empty"; |
992 | 242 |
|
11317 | 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"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
246 |
by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1)); |
4091 | 247 |
by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1); |
3731 | 248 |
qed "uu_not_empty"; |
992 | 249 |
|
11317 | 250 |
Goal "[| r \\<subseteq> A*B; r\\<noteq>0 |] ==> domain(r)\\<noteq>0"; |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5315
diff
changeset
|
251 |
by (Blast_tac 1); |
3731 | 252 |
qed "not_empty_rel_imp_domain"; |
992 | 253 |
|
11317 | 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"; |
|
992 | 257 |
by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1 |
1461 | 258 |
THEN REPEAT (assume_tac 1)); |
992 | 259 |
by (resolve_tac [Least_le RS lt_trans1] 1 |
1461 | 260 |
THEN (REPEAT (ares_tac [lt_Ord] 1))); |
3731 | 261 |
qed "Least_uu_not_empty_lt_a"; |
992 | 262 |
|
11317 | 263 |
Goal "[| B \\<subseteq> A; a\\<notin>B |] ==> B \\<subseteq> A-{a}"; |
3731 | 264 |
by (Blast_tac 1); |
265 |
qed "subset_Diff_sing"; |
|
992 | 266 |
|
1041 | 267 |
(*Could this be proved more directly?*) |
11317 | 268 |
Goal "[| A lepoll m; m lepoll B; B \\<subseteq> A; m \\<in> nat |] ==> A=B"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
269 |
by (etac natE 1); |
4091 | 270 |
by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [equalityI]) 1); |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5315
diff
changeset
|
271 |
by (safe_tac (claset() addSIs [equalityI])); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5315
diff
changeset
|
272 |
by (rtac ccontr 1); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5315
diff
changeset
|
273 |
by (etac (subset_Diff_sing RS subset_imp_lepoll |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5315
diff
changeset
|
274 |
RSN (2, Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5315
diff
changeset
|
275 |
succ_lepoll_natE) 1 |
1461 | 276 |
THEN REPEAT (assume_tac 1)); |
3731 | 277 |
qed "supset_lepoll_imp_eq"; |
992 | 278 |
|
11317 | 279 |
Goal "[| \\<forall>g<a. \\<forall>d<a. domain(uu(f, b, g, d))\\<noteq>0 --> \ |
1461 | 280 |
\ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
11317 | 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"; |
|
1071 | 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); |
|
992 | 288 |
by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS |
1461 | 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); |
|
1071 | 292 |
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1); |
12667 | 293 |
by (REPEAT_FIRST assume_tac); |
5137 | 294 |
by (REPEAT (fast_tac (claset() addSIs [domain_uu_subset]) 1)); |
3731 | 295 |
qed "uu_Least_is_fun"; |
992 | 296 |
|
5068 | 297 |
Goalw [vv2_def] |
11317 | 298 |
"!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f, b, g, d))\\<noteq>0 --> \ |
1461 | 299 |
\ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
11317 | 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"; |
|
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
5068
diff
changeset
|
303 |
by (split_tac [split_if] 1); |
3731 | 304 |
by Safe_tac; |
2493 | 305 |
by (etac (uu_Least_is_fun RS apply_type) 1); |
4091 | 306 |
by (REPEAT_SOME (fast_tac (claset() addSIs [not_emptyI, singleton_subsetI]))); |
3731 | 307 |
qed "vv2_subset"; |
992 | 308 |
|
309 |
(* ********************************************************************** *) |
|
11317 | 310 |
(* Case 2 \\<in> Union of images is the whole "y" *) |
992 | 311 |
(* ********************************************************************** *) |
5068 | 312 |
Goalw [gg2_def] |
11317 | 313 |
"!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 --> \ |
1461 | 314 |
\ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
11317 | 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"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
318 |
by (dtac sym 1); |
1041 | 319 |
by (asm_simp_tac |
4091 | 320 |
(simpset() addsimps [UN_oadd, lt_oadd1, |
1461 | 321 |
oadd_le_self RS le_imp_not_lt, lt_Ord, |
322 |
odiff_oadd_inverse, ww2_def, |
|
323 |
vv2_subset RS Diff_partition]) 1); |
|
3731 | 324 |
qed "UN_gg2_eq"; |
1041 | 325 |
|
5068 | 326 |
Goal "domain(gg2(f,a,b,s)) = a++a"; |
4091 | 327 |
by (simp_tac (simpset() addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1); |
3731 | 328 |
qed "domain_gg2"; |
992 | 329 |
|
330 |
(* ********************************************************************** *) |
|
1461 | 331 |
(* every value of defined function is less than or equipollent to m *) |
992 | 332 |
(* ********************************************************************** *) |
333 |
||
11317 | 334 |
Goalw [vv2_def] "[| m \\<in> nat; m\\<noteq>0 |] ==> vv2(f,b,g,s) lepoll m"; |
5137 | 335 |
by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 1); |
4091 | 336 |
by (fast_tac (claset() |
1461 | 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); |
|
3731 | 341 |
qed "vv2_lepoll"; |
992 | 342 |
|
5068 | 343 |
Goalw [ww2_def] |
11317 | 344 |
"[| \\<forall>b<a. f`b lepoll succ(m); g<a; m \\<in> nat; vv2(f,b,g,d) \\<subseteq> f`g |] \ |
5315 | 345 |
\ ==> ww2(f,b,g,d) lepoll m"; |
1041 | 346 |
by (excluded_middle_tac "f`g = 0" 1); |
4091 | 347 |
by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
348 |
by (dtac ospec 1 THEN (assume_tac 1)); |
5137 | 349 |
by (rtac Diff_lepoll 1 THEN (TRYALL assume_tac)); |
350 |
by (asm_simp_tac (simpset() addsimps [vv2_def, not_emptyI]) 1); |
|
3731 | 351 |
qed "ww2_lepoll"; |
1041 | 352 |
|
5068 | 353 |
Goalw [gg2_def] |
11317 | 354 |
"!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 --> \ |
1461 | 355 |
\ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
11317 | 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 \ |
|
1041 | 358 |
\ |] ==> gg2(f,a,b,s) ` g lepoll m"; |
2469 | 359 |
by (Asm_simp_tac 1); |
4091 | 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); |
|
3731 | 363 |
qed "gg2_lepoll_m"; |
992 | 364 |
|
365 |
(* ********************************************************************** *) |
|
1461 | 366 |
(* lemma ii *) |
992 | 367 |
(* ********************************************************************** *) |
11317 | 368 |
Goalw [NN_def] "[| succ(m) \\<in> NN(y); y*y \\<subseteq> y; m \\<in> nat; m\\<noteq>0 |] ==> m \\<in> NN(y)"; |
992 | 369 |
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1)); |
370 |
by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1 |
|
1041 | 371 |
THEN (assume_tac 1)); |
992 | 372 |
(* case 1 *) |
4091 | 373 |
by (asm_full_simp_tac (simpset() addsimps [lesspoll_succ_iff]) 1); |
1041 | 374 |
by (res_inst_tac [("x","a++a")] exI 1); |
4091 | 375 |
by (fast_tac (claset() addSIs [Ord_oadd, domain_gg1, UN_gg1_eq, |
1461 | 376 |
gg1_lepoll_m]) 1); |
992 | 377 |
(* case 2 *) |
378 |
by (REPEAT (eresolve_tac [oexE, conjE] 1)); |
|
1041 | 379 |
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
|
380 |
by (rtac CollectI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
381 |
by (etac succ_natD 1); |
992 | 382 |
by (res_inst_tac [("x","a++a")] exI 1); |
1041 | 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.*) |
|
4091 | 386 |
by (asm_simp_tac (simpset() addsimps |
1461 | 387 |
[Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1); |
3731 | 388 |
qed "lemma_ii"; |
992 | 389 |
|
390 |
||
391 |
(* ********************************************************************** *) |
|
11317 | 392 |
(* lemma iv - p. 4 \\<in> *) |
393 |
(* For every set x there is a set y such that x Un (y * y) \\<subseteq> y *) |
|
992 | 394 |
(* ********************************************************************** *) |
395 |
||
11317 | 396 |
(* the quantifier \\<forall>looks inelegant but makes the proofs shorter *) |
992 | 397 |
(* (used only in the following two lemmas) *) |
398 |
||
11317 | 399 |
Goal "\\<forall>n \\<in> nat. rec(n, x, %k r. r Un r*r) \\<subseteq> \ |
992 | 400 |
\ rec(succ(n), x, %k r. r Un r*r)"; |
4091 | 401 |
by (fast_tac (claset() addIs [rec_succ RS ssubst]) 1); |
3731 | 402 |
qed "z_n_subset_z_succ_n"; |
992 | 403 |
|
11317 | 404 |
Goal "[| \\<forall>n \\<in> nat. f(n)<=f(succ(n)); n le m; n \\<in> nat; m \\<in> nat |] \ |
5315 | 405 |
\ ==> f(n)<=f(m)"; |
2469 | 406 |
by (eres_inst_tac [("P","n le m")] rev_mp 1); |
11317 | 407 |
by (res_inst_tac [("P","%z. n le z --> f(n) \\<subseteq> f(z)")] nat_induct 1); |
2469 | 408 |
by (REPEAT (fast_tac le_cs 1)); |
3731 | 409 |
qed "le_subsets"; |
992 | 410 |
|
11317 | 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)"; |
|
992 | 413 |
by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1 |
1041 | 414 |
THEN (TRYALL assume_tac)); |
992 | 415 |
by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1 |
1041 | 416 |
THEN (assume_tac 1)); |
3731 | 417 |
qed "le_imp_rec_subset"; |
992 | 418 |
|
11317 | 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); |
|
4152 | 421 |
by Safe_tac; |
2493 | 422 |
by (rtac (nat_0I RS UN_I) 1); |
2469 | 423 |
by (Asm_simp_tac 1); |
992 | 424 |
by (res_inst_tac [("a","succ(n Un na)")] UN_I 1); |
1041 | 425 |
by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (assume_tac 1)); |
992 | 426 |
by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD] |
1461 | 427 |
addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type] |
4091 | 428 |
addSEs [nat_into_Ord] addss (simpset())) 1); |
3731 | 429 |
qed "lemma_iv"; |
992 | 430 |
|
431 |
(* ********************************************************************** *) |
|
11317 | 432 |
(* Rubin & Rubin wrote \\<in> *) |
433 |
(* "It follows from (ii) and mathematical induction that if y*y \\<subseteq> y then *) |
|
1461 | 434 |
(* y can be well-ordered" *) |
992 | 435 |
|
11317 | 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 *) |
|
992 | 440 |
(* ********************************************************************** *) |
441 |
||
442 |
(* ********************************************************************** *) |
|
11317 | 443 |
(* WO6 ==> NN(y) \\<noteq> 0 *) |
992 | 444 |
(* ********************************************************************** *) |
445 |
||
11317 | 446 |
Goalw [WO6_def, NN_def] "WO6 ==> NN(y) \\<noteq> 0"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
447 |
by (fast_tac ZF_cs 1); (*SLOW if current claset is used*) |
3731 | 448 |
qed "WO6_imp_NN_not_empty"; |
992 | 449 |
|
450 |
(* ********************************************************************** *) |
|
11317 | 451 |
(* 1 \\<in> NN(y) ==> y can be well-ordered *) |
992 | 452 |
(* ********************************************************************** *) |
453 |
||
11317 | 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}"; |
|
4091 | 456 |
by (fast_tac (claset() addSEs [lepoll_1_is_sing]) 1); |
992 | 457 |
val lemma1 = result(); |
458 |
||
11317 | 459 |
Goal "[| (\\<Union>b<a. f`b)=y; x \\<in> y; \\<forall>b<a. f`b lepoll 1; Ord(a) |] \ |
5315 | 460 |
\ ==> f` (LEAST i. f`i = {x}) = {x}"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
461 |
by (dtac lemma1 1 THEN REPEAT (assume_tac 1)); |
4091 | 462 |
by (fast_tac (claset() addSEs [lt_Ord] addIs [LeastI]) 1); |
992 | 463 |
val lemma2 = result(); |
464 |
||
11317 | 465 |
Goalw [NN_def] "1 \\<in> NN(y) ==> \\<exists>a f. Ord(a) & f \\<in> inj(y, a)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
466 |
by (etac CollectE 1); |
992 | 467 |
by (REPEAT (eresolve_tac [exE, conjE] 1)); |
468 |
by (res_inst_tac [("x","a")] exI 1); |
|
11317 | 469 |
by (res_inst_tac [("x","\\<lambda>x \\<in> y. LEAST i. f`i = {x}")] exI 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
470 |
by (rtac conjI 1 THEN (assume_tac 1)); |
11317 | 471 |
by (res_inst_tac [("d","%i. THE x. x \\<in> f`i")] lam_injective 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
472 |
by (dtac lemma1 1 THEN REPEAT (assume_tac 1)); |
4091 | 473 |
by (fast_tac (claset() addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1); |
1041 | 474 |
by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1)); |
5505 | 475 |
by (Blast_tac 1); |
3731 | 476 |
qed "NN_imp_ex_inj"; |
992 | 477 |
|
11317 | 478 |
Goal "[| y*y \\<subseteq> y; 1 \\<in> NN(y) |] ==> \\<exists>r. well_ord(y, r)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
479 |
by (dtac NN_imp_ex_inj 1); |
4091 | 480 |
by (fast_tac (claset() addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1); |
3731 | 481 |
qed "y_well_ord"; |
992 | 482 |
|
483 |
(* ********************************************************************** *) |
|
11317 | 484 |
(* reverse induction which lets us infer that 1 \\<in> NN(y) *) |
992 | 485 |
(* ********************************************************************** *) |
486 |
||
487 |
val [prem1, prem2] = goal thy |
|
11317 | 488 |
"[| n \\<in> nat; !!m. [| m \\<in> nat; m\\<noteq>0; P(succ(m)) |] ==> P(m) |] \ |
489 |
\ ==> n\\<noteq>0 --> P(n) --> P(1)"; |
|
6070 | 490 |
by (rtac (prem1 RS nat_induct) 1); |
3731 | 491 |
by (Blast_tac 1); |
992 | 492 |
by (excluded_middle_tac "x=0" 1); |
3731 | 493 |
by (Blast_tac 2); |
4091 | 494 |
by (fast_tac (claset() addSIs [prem2]) 1); |
3731 | 495 |
qed "rev_induct_lemma"; |
992 | 496 |
|
5315 | 497 |
val prems = |
11317 | 498 |
Goal "[| P(n); n \\<in> nat; n\\<noteq>0; \ |
499 |
\ !!m. [| m \\<in> nat; m\\<noteq>0; P(succ(m)) |] ==> P(m) |] \ |
|
5315 | 500 |
\ ==> P(1)"; |
992 | 501 |
by (resolve_tac [rev_induct_lemma RS impE] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
502 |
by (etac impE 4 THEN (assume_tac 5)); |
992 | 503 |
by (REPEAT (ares_tac prems 1)); |
3731 | 504 |
qed "rev_induct"; |
992 | 505 |
|
11317 | 506 |
Goalw [NN_def] "n \\<in> NN(y) ==> n \\<in> nat"; |
1057 | 507 |
by (etac CollectD1 1); |
3731 | 508 |
qed "NN_into_nat"; |
992 | 509 |
|
11317 | 510 |
Goal "[| n \\<in> NN(y); y*y \\<subseteq> y; n\\<noteq>0 |] ==> 1 \\<in> NN(y)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
511 |
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
|
512 |
by (rtac lemma_ii 1 THEN REPEAT (assume_tac 1)); |
992 | 513 |
val lemma3 = result(); |
514 |
||
515 |
(* ********************************************************************** *) |
|
1461 | 516 |
(* Main theorem "WO6 ==> WO1" *) |
992 | 517 |
(* ********************************************************************** *) |
518 |
||
519 |
(* another helpful lemma *) |
|
11317 | 520 |
Goalw [NN_def] "0 \\<in> NN(y) ==> y=0"; |
4091 | 521 |
by (fast_tac (claset() addSIs [equalityI] |
5315 | 522 |
addSDs [lepoll_0_is_0] addEs [subst]) 1); |
3731 | 523 |
qed "NN_y_0"; |
992 | 524 |
|
5137 | 525 |
Goalw [WO1_def] "WO6 ==> WO1"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
526 |
by (rtac allI 1); |
992 | 527 |
by (excluded_middle_tac "A=0" 1); |
4091 | 528 |
by (fast_tac (claset() addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2); |
992 | 529 |
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
|
530 |
by (etac exE 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1071
diff
changeset
|
531 |
by (dtac WO6_imp_NN_not_empty 1); |
992 | 532 |
by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1); |
533 |
by (eres_inst_tac [("A","NN(y)")] not_emptyE 1); |
|
7499 | 534 |
by (ftac y_well_ord 1); |
4091 | 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); |
|
992 | 537 |
qed "WO6_imp_WO1"; |
538 |