author | paulson |
Tue, 07 Jan 1997 12:42:48 +0100 | |
changeset 2483 | 95c2f9c0930a |
parent 2469 | b50b8c0eec01 |
child 2496 | 40efb87985b5 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/AC16_WO4.ML |
1200 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1200 | 4 |
|
5 |
The proof of AC16(n, k) ==> WO4(n-k) |
|
6 |
*) |
|
1196 | 7 |
|
8 |
open AC16_WO4; |
|
9 |
||
10 |
(* ********************************************************************** *) |
|
1461 | 11 |
(* The case of finite set *) |
1196 | 12 |
(* ********************************************************************** *) |
13 |
||
14 |
goalw thy [Finite_def] "!!A. [| Finite(A); 0<m; m:nat |] ==> \ |
|
1461 | 15 |
\ EX a f. Ord(a) & domain(f) = a & \ |
16 |
\ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
17 |
by (etac bexE 1); |
1196 | 18 |
by (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
19 |
by (etac exE 1); |
1196 | 20 |
by (res_inst_tac [("x","n")] exI 1); |
21 |
by (res_inst_tac [("x","lam i:n. {f`i}")] exI 1); |
|
2469 | 22 |
by (Asm_full_simp_tac 1); |
1196 | 23 |
by (rewrite_goals_tac [bij_def, surj_def]); |
2469 | 24 |
by (fast_tac (!claset addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun, |
1461 | 25 |
equalityI, singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
26 |
nat_1_lepoll_iff RS iffD2] |
|
1932
cc9f1ba8f29a
Tidying: removing redundant args in classical reasoner calls
paulson
parents:
1924
diff
changeset
|
27 |
addSEs [apply_type, ltE]) 1); |
1196 | 28 |
val lemma1 = result(); |
29 |
||
30 |
(* ********************************************************************** *) |
|
1461 | 31 |
(* The case of infinite set *) |
1196 | 32 |
(* ********************************************************************** *) |
33 |
||
2167 | 34 |
(* well_ord(x,r) ==> well_ord({{y,z}. y:x}, Something(x,z)) **) |
35 |
val well_ord_paired = standard (paired_bij RS bij_is_inj RS well_ord_rvimage); |
|
1196 | 36 |
|
37 |
goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C"; |
|
2469 | 38 |
by (fast_tac (!claset addEs [notE, lepoll_trans]) 1); |
1196 | 39 |
val lepoll_trans1 = result(); |
40 |
||
41 |
goalw thy [lepoll_def] |
|
1461 | 42 |
"!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)"; |
2469 | 43 |
by (fast_tac (!claset addSEs [well_ord_rvimage]) 1); |
1196 | 44 |
val well_ord_lepoll = result(); |
45 |
||
46 |
goal thy "!!X. [| well_ord(X,R); well_ord(Y,S) \ |
|
1461 | 47 |
\ |] ==> EX T. well_ord(X Un Y, T)"; |
1196 | 48 |
by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS well_ord_lepoll)] 1); |
49 |
by (assume_tac 1); |
|
50 |
val well_ord_Un = result(); |
|
51 |
||
52 |
(* ********************************************************************** *) |
|
1461 | 53 |
(* There exists a well ordered set y such that ... *) |
1196 | 54 |
(* ********************************************************************** *) |
55 |
||
56 |
goal thy "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)"; |
|
57 |
by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1); |
|
58 |
by (resolve_tac [Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS |
|
1461 | 59 |
well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); |
2469 | 60 |
by (fast_tac (!claset addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, |
1461 | 61 |
equals0I, HartogI RSN (2, lepoll_trans1), |
62 |
subset_imp_lepoll RS (paired_eqpoll RS eqpoll_sym RS |
|
63 |
eqpoll_imp_lepoll RSN (2, lepoll_trans))] |
|
64 |
addSEs [RepFunE, nat_not_Finite RS notE] addEs [mem_asym] |
|
65 |
addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite, |
|
66 |
paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
|
67 |
RS lepoll_Finite]) 1); |
|
1196 | 68 |
val lemma2 = result(); |
69 |
||
70 |
val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)"; |
|
2469 | 71 |
by (fast_tac (!claset |
1461 | 72 |
addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1); |
1196 | 73 |
val infinite_Un = result(); |
74 |
||
75 |
(* ********************************************************************** *) |
|
1461 | 76 |
(* There is a v : s_u such that k lepoll x Int y (in our case succ(k)) *) |
77 |
(* The idea of the proof is the following : *) |
|
78 |
(* Suppose not, i.e. every element of s_u has exactly k-1 elements of y *) |
|
79 |
(* Thence y is less than or equipollent to {v:Pow(x). v eqpoll n#-k} *) |
|
80 |
(* We have obtained this result in two steps : *) |
|
81 |
(* 1. y is less than or equipollent to {v:s_u. a <= v} *) |
|
82 |
(* where a is certain k-2 element subset of y *) |
|
83 |
(* 2. {v:s_u. a <= v} is less than or equipollent *) |
|
84 |
(* to {v:Pow(x). v eqpoll n-k} *) |
|
1196 | 85 |
(* ********************************************************************** *) |
86 |
||
1710 | 87 |
(*Proof simplified by LCP*) |
1196 | 88 |
goal thy "!!A. [| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \ |
1461 | 89 |
\ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)"; |
1196 | 90 |
by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); |
1710 | 91 |
by (ALLGOALS |
92 |
(asm_simp_tac |
|
2469 | 93 |
(!simpset addsimps [inj_is_fun RS apply_type, left_inverse] |
94 |
setloop (split_tac [expand_if] ORELSE' Step_tac)))); |
|
1196 | 95 |
val succ_not_lepoll_lemma = result(); |
96 |
||
97 |
goalw thy [lepoll_def, eqpoll_def, bij_def, surj_def] |
|
1461 | 98 |
"!!A. [| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; |
2469 | 99 |
by (fast_tac (!claset addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |
1196 | 100 |
val succ_not_lepoll_imp_eqpoll = result(); |
101 |
||
102 |
val [prem] = goalw thy [s_u_def] |
|
1461 | 103 |
"(ALL v:s_u(u, t_n, k, y). k eqpoll v Int y ==> False) \ |
104 |
\ ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y"; |
|
1196 | 105 |
by (excluded_middle_tac "?P" 1 THEN (assume_tac 2)); |
106 |
by (resolve_tac [prem RS FalseE] 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
107 |
by (rtac ballI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
108 |
by (etac CollectE 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
109 |
by (etac conjE 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
110 |
by (etac swap 1); |
2469 | 111 |
by (fast_tac (!claset addSEs [succ_not_lepoll_imp_eqpoll]) 1); |
1196 | 112 |
val suppose_not = result(); |
113 |
||
114 |
(* ********************************************************************** *) |
|
1461 | 115 |
(* There is a k-2 element subset of y *) |
1196 | 116 |
(* ********************************************************************** *) |
117 |
||
118 |
goalw thy [lepoll_def, eqpoll_def] |
|
1461 | 119 |
"!!X. [| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y"; |
1196 | 120 |
by (fast_tac (FOL_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)] |
1461 | 121 |
addSIs [subset_refl] |
122 |
addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1); |
|
1196 | 123 |
val nat_lepoll_imp_ex_eqpoll_n = result(); |
124 |
||
125 |
val ordertype_eqpoll = |
|
1461 | 126 |
ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2)); |
1196 | 127 |
|
128 |
goal thy "!!y. [| well_ord(y,R); ~Finite(y); n:nat \ |
|
1461 | 129 |
\ |] ==> EX z. z<=y & n eqpoll z"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
130 |
by (etac nat_lepoll_imp_ex_eqpoll_n 1); |
1196 | 131 |
by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
1461 | 132 |
RSN (2, lepoll_trans)] 1 THEN (assume_tac 2)); |
2469 | 133 |
by (fast_tac (!claset addSIs [nat_le_infinite_Ord RS le_imp_lepoll] |
1461 | 134 |
addSEs [Ord_ordertype, ordertype_eqpoll RS eqpoll_imp_lepoll |
135 |
RS lepoll_infinite]) 1); |
|
1196 | 136 |
val ex_subset_eqpoll_n = result(); |
137 |
||
138 |
goalw thy [lesspoll_def] "!!n. n: nat ==> n lesspoll nat"; |
|
2469 | 139 |
by (fast_tac (!claset addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll, |
1461 | 140 |
eqpoll_sym RS eqpoll_imp_lepoll] |
141 |
addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI |
|
142 |
RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1); |
|
1196 | 143 |
val n_lesspoll_nat = result(); |
144 |
||
145 |
goal thy "!!y. [| well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; k: nat |] \ |
|
1461 | 146 |
\ ==> y - a eqpoll y"; |
1196 | 147 |
by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll] |
1461 | 148 |
addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans, |
149 |
Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord |
|
150 |
RS le_imp_lepoll] |
|
151 |
addSEs [well_ord_cardinal_eqpoll, |
|
152 |
well_ord_cardinal_eqpoll RS eqpoll_sym, |
|
153 |
eqpoll_sym RS eqpoll_imp_lepoll, |
|
154 |
n_lesspoll_nat RS lesspoll_lepoll_lesspoll, |
|
155 |
well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
|
156 |
RS lepoll_infinite]) 1); |
|
1196 | 157 |
val Diff_Finite_eqpoll = result(); |
158 |
||
159 |
goal thy "!!x. [| a<=y; b:y-a; u:x |] ==> cons(b, cons(u, a)) : Pow(x Un y)"; |
|
2469 | 160 |
by (Fast_tac 1); |
1196 | 161 |
val cons_cons_subset = result(); |
162 |
||
163 |
goal thy "!!x. [| a eqpoll k; a<=y; b:y-a; u:x; x Int y = 0 \ |
|
1461 | 164 |
\ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))"; |
2469 | 165 |
by (fast_tac (!claset addSIs [cons_eqpoll_succ] addEs [equals0D]) 1); |
1196 | 166 |
val cons_cons_eqpoll = result(); |
167 |
||
168 |
goalw thy [s_u_def] "s_u(u, t_n, k, y) <= t_n"; |
|
2469 | 169 |
by (Fast_tac 1); |
1196 | 170 |
val s_u_subset = result(); |
171 |
||
172 |
goalw thy [s_u_def, succ_def] |
|
1461 | 173 |
"!!w. [| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; k eqpoll a \ |
174 |
\ |] ==> w: s_u(u, t_n, succ(k), y)"; |
|
2469 | 175 |
by (fast_tac (!claset addDs [eqpoll_imp_lepoll RS cons_lepoll_cong] |
1461 | 176 |
addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); |
1196 | 177 |
val s_uI = result(); |
178 |
||
179 |
goalw thy [s_u_def] "!!v. v : s_u(u, t_n, k, y) ==> u : v"; |
|
2469 | 180 |
by (Fast_tac 1); |
1196 | 181 |
val in_s_u_imp_u_in = result(); |
182 |
||
183 |
goal thy |
|
1461 | 184 |
"!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ |
185 |
\ EX! w. w:t_n & z <= w; \ |
|
186 |
\ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0 |] \ |
|
187 |
\ ==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
188 |
by (etac ballE 1); |
1196 | 189 |
by (fast_tac (FOL_cs addSIs [CollectI, cons_cons_subset, |
2469 | 190 |
eqpoll_sym RS cons_cons_eqpoll]) 2); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
191 |
by (etac ex1E 1); |
1196 | 192 |
by (res_inst_tac [("a","w")] ex1I 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
193 |
by (rtac conjI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
194 |
by (rtac CollectI 1); |
1196 | 195 |
by (fast_tac (FOL_cs addSEs [s_uI]) 1); |
2469 | 196 |
by (Fast_tac 1); |
197 |
by (Fast_tac 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
198 |
by (etac allE 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
199 |
by (etac impE 1); |
1196 | 200 |
by (assume_tac 2); |
2469 | 201 |
by (fast_tac (!claset addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
1196 | 202 |
val ex1_superset_a = result(); |
203 |
||
204 |
goal thy |
|
1461 | 205 |
"!!A. [| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \ |
206 |
\ |] ==> A = cons(a, B)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
207 |
by (rtac equalityI 1); |
2469 | 208 |
by (Fast_tac 2); |
1196 | 209 |
by (resolve_tac [Diff_eq_0_iff RS iffD1] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
210 |
by (rtac equals0I 1); |
1196 | 211 |
by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1); |
212 |
by (dresolve_tac [eqpoll_sym RS cons_eqpoll_succ] 1); |
|
2469 | 213 |
by (Fast_tac 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
214 |
by (dtac cons_eqpoll_succ 1); |
2469 | 215 |
by (Fast_tac 1); |
216 |
by (fast_tac (!claset addSIs [nat_succI] |
|
1461 | 217 |
addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS |
218 |
(lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1); |
|
1196 | 219 |
val set_eq_cons = result(); |
220 |
||
221 |
goal thy |
|
1461 | 222 |
"!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ |
223 |
\ EX! w. w:t_n & z <= w; \ |
|
224 |
\ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \ |
|
225 |
\ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0; k:nat \ |
|
226 |
\ |] ==> (THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c) \ |
|
227 |
\ Int y = cons(b, a)"; |
|
1196 | 228 |
by (dresolve_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
229 |
by (rtac set_eq_cons 1); |
2469 | 230 |
by (REPEAT (Fast_tac 1)); |
1196 | 231 |
val the_eq_cons = result(); |
232 |
||
233 |
goal thy "!!a. [| cons(x,a) = cons(y,a); x~: a |] ==> x = y "; |
|
2469 | 234 |
by (fast_tac (!claset addSEs [equalityE]) 1); |
1196 | 235 |
val cons_eqE = result(); |
236 |
||
237 |
goal thy "!!A. A = B ==> A Int C = B Int C"; |
|
2469 | 238 |
by (Asm_simp_tac 1); |
1196 | 239 |
val eq_imp_Int_eq = result(); |
240 |
||
241 |
goal thy "!!a. [| a=b; a=c; b=d |] ==> c=d"; |
|
2469 | 242 |
by (Asm_full_simp_tac 1); |
1196 | 243 |
val msubst = result(); |
244 |
||
245 |
(* ********************************************************************** *) |
|
1461 | 246 |
(* 1. y is less than or equipollent to {v:s_u. a <= v} *) |
247 |
(* where a is certain k-2 element subset of y *) |
|
1196 | 248 |
(* ********************************************************************** *) |
249 |
||
250 |
goal thy |
|
1461 | 251 |
"!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ |
252 |
\ EX! w. w:t_n & z <= w; \ |
|
253 |
\ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \ |
|
254 |
\ well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; \ |
|
255 |
\ k:nat; u:x; x Int y = 0 |] \ |
|
256 |
\ ==> y lepoll {v:s_u(u, t_n, succ(k), y). a <= v}"; |
|
1196 | 257 |
by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS |
1461 | 258 |
eqpoll_imp_lepoll RS lepoll_trans] 1 |
259 |
THEN REPEAT (assume_tac 1)); |
|
1196 | 260 |
by (res_inst_tac [("f3","lam b:y-a. \ |
1461 | 261 |
\ THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c")] |
262 |
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
|
1196 | 263 |
by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
264 |
by (rtac CollectI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
265 |
by (rtac lam_type 1); |
1196 | 266 |
by (resolve_tac [ex1_superset_a RS theI RS conjunct1] 1 |
1461 | 267 |
THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
268 |
by (rtac ballI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
269 |
by (rtac ballI 1); |
1196 | 270 |
by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); |
271 |
by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
272 |
by (rtac impI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
273 |
by (rtac cons_eqE 1); |
2469 | 274 |
by (Fast_tac 2); |
1196 | 275 |
by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1); |
276 |
by (eresolve_tac [[asm_rl, the_eq_cons, the_eq_cons] MRS msubst] 1 |
|
1461 | 277 |
THEN REPEAT (assume_tac 1)); |
1196 | 278 |
val y_lepoll_subset_s_u = result(); |
279 |
||
280 |
(* ********************************************************************** *) |
|
1461 | 281 |
(* some arithmetic *) |
1196 | 282 |
(* ********************************************************************** *) |
283 |
||
284 |
goal thy |
|
1461 | 285 |
"!!k. [| k:nat; m:nat |] ==> \ |
286 |
\ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m"; |
|
1196 | 287 |
by (eres_inst_tac [("n","k")] nat_induct 1); |
2469 | 288 |
by (simp_tac (!simpset addsimps [add_0]) 1); |
289 |
by (fast_tac (!claset addIs [eqpoll_imp_lepoll RS |
|
1461 | 290 |
(Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1); |
1196 | 291 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
292 |
by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
|
2469 | 293 |
by (Fast_tac 1); |
1196 | 294 |
by (eres_inst_tac [("x","A - {xa}")] allE 1); |
295 |
by (eres_inst_tac [("x","B - {xa}")] allE 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
296 |
by (etac impE 1); |
2469 | 297 |
by (asm_full_simp_tac (!simpset addsimps [add_succ]) 1); |
298 |
by (fast_tac (!claset addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1); |
|
1196 | 299 |
by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2)); |
2469 | 300 |
by (fast_tac (!claset addSIs [equalityI]) 1); |
1196 | 301 |
val eqpoll_sum_imp_Diff_lepoll_lemma = result(); |
302 |
||
303 |
goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; \ |
|
1461 | 304 |
\ k:nat; m:nat |] \ |
305 |
\ ==> A-B lepoll m"; |
|
1196 | 306 |
by (dresolve_tac [add_succ RS ssubst] 1); |
307 |
by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_lepoll_lemma] 1 |
|
1461 | 308 |
THEN (REPEAT (assume_tac 1))); |
2469 | 309 |
by (Fast_tac 1); |
1196 | 310 |
val eqpoll_sum_imp_Diff_lepoll = result(); |
311 |
||
312 |
(* ********************************************************************** *) |
|
1461 | 313 |
(* similar properties for eqpoll *) |
1196 | 314 |
(* ********************************************************************** *) |
315 |
||
316 |
goal thy |
|
1461 | 317 |
"!!k. [| k:nat; m:nat |] ==> \ |
318 |
\ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m"; |
|
1196 | 319 |
by (eres_inst_tac [("n","k")] nat_induct 1); |
2469 | 320 |
by (fast_tac (!claset addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] |
321 |
addss (!simpset addsimps [add_0])) 1); |
|
1196 | 322 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
323 |
by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
|
2469 | 324 |
by (fast_tac (!claset addSEs [eqpoll_imp_lepoll]) 1); |
1196 | 325 |
by (eres_inst_tac [("x","A - {xa}")] allE 1); |
326 |
by (eres_inst_tac [("x","B - {xa}")] allE 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
327 |
by (etac impE 1); |
2469 | 328 |
by (fast_tac (!claset addSIs [Diff_sing_eqpoll, |
1461 | 329 |
eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym] |
2469 | 330 |
addss (!simpset addsimps [add_succ])) 1); |
1196 | 331 |
by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2)); |
2469 | 332 |
by (fast_tac (!claset addSIs [equalityI]) 1); |
1196 | 333 |
val eqpoll_sum_imp_Diff_eqpoll_lemma = result(); |
334 |
||
335 |
goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; \ |
|
1461 | 336 |
\ k:nat; m:nat |] \ |
337 |
\ ==> A-B eqpoll m"; |
|
1196 | 338 |
by (dresolve_tac [add_succ RS ssubst] 1); |
339 |
by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_eqpoll_lemma] 1 |
|
1461 | 340 |
THEN (REPEAT (assume_tac 1))); |
2469 | 341 |
by (Fast_tac 1); |
1196 | 342 |
val eqpoll_sum_imp_Diff_eqpoll = result(); |
343 |
||
344 |
(* ********************************************************************** *) |
|
1461 | 345 |
(* back to the second part *) |
1196 | 346 |
(* ********************************************************************** *) |
347 |
||
348 |
goal thy "!!w. [| x Int y = 0; w <= x Un y |] \ |
|
1461 | 349 |
\ ==> w Int (x - {u}) = w - cons(u, w Int y)"; |
2469 | 350 |
by (fast_tac (!claset addSIs [equalityI] addEs [equals0D]) 1); |
1196 | 351 |
val w_Int_eq_w_Diff = result(); |
352 |
||
353 |
goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \ |
|
1461 | 354 |
\ l eqpoll a; t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ |
355 |
\ m:nat; l:nat; x Int y = 0; u : x; \ |
|
356 |
\ ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y \ |
|
357 |
\ |] ==> w Int (x - {u}) eqpoll m"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
358 |
by (etac CollectE 1); |
1196 | 359 |
by (resolve_tac [w_Int_eq_w_Diff RS ssubst] 1 THEN (assume_tac 1)); |
2469 | 360 |
by (fast_tac (!claset addSDs [s_u_subset RS subsetD]) 1); |
361 |
by (fast_tac (!claset addEs [equals0D] addSDs [bspec] |
|
1461 | 362 |
addDs [s_u_subset RS subsetD] |
363 |
addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_u_imp_u_in] |
|
364 |
addSIs [nat_succI, eqpoll_sum_imp_Diff_eqpoll]) 1); |
|
1196 | 365 |
val w_Int_eqpoll_m = result(); |
366 |
||
367 |
goal thy "!!m. [| 0<m; x eqpoll m; m:nat |] ==> x ~= 0"; |
|
368 |
by (fast_tac (empty_cs |
|
1461 | 369 |
addSEs [mem_irrefl, ltE, eqpoll_succ_imp_not_empty, natE]) 1); |
1196 | 370 |
val eqpoll_m_not_empty = result(); |
371 |
||
372 |
goal thy |
|
1461 | 373 |
"!!z. [| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x \ |
374 |
\ |] ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}"; |
|
2469 | 375 |
by (fast_tac (!claset addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1); |
1196 | 376 |
val cons_cons_in = result(); |
377 |
||
378 |
(* ********************************************************************** *) |
|
1461 | 379 |
(* 2. {v:s_u. a <= v} is less than or equipollent *) |
380 |
(* to {v:Pow(x). v eqpoll n-k} *) |
|
1196 | 381 |
(* ********************************************************************** *) |
382 |
||
383 |
goal thy |
|
1461 | 384 |
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \ |
385 |
\ EX! w. w:t_n & z <= w; \ |
|
386 |
\ t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ |
|
387 |
\ 0<m; m:nat; l:nat; \ |
|
388 |
\ ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y; \ |
|
389 |
\ a <= y; l eqpoll a; x Int y = 0; u : x \ |
|
390 |
\ |] ==> {v:s_u(u, t_n, succ(l), y). a <= v} \ |
|
391 |
\ lepoll {v:Pow(x). v eqpoll m}"; |
|
1196 | 392 |
by (res_inst_tac [("f3","lam w:{v:s_u(u, t_n, succ(l), y). a <= v}. \ |
1461 | 393 |
\ w Int (x - {u})")] |
394 |
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
|
1196 | 395 |
by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
396 |
by (rtac CollectI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
397 |
by (rtac lam_type 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
398 |
by (rtac CollectI 1); |
2469 | 399 |
by (Fast_tac 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
400 |
by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1)); |
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
401 |
by (simp_tac (!simpset delsimps ball_simps) 1); |
1196 | 402 |
by (REPEAT (resolve_tac [ballI, impI] 1)); |
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
403 |
(** LEVEL 9 **) |
1196 | 404 |
by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1 |
1461 | 405 |
THEN REPEAT (assume_tac 1)); |
1196 | 406 |
by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); |
407 |
by (dresolve_tac [cons_cons_in RSN (2, bspec)] 1 THEN REPEAT (assume_tac 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
408 |
by (etac ex1_two_eq 1); |
2469 | 409 |
by (fast_tac (!claset addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
410 |
by (fast_tac (!claset addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
|
1196 | 411 |
val subset_s_u_lepoll_w = result(); |
412 |
||
413 |
goal thy "!!k. [| 0<k; k:nat |] ==> EX l:nat. k = succ(l)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
414 |
by (etac natE 1); |
1196 | 415 |
by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1); |
416 |
by (fast_tac (empty_cs addSIs [refl, bexI]) 1); |
|
417 |
val ex_eq_succ = result(); |
|
418 |
||
419 |
goal thy |
|
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
420 |
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
421 |
\ EX! w. w:t_n & z <= w; \ |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
422 |
\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
423 |
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
424 |
\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
425 |
\ |] ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
426 |
by (rtac suppose_not 1); |
1196 | 427 |
by (eresolve_tac [ex_eq_succ RS bexE] 1 THEN (assume_tac 1)); |
428 |
by (hyp_subst_tac 1); |
|
429 |
by (res_inst_tac [("n1","xa")] (ex_subset_eqpoll_n RS exE) 1 |
|
1461 | 430 |
THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
431 |
by (etac conjE 1); |
1196 | 432 |
by (forward_tac [[y_lepoll_subset_s_u, subset_s_u_lepoll_w] MRS lepoll_trans] 1 |
1461 | 433 |
THEN REPEAT (assume_tac 1)); |
1196 | 434 |
by (contr_tac 1); |
435 |
val exists_proper_in_s_u = result(); |
|
436 |
||
437 |
(* ********************************************************************** *) |
|
1461 | 438 |
(* LL can be well ordered *) |
1196 | 439 |
(* ********************************************************************** *) |
440 |
||
441 |
goal thy "{x:Pow(X). x lepoll 0} = {0}"; |
|
2469 | 442 |
by (fast_tac (!claset addSDs [lepoll_0_is_0] |
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1710
diff
changeset
|
443 |
addSIs [lepoll_refl, equalityI]) 1); |
1196 | 444 |
val subsets_lepoll_0_eq_unit = result(); |
445 |
||
446 |
goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \ |
|
1461 | 447 |
\ ==> EX S. well_ord({Y: Pow(X) . Y eqpoll succ(n)}, S)"; |
1196 | 448 |
by (resolve_tac [well_ord_infinite_subsets_eqpoll_X |
1461 | 449 |
RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1 |
1196 | 450 |
THEN (REPEAT (assume_tac 1))); |
2469 | 451 |
by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
1196 | 452 |
val well_ord_subsets_eqpoll_n = result(); |
453 |
||
454 |
goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ |
|
1461 | 455 |
\ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; |
2469 | 456 |
by (fast_tac (!claset addIs [le_refl, leI, |
1461 | 457 |
le_imp_lepoll, equalityI] |
458 |
addSDs [lepoll_succ_disj] |
|
459 |
addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
|
1196 | 460 |
val subsets_lepoll_succ = result(); |
461 |
||
462 |
goal thy "!!n. n:nat ==> \ |
|
1461 | 463 |
\ {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0"; |
2469 | 464 |
by (fast_tac (!claset addSEs [eqpoll_sym RS eqpoll_imp_lepoll |
1461 | 465 |
RS lepoll_trans RS succ_lepoll_natE] |
466 |
addSIs [equals0I]) 1); |
|
1196 | 467 |
val Int_empty = result(); |
468 |
||
469 |
(* ********************************************************************** *) |
|
1461 | 470 |
(* unit set is well-ordered by the empty relation *) |
1196 | 471 |
(* ********************************************************************** *) |
472 |
||
473 |
goalw thy [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def] |
|
1461 | 474 |
"tot_ord({a},0)"; |
2469 | 475 |
by (Simp_tac 1); |
1196 | 476 |
val tot_ord_unit = result(); |
477 |
||
478 |
goalw thy [wf_on_def, wf_def] "wf[{a}](0)"; |
|
2469 | 479 |
by (fast_tac (!claset addSIs [equalityI]) 1); |
1196 | 480 |
val wf_on_unit = result(); |
481 |
||
482 |
goalw thy [well_ord_def] "well_ord({a},0)"; |
|
2469 | 483 |
by (simp_tac (!simpset addsimps [tot_ord_unit, wf_on_unit]) 1); |
1196 | 484 |
val well_ord_unit = result(); |
485 |
||
486 |
(* ********************************************************************** *) |
|
1461 | 487 |
(* well_ord_subsets_lepoll_n *) |
1196 | 488 |
(* ********************************************************************** *) |
489 |
||
490 |
goal thy "!!y r. [| well_ord(y,r); ~Finite(y); n:nat |] ==> \ |
|
1461 | 491 |
\ EX R. well_ord({z:Pow(y). z lepoll n}, R)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
492 |
by (etac nat_induct 1); |
2469 | 493 |
by (fast_tac (!claset addSIs [well_ord_unit] |
494 |
addss (!simpset addsimps [subsets_lepoll_0_eq_unit])) 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
495 |
by (etac exE 1); |
1196 | 496 |
by (eresolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 |
1461 | 497 |
THEN REPEAT (assume_tac 1)); |
2469 | 498 |
by (asm_simp_tac (!simpset addsimps [subsets_lepoll_succ]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
499 |
by (dtac well_ord_radd 1 THEN (assume_tac 1)); |
1196 | 500 |
by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS |
1461 | 501 |
(eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
2469 | 502 |
by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
1196 | 503 |
val well_ord_subsets_lepoll_n = result(); |
504 |
||
505 |
goalw thy [LL_def, MM_def] |
|
1461 | 506 |
"!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \ |
507 |
\ ==> LL(t_n, k, y) <= {z:Pow(y). z lepoll n}"; |
|
2469 | 508 |
by (fast_tac (!claset addSEs [RepFunE] |
1461 | 509 |
addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll |
510 |
RSN (2, lepoll_trans))]) 1); |
|
1196 | 511 |
val LL_subset = result(); |
512 |
||
513 |
goal thy "!!x. [| t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
|
1461 | 514 |
\ well_ord(y, R); ~Finite(y); n:nat \ |
515 |
\ |] ==> EX S. well_ord(LL(t_n, k, y), S)"; |
|
1196 | 516 |
by (fast_tac (FOL_cs addIs [exI] |
1461 | 517 |
addSEs [LL_subset RSN (2, well_ord_subset)] |
518 |
addEs [well_ord_subsets_lepoll_n RS exE]) 1); |
|
1196 | 519 |
val well_ord_LL = result(); |
520 |
||
521 |
(* ********************************************************************** *) |
|
1461 | 522 |
(* every element of LL is a contained in exactly one element of MM *) |
1196 | 523 |
(* ********************************************************************** *) |
524 |
||
525 |
goalw thy [MM_def, LL_def] |
|
1461 | 526 |
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
527 |
\ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
|
528 |
\ v:LL(t_n, k, y) \ |
|
529 |
\ |] ==> EX! w. w:MM(t_n, k, y) & v<=w"; |
|
2469 | 530 |
by (step_tac (!claset addSEs [RepFunE]) 1); |
1196 | 531 |
by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1)); |
532 |
by (eres_inst_tac [("x","xa")] ballE 1); |
|
2469 | 533 |
by (fast_tac (!claset addSEs [eqpoll_sym]) 2); |
1196 | 534 |
by (res_inst_tac [("a","v")] ex1I 1); |
2469 | 535 |
by (Fast_tac 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
536 |
by (etac ex1E 1); |
1196 | 537 |
by (res_inst_tac [("x","v")] allE 1 THEN (assume_tac 1)); |
538 |
by (eres_inst_tac [("x","xb")] allE 1); |
|
2469 | 539 |
by (Fast_tac 1); |
1196 | 540 |
val unique_superset_in_MM = result(); |
541 |
||
542 |
(* ********************************************************************** *) |
|
1461 | 543 |
(* The function GG satisfies the conditions of WO4 *) |
1196 | 544 |
(* ********************************************************************** *) |
545 |
||
546 |
(* ********************************************************************** *) |
|
1461 | 547 |
(* The union of appropriate values is the whole x *) |
1196 | 548 |
(* ********************************************************************** *) |
549 |
||
550 |
goal thy |
|
1461 | 551 |
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ |
552 |
\ EX! w. w:t_n & z <= w; \ |
|
553 |
\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ |
|
554 |
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
|
555 |
\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
|
556 |
\ |] ==> EX w:MM(t_n, succ(k), y). u:w"; |
|
1196 | 557 |
by (eresolve_tac [exists_proper_in_s_u RS bexE] 1 |
1461 | 558 |
THEN REPEAT (assume_tac 1)); |
1196 | 559 |
by (rewrite_goals_tac [MM_def, s_u_def]); |
2469 | 560 |
by (Fast_tac 1); |
1196 | 561 |
val exists_in_MM = result(); |
562 |
||
563 |
goalw thy [LL_def] "!!w. w : MM(t_n, k, y) ==> w Int y : LL(t_n, k, y)"; |
|
2469 | 564 |
by (Fast_tac 1); |
1196 | 565 |
val Int_in_LL = result(); |
566 |
||
567 |
goalw thy [MM_def] "MM(t_n, k, y) <= t_n"; |
|
2469 | 568 |
by (Fast_tac 1); |
1196 | 569 |
val MM_subset = result(); |
570 |
||
571 |
goal thy |
|
1461 | 572 |
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ |
573 |
\ EX! w. w:t_n & z <= w; \ |
|
574 |
\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ |
|
575 |
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
|
576 |
\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
|
577 |
\ |] ==> EX w:LL(t_n, succ(k), y). u:GG(t_n, succ(k), y)`w"; |
|
1196 | 578 |
by (forward_tac [exists_in_MM] 1 THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
579 |
by (etac bexE 1); |
1196 | 580 |
by (res_inst_tac [("x","w Int y")] bexI 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
581 |
by (etac Int_in_LL 2); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
582 |
by (rewtac GG_def); |
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
583 |
by (asm_full_simp_tac (!simpset delsimps ball_simps addsimps [Int_in_LL]) 1); |
1196 | 584 |
by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1 |
1461 | 585 |
THEN (assume_tac 1)); |
2469 | 586 |
by (REPEAT (fast_tac (!claset addEs [equals0D] addSEs [Int_in_LL]) 1)); |
1196 | 587 |
val exists_in_LL = result(); |
588 |
||
589 |
goalw thy [LL_def] |
|
1461 | 590 |
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
591 |
\ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
|
592 |
\ v : LL(t_n, k, y) |] \ |
|
593 |
\ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y"; |
|
2469 | 594 |
by (fast_tac (!claset addSEs [Int_in_LL, |
1461 | 595 |
unique_superset_in_MM RS the_equality2 RS ssubst]) 1); |
1196 | 596 |
val in_LL_eq_Int = result(); |
597 |
||
598 |
goal thy |
|
1461 | 599 |
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
600 |
\ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
|
601 |
\ v : LL(t_n, k, y) |] \ |
|
602 |
\ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y"; |
|
2469 | 603 |
by (fast_tac (!claset addSDs [unique_superset_in_MM RS theI RS conjunct1 RS |
1461 | 604 |
(MM_subset RS subsetD)]) 1); |
1196 | 605 |
val the_in_MM_subset = result(); |
606 |
||
607 |
goalw thy [GG_def] |
|
1461 | 608 |
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
609 |
\ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
|
610 |
\ v : LL(t_n, k, y) |] \ |
|
611 |
\ ==> GG(t_n, k, y) ` v <= x"; |
|
1196 | 612 |
by (forward_tac [the_in_MM_subset] 1 THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
613 |
by (dtac in_LL_eq_Int 1 THEN REPEAT (assume_tac 1)); |
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
614 |
by (Asm_full_simp_tac 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
615 |
by (rtac subsetI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
616 |
by (etac DiffE 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
617 |
by (etac swap 1); |
2469 | 618 |
by (fast_tac (!claset addEs [ssubst]) 1); |
1196 | 619 |
val GG_subset = result(); |
620 |
||
621 |
goal thy |
|
1461 | 622 |
"!!x. [| well_ord(LL(t_n, succ(k), y), S); \ |
623 |
\ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ |
|
624 |
\ well_ord(y,R); ~Finite(y); x Int y = 0; \ |
|
625 |
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
|
626 |
\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
|
627 |
\ |] ==> (UN b<ordertype(LL(t_n, succ(k), y), S). \ |
|
628 |
\ (GG(t_n, succ(k), y)) ` \ |
|
629 |
\ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b)) = x"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
630 |
by (rtac equalityI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
631 |
by (rtac subsetI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
632 |
by (etac OUN_E 1); |
1196 | 633 |
by (eresolve_tac [GG_subset RS subsetD] 1 THEN TRYALL assume_tac); |
634 |
by (eresolve_tac [ordermap_bij RS bij_converse_bij RS |
|
1461 | 635 |
bij_is_fun RS apply_type] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
636 |
by (etac ltD 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
637 |
by (rtac subsetI 1); |
1196 | 638 |
by (eresolve_tac [exists_in_LL RS bexE] 1 THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
639 |
by (rtac OUN_I 1); |
1196 | 640 |
by (resolve_tac [Ord_ordertype RSN (2, ltI)] 1 THEN (assume_tac 2)); |
641 |
by (eresolve_tac [ordermap_type RS apply_type] 1); |
|
642 |
by (eresolve_tac [ordermap_bij RS bij_is_inj RS left_inverse RS ssubst] 1 |
|
1461 | 643 |
THEN REPEAT (assume_tac 1)); |
1196 | 644 |
val OUN_eq_x = result(); |
645 |
||
646 |
(* ********************************************************************** *) |
|
1461 | 647 |
(* Every element of the family is less than or equipollent to n-k (m) *) |
1196 | 648 |
(* ********************************************************************** *) |
649 |
||
650 |
goalw thy [MM_def] |
|
1461 | 651 |
"!!w. [| w : MM(t_n, k, y); t_n <= {v:Pow(x Un y). v eqpoll n} \ |
652 |
\ |] ==> w eqpoll n"; |
|
2469 | 653 |
by (Fast_tac 1); |
1196 | 654 |
val in_MM_eqpoll_n = result(); |
655 |
||
656 |
goalw thy [LL_def, MM_def] |
|
1461 | 657 |
"!!w. w : LL(t_n, k, y) ==> k lepoll w"; |
2469 | 658 |
by (Fast_tac 1); |
1196 | 659 |
val in_LL_eqpoll_n = result(); |
660 |
||
661 |
goalw thy [GG_def] |
|
1461 | 662 |
"!!x. [| \ |
663 |
\ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ |
|
664 |
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
|
665 |
\ well_ord(LL(t_n, succ(k), y), S); k:nat; m:nat |] \ |
|
666 |
\ ==> ALL b<ordertype(LL(t_n, succ(k), y), S). \ |
|
667 |
\ (GG(t_n, succ(k), y)) ` \ |
|
668 |
\ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b) lepoll m"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
669 |
by (rtac oallI 1); |
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
670 |
by (asm_full_simp_tac |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
671 |
(!simpset delsimps ball_simps |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
672 |
addsimps [ltD, |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
673 |
ordermap_bij RS bij_converse_bij RS |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
674 |
bij_is_fun RS apply_type]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
675 |
by (rtac eqpoll_sum_imp_Diff_lepoll 1); |
2469 | 676 |
by (REPEAT (fast_tac |
677 |
(FOL_cs addSDs [ltD] |
|
1461 | 678 |
addSIs [eqpoll_sum_imp_Diff_lepoll, in_LL_eqpoll_n] |
679 |
addEs [unique_superset_in_MM RS theI RS conjunct1 RS in_MM_eqpoll_n, |
|
2469 | 680 |
in_LL_eq_Int RS equalityD1 RS (Int_lower1 RSN (2, subset_trans)), |
1461 | 681 |
ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1)); |
1196 | 682 |
val all_in_lepoll_m = result(); |
683 |
||
684 |
(* ********************************************************************** *) |
|
1461 | 685 |
(* The main theorem AC16(n, k) ==> WO4(n-k) *) |
1196 | 686 |
(* ********************************************************************** *) |
687 |
||
688 |
goalw thy [AC16_def,WO4_def] |
|
1461 | 689 |
"!!n k. [| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
690 |
by (rtac allI 1); |
1196 | 691 |
by (excluded_middle_tac "Finite(A)" 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
692 |
by (rtac lemma1 2 THEN REPEAT (assume_tac 2)); |
1196 | 693 |
by (resolve_tac [lemma2 RS revcut_rl] 1); |
694 |
by (REPEAT (eresolve_tac [exE, conjE] 1)); |
|
695 |
by (eres_inst_tac [("x","A Un y")] allE 1); |
|
696 |
by (forward_tac [infinite_Un] 1 THEN (mp_tac 1)); |
|
697 |
by (REPEAT (eresolve_tac [exE, conjE] 1)); |
|
698 |
by (resolve_tac [well_ord_LL RS exE] 1 THEN REPEAT (assume_tac 1)); |
|
2469 | 699 |
by (fast_tac (!claset addSIs [nat_succI, add_type]) 1); |
1196 | 700 |
by (res_inst_tac [("x","ordertype(LL(T, succ(k), y), x)")] exI 1); |
701 |
by (res_inst_tac [("x","lam b:ordertype(LL(T, succ(k), y), x). \ |
|
1461 | 702 |
\ (GG(T, succ(k), y)) ` \ |
703 |
\ (converse(ordermap(LL(T, succ(k), y), x)) ` b)")] exI 1); |
|
2469 | 704 |
by (Simp_tac 1); |
1196 | 705 |
by (fast_tac (empty_cs addSIs [conjI, lam_funtype RS domain_of_fun] |
1461 | 706 |
addSEs [Ord_ordertype, all_in_lepoll_m, OUN_eq_x]) 1); |
1196 | 707 |
qed "AC16_WO4"; |