author | paulson |
Tue, 20 Aug 1996 12:23:13 +0200 | |
changeset 1924 | 0f1a583457da |
parent 1461 | 6bcb44e4d6e5 |
child 1932 | cc9f1ba8f29a |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/WO2_AC16.ML |
1196 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1196 | 4 |
|
5 |
The proof of WO2 ==> AC16(k #+ m, k) |
|
6 |
||
7 |
The main part of the proof is the inductive reasoning concerning |
|
8 |
properties of constructed family T_gamma. |
|
9 |
The proof deals with three cases for ordinals: 0, succ and limit ordinal. |
|
10 |
The first instance is trivial, the third not difficult, but the second |
|
11 |
is very complicated requiring many lemmas. |
|
12 |
We also need to prove that at any stage gamma the set |
|
13 |
(s - Union(...) - k_gamma) (Rubin & Rubin page 15) |
|
14 |
contains m distinct elements (in fact is equipollent to s) |
|
15 |
*) |
|
16 |
||
17 |
(* ********************************************************************** *) |
|
1461 | 18 |
(* case of limit ordinal *) |
1196 | 19 |
(* ********************************************************************** *) |
20 |
||
21 |
goal thy "!!Z. [| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y) \ |
|
1461 | 22 |
\ --> (EX! Y. Y:F(y) & f(z)<=Y); \ |
23 |
\ ALL i j. i le j --> F(i) <= F(j); j le i; i<x; z<a; \ |
|
24 |
\ V: F(i); f(z)<=V; W:F(j); f(z)<=W |] \ |
|
25 |
\ ==> V = W"; |
|
1196 | 26 |
by (REPEAT (eresolve_tac [asm_rl, allE, impE] 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
27 |
by (dtac subsetD 1 THEN (assume_tac 1)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
28 |
by (REPEAT (dtac ospec 1 THEN (assume_tac 1))); |
1196 | 29 |
by (eresolve_tac [disjI2 RSN (2, impE)] 1); |
30 |
by (fast_tac (FOL_cs addSIs [bexI]) 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
31 |
by (etac ex1_two_eq 1 THEN (REPEAT (ares_tac [conjI] 1))); |
1196 | 32 |
val lemma3_1 = result(); |
33 |
||
34 |
goal thy "!!Z. [| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y) \ |
|
1461 | 35 |
\ --> (EX! Y. Y:F(y) & f(z)<=Y); \ |
36 |
\ ALL i j. i le j --> F(i) <= F(j); i<x; j<x; z<a; \ |
|
37 |
\ V: F(i); f(z)<=V; W:F(j); f(z)<=W |] \ |
|
38 |
\ ==> V = W"; |
|
1196 | 39 |
by (res_inst_tac [("j","j")] (lt_Ord RS (lt_Ord RSN (2, Ord_linear_le))) 1 |
1461 | 40 |
THEN (REPEAT (assume_tac 1))); |
1196 | 41 |
by (eresolve_tac [lemma3_1 RS sym] 1 THEN (REPEAT (assume_tac 1))); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
42 |
by (etac lemma3_1 1 THEN (REPEAT (assume_tac 1))); |
1196 | 43 |
val lemma3 = result(); |
44 |
||
45 |
goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X & \ |
|
1461 | 46 |
\ (ALL x<a. x < y | (EX Y:F(y). fa(x) <= Y) --> \ |
47 |
\ (EX! Y. Y : F(y) & fa(x) <= Y)); x < a |] \ |
|
48 |
\ ==> ALL y<x. ALL z<a. z < y | (EX Y:F(y). fa(z) <= Y) --> \ |
|
49 |
\ (EX! Y. Y : F(y) & fa(z) <= Y)"; |
|
1196 | 50 |
by (REPEAT (resolve_tac [oallI, impI] 1)); |
51 |
by (dresolve_tac [ltD RSN (2, bspec)] 1 THEN (assume_tac 1)); |
|
52 |
by (eresolve_tac [lt_trans RSN (2, impE)] 1 THEN (REPEAT (assume_tac 1))); |
|
53 |
by (fast_tac (FOL_cs addSEs [oallE]) 1); |
|
54 |
val lemma4 = result(); |
|
55 |
||
56 |
goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X & \ |
|
1461 | 57 |
\ (ALL x<a. x < y | (EX Y:F(y). fa(x) <= Y) --> \ |
58 |
\ (EX! Y. Y : F(y) & fa(x) <= Y)); \ |
|
59 |
\ x < a; Limit(x); ALL i j. i le j --> F(i) <= F(j) |] \ |
|
60 |
\ ==> (UN x<x. F(x)) <= X & \ |
|
61 |
\ (ALL xa<a. xa < x | (EX x:UN x<x. F(x). fa(xa) <= x) \ |
|
62 |
\ --> (EX! Y. Y : (UN x<x. F(x)) & fa(xa) <= Y))"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
63 |
by (rtac conjI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
64 |
by (rtac subsetI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
65 |
by (etac OUN_E 1); |
1196 | 66 |
by (dresolve_tac [ltD RSN (2, bspec)] 1 THEN (assume_tac 1)); |
67 |
by (eresolve_tac [lt_trans RSN (2, impE)] 1 THEN (REPEAT (assume_tac 1))); |
|
68 |
by (fast_tac AC_cs 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
69 |
by (dtac lemma4 1 THEN (assume_tac 1)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
70 |
by (rtac oallI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
71 |
by (rtac impI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
72 |
by (etac disjE 1); |
1196 | 73 |
by (forward_tac [Limit_has_succ RSN (2, ospec)] 1 THEN (REPEAT (assume_tac 1))); |
74 |
by (dres_inst_tac [("A","a"),("x","xa")] ospec 1 THEN (assume_tac 1)); |
|
75 |
by (eresolve_tac [lt_Ord RS le_refl RSN (2, disjI1 RSN (2, impE))] 1 |
|
1461 | 76 |
THEN (assume_tac 1)); |
1196 | 77 |
by (REPEAT (eresolve_tac [ex1E, conjE] 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
78 |
by (rtac ex1I 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
79 |
by (rtac conjI 1 THEN (assume_tac 2)); |
1196 | 80 |
by (eresolve_tac [Limit_has_succ RS OUN_I] 1 THEN (TRYALL assume_tac)); |
81 |
by (REPEAT (eresolve_tac [conjE, OUN_E] 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
82 |
by (etac lemma3 1 THEN (TRYALL assume_tac)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
83 |
by (etac Limit_has_succ 1 THEN (assume_tac 1)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
84 |
by (etac bexE 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
85 |
by (rtac ex1I 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
86 |
by (etac conjI 1 THEN (assume_tac 1)); |
1196 | 87 |
by (REPEAT (eresolve_tac [conjE, OUN_E] 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
88 |
by (etac lemma3 1 THEN (TRYALL assume_tac)); |
1196 | 89 |
val lemma5 = result(); |
90 |
||
91 |
(* ********************************************************************** *) |
|
1461 | 92 |
(* case of successor ordinal *) |
1196 | 93 |
(* ********************************************************************** *) |
94 |
||
95 |
(* |
|
96 |
First quite complicated proof of the fact used in the recursive construction |
|
97 |
of the family T_gamma (WO2 ==> AC16(k #+ m, k)) - the fact that at any stage |
|
98 |
gamma the set (s - Union(...) - k_gamma) is equipollent to s |
|
99 |
(Rubin & Rubin page 15). |
|
100 |
*) |
|
101 |
||
102 |
(* ********************************************************************** *) |
|
1461 | 103 |
(* dbl_Diff_eqpoll_Card *) |
1196 | 104 |
(* ********************************************************************** *) |
105 |
||
106 |
goal thy "!!A. [| A eqpoll a; Card(a); ~Finite(a); B lesspoll a; \ |
|
1461 | 107 |
\ C lesspoll a |] ==> A - B - C eqpoll a"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
108 |
by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1))); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
109 |
by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1))); |
1196 | 110 |
val dbl_Diff_eqpoll_Card = result(); |
111 |
||
112 |
(* ********************************************************************** *) |
|
1461 | 113 |
(* Case of finite ordinals *) |
1196 | 114 |
(* ********************************************************************** *) |
115 |
||
116 |
goalw thy [lesspoll_def] |
|
1461 | 117 |
"!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
118 |
by (rtac conjI 1); |
1196 | 119 |
by (dresolve_tac [nat_le_infinite_Ord RS le_imp_lepoll] 1 |
1461 | 120 |
THEN (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
121 |
by (rewtac Finite_def); |
1196 | 122 |
by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_trans]) 2); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
123 |
by (rtac lepoll_trans 1 THEN (assume_tac 2)); |
1196 | 124 |
by (fast_tac (AC_cs addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_subset RS |
1461 | 125 |
subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1); |
1196 | 126 |
val Finite_lesspoll_infinite_Ord = result(); |
127 |
||
128 |
goal thy "!!x. x:X ==> Union(X) = Union(X-{x}) Un x"; |
|
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
129 |
by (fast_tac eq_cs 1); |
1196 | 130 |
val Union_eq_Un_Diff = result(); |
131 |
||
132 |
goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x)) \ |
|
1461 | 133 |
\ --> Finite(Union(X))"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
134 |
by (etac nat_induct 1); |
1196 | 135 |
by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0] |
1461 | 136 |
addSIs [nat_0I RS nat_into_Finite] addIs [Union_0 RS ssubst]) 1); |
1196 | 137 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
138 |
by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1)); |
|
139 |
by (res_inst_tac [("P","%z. Finite(z)")] (Union_eq_Un_Diff RS ssubst) 1 |
|
1461 | 140 |
THEN (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
141 |
by (rtac Finite_Un 1); |
1196 | 142 |
by (fast_tac AC_cs 2); |
143 |
by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll]) 1); |
|
144 |
val Finite_Union_lemma = result(); |
|
145 |
||
146 |
goal thy "!!X. [| ALL x:X. Finite(x); Finite(X) |] ==> Finite(Union(X))"; |
|
147 |
by (eresolve_tac [Finite_def RS def_imp_iff RS iffD1 RS bexE] 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
148 |
by (dtac Finite_Union_lemma 1); |
1196 | 149 |
by (fast_tac AC_cs 1); |
150 |
val Finite_Union = result(); |
|
151 |
||
152 |
goalw thy [Finite_def] "!!x. [| x lepoll n; n:nat |] ==> Finite(x)"; |
|
153 |
by (fast_tac (AC_cs |
|
1461 | 154 |
addEs [nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll) RS exE, |
155 |
Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD]) 1); |
|
1196 | 156 |
val lepoll_nat_num_imp_Finite = result(); |
157 |
||
158 |
goal thy "!!X. [| ALL x:X. x lepoll n & x <= T; well_ord(T, R); X lepoll b; \ |
|
1461 | 159 |
\ b<a; ~Finite(a); Card(a); n:nat |] \ |
160 |
\ ==> Union(X) lesspoll a"; |
|
1196 | 161 |
by (excluded_middle_tac "Finite(X)" 1); |
162 |
by (resolve_tac [Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord)] 2 |
|
1461 | 163 |
THEN (REPEAT (assume_tac 3))); |
1196 | 164 |
by (fast_tac (AC_cs addSEs [lepoll_nat_num_imp_Finite] |
1461 | 165 |
addSIs [Finite_Union]) 2); |
1196 | 166 |
by (dresolve_tac [lt_Ord RSN (2, lepoll_imp_ex_le_eqpoll)] 1 THEN (assume_tac 1)); |
167 |
by (REPEAT (eresolve_tac [exE, conjE] 1)); |
|
168 |
by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1)); |
|
169 |
by (eresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1) RS |
|
1461 | 170 |
exE] 1); |
1196 | 171 |
by (forward_tac [bij_is_surj RS surj_image_eq] 1); |
172 |
by (dresolve_tac [[bij_is_fun, subset_refl] MRS image_fun] 1); |
|
173 |
by (dresolve_tac [sym RS trans] 1 THEN (assume_tac 1)); |
|
174 |
by (hyp_subst_tac 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
175 |
by (rtac lepoll_lesspoll_lesspoll 1); |
1196 | 176 |
by (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1 |
1461 | 177 |
THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
178 |
by (rtac UN_lepoll 1 |
1461 | 179 |
THEN (TRYALL (fast_tac (AC_cs addSEs [lt_Ord])))); |
1196 | 180 |
val Union_lesspoll = result(); |
181 |
||
182 |
(* ********************************************************************** *) |
|
1461 | 183 |
(* recfunAC16_lepoll_index *) |
1196 | 184 |
(* ********************************************************************** *) |
185 |
||
186 |
goal thy "A Un {a} = cons(a, A)"; |
|
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
187 |
by (fast_tac eq_cs 1); |
1196 | 188 |
val Un_sing_eq_cons = result(); |
189 |
||
190 |
goal thy "!!A. A lepoll B ==> A Un {a} lepoll succ(B)"; |
|
191 |
by (asm_simp_tac (AC_ss addsimps [Un_sing_eq_cons, succ_def]) 1); |
|
192 |
by (eresolve_tac [mem_not_refl RSN (2, cons_lepoll_cong)] 1); |
|
193 |
val Un_lepoll_succ = result(); |
|
194 |
||
195 |
goal thy "!!a. Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0"; |
|
196 |
by (fast_tac (AC_cs addSIs [OUN_I, le_refl] addIs [equalityI]) 1); |
|
197 |
val Diff_UN_succ_empty = result(); |
|
198 |
||
199 |
goal thy "!!a. Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X"; |
|
200 |
by (fast_tac (AC_cs addSIs [OUN_I, le_refl]) 1); |
|
201 |
val Diff_UN_succ_subset = result(); |
|
202 |
||
203 |
goal thy "!!x. Ord(x) ==> \ |
|
1461 | 204 |
\ recfunAC16(f, g, x, a) - (UN i<x. recfunAC16(f, g, i, a)) lepoll 1"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
205 |
by (etac Ord_cases 1); |
1196 | 206 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0, |
1461 | 207 |
empty_subsetI RS subset_imp_lepoll]) 1); |
1196 | 208 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit, |
1461 | 209 |
Diff_cancel, empty_subsetI RS subset_imp_lepoll]) 2); |
1196 | 210 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1); |
211 |
by (resolve_tac [conjI RS (expand_if RS iffD2)] 1); |
|
212 |
by (fast_tac (AC_cs addSIs [empty_subsetI RS subset_imp_lepoll] |
|
1461 | 213 |
addSEs [Diff_UN_succ_empty RS ssubst]) 1); |
1196 | 214 |
by (fast_tac (AC_cs addSEs [Diff_UN_succ_subset RS subset_imp_lepoll RS |
1461 | 215 |
(singleton_eqpoll_1 RS eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1); |
1196 | 216 |
val recfunAC16_Diff_lepoll_1 = result(); |
217 |
||
218 |
goal thy "!!z. [| z : F(x); Ord(x) |] \ |
|
1461 | 219 |
\ ==> z:F(LEAST i. z:F(i)) - (UN j<(LEAST i. z:F(i)). F(j))"; |
1196 | 220 |
by (fast_tac (AC_cs addEs [less_LeastE] addSEs [OUN_E, LeastI]) 1); |
221 |
val in_Least_Diff = result(); |
|
222 |
||
223 |
goal thy "!!w. [| (LEAST i. w:F(i)) = (LEAST i. z:F(i)); \ |
|
1461 | 224 |
\ w:(UN i<a. F(i)); z:(UN i<a. F(i)) |] \ |
225 |
\ ==> EX b<a. w:(F(b) - (UN c<b. F(c))) & z:(F(b) - (UN c<b. F(c)))"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
226 |
by (REPEAT (etac OUN_E 1)); |
1196 | 227 |
by (dresolve_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1)); |
228 |
by (forward_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
229 |
by (rtac oexI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
230 |
by (rtac conjI 1 THEN (assume_tac 2)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
231 |
by (etac subst 1 THEN (assume_tac 1)); |
1196 | 232 |
by (eresolve_tac [lt_Ord RSN (2, Least_le) RS lt_trans1] 1 |
1461 | 233 |
THEN (REPEAT (assume_tac 1))); |
1196 | 234 |
val Least_eq_imp_ex = result(); |
235 |
||
236 |
goal thy "!!A. [| A lepoll 1; a:A; b:A |] ==> a=b"; |
|
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
237 |
by (fast_tac (AC_cs addSDs [lepoll_1_is_sing]) 1); |
1196 | 238 |
val two_in_lepoll_1 = result(); |
239 |
||
240 |
goal thy "!!a. [| ALL i<a. F(i)-(UN j<i. F(j)) lepoll 1; Limit(a) |] \ |
|
1461 | 241 |
\ ==> (UN x<a. F(x)) lepoll a"; |
1196 | 242 |
by (resolve_tac [lepoll_def RS (def_imp_iff RS iffD2)] 1); |
243 |
by (res_inst_tac [("x","lam z: (UN x<a. F(x)). LEAST i. z:F(i)")] exI 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
244 |
by (rewtac inj_def); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
245 |
by (rtac CollectI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
246 |
by (rtac lam_type 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
247 |
by (etac OUN_E 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
248 |
by (etac Least_in_Ord 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
249 |
by (etac ltD 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
250 |
by (etac lt_Ord2 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
251 |
by (rtac ballI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
252 |
by (rtac ballI 1); |
1196 | 253 |
by (asm_simp_tac AC_ss 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
254 |
by (rtac impI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
255 |
by (dtac Least_eq_imp_ex 1 THEN (REPEAT (assume_tac 1))); |
1196 | 256 |
by (fast_tac (AC_cs addSEs [two_in_lepoll_1]) 1); |
257 |
val UN_lepoll_index = result(); |
|
258 |
||
259 |
goal thy "!!y. Ord(y) ==> recfunAC16(f, fa, y, a) lepoll y"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
260 |
by (etac trans_induct 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
261 |
by (etac Ord_cases 1); |
1196 | 262 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0, lepoll_refl]) 1); |
263 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1); |
|
264 |
by (fast_tac (AC_cs addIs [conjI RS (expand_if RS iffD2)] |
|
1461 | 265 |
addSDs [succI1 RSN (2, bspec)] |
266 |
addSEs [subset_succI RS subset_imp_lepoll RSN (2, lepoll_trans), |
|
267 |
Un_lepoll_succ]) 1); |
|
1196 | 268 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 1); |
269 |
by (fast_tac (AC_cs addSEs [lt_Ord RS recfunAC16_Diff_lepoll_1] |
|
1461 | 270 |
addSIs [UN_lepoll_index]) 1); |
1196 | 271 |
val recfunAC16_lepoll_index = result(); |
272 |
||
273 |
goal thy "!!y. [| recfunAC16(f,g,y,a) <= {X: Pow(A). X eqpoll n}; \ |
|
1461 | 274 |
\ A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |] \ |
275 |
\ ==> Union(recfunAC16(f,g,y,a)) lesspoll a"; |
|
1196 | 276 |
by (eresolve_tac [eqpoll_def RS def_imp_iff RS iffD1 RS exE] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
277 |
by (rtac Union_lesspoll 1 THEN (TRYALL assume_tac)); |
1196 | 278 |
by (eresolve_tac [lt_Ord RS recfunAC16_lepoll_index] 3); |
279 |
by (eresolve_tac [[bij_is_inj, Card_is_Ord RS well_ord_Memrel] MRS |
|
1461 | 280 |
well_ord_rvimage] 2 THEN (assume_tac 2)); |
1196 | 281 |
by (fast_tac (AC_cs addSEs [eqpoll_imp_lepoll]) 1); |
282 |
val Union_recfunAC16_lesspoll = result(); |
|
283 |
||
284 |
goal thy |
|
285 |
"!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \ |
|
1461 | 286 |
\ Card(a); ~ Finite(a); A eqpoll a; \ |
287 |
\ k : nat; m : nat; y<a; \ |
|
288 |
\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |] \ |
|
289 |
\ ==> A - Union(recfunAC16(f, fa, y, a)) - fa`y eqpoll a"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
290 |
by (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
291 |
by (rtac Union_recfunAC16_lesspoll 1 THEN (REPEAT (assume_tac 1))); |
1196 | 292 |
by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1)); |
293 |
by (resolve_tac [nat_succI RSN (2, bexI RS (Finite_def RS def_imp_iff RS |
|
1461 | 294 |
iffD2)) RS (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1 |
295 |
THEN (TRYALL assume_tac)); |
|
1196 | 296 |
by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type) RS CollectE] 1 |
1461 | 297 |
THEN (TRYALL assume_tac)); |
1196 | 298 |
val dbl_Diff_eqpoll = result(); |
299 |
||
300 |
(* back to the proof *) |
|
301 |
||
302 |
val disj_Un_eqpoll_nat_sum = disj_Un_eqpoll_sum RS ( |
|
303 |
sum_eqpoll_cong RSN (2, |
|
304 |
nat_sum_eqpoll_sum RSN (3, |
|
305 |
eqpoll_trans RS eqpoll_trans))) |> standard; |
|
306 |
||
307 |
goal thy "!!x. [| x : Pow(A - B - fa`i); x eqpoll m; \ |
|
1461 | 308 |
\ fa : bij(a, {x: Pow(A) . x eqpoll k}); i<a; k:nat; m:nat |] \ |
309 |
\ ==> fa ` i Un x : {x: Pow(A) . x eqpoll k #+ m}"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
310 |
by (rtac CollectI 1); |
1196 | 311 |
by (fast_tac (AC_cs addSIs [PowD RS (PowD RSN (2, Un_least RS PowI))] |
1461 | 312 |
addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
313 |
by (rtac disj_Un_eqpoll_nat_sum 1 |
1461 | 314 |
THEN (TRYALL assume_tac)); |
1196 | 315 |
by (fast_tac (AC_cs addSIs [equals0I]) 1); |
316 |
by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)] 1 |
|
1461 | 317 |
THEN (REPEAT (assume_tac 1))); |
1196 | 318 |
val Un_in_Collect = result(); |
319 |
||
320 |
(* ********************************************************************** *) |
|
1461 | 321 |
(* Lemmas simplifying assumptions *) |
1196 | 322 |
(* ********************************************************************** *) |
323 |
||
324 |
goal thy "!!j. [| ALL y:succ(j). y<a --> F(y)<=X & (ALL x<a. x<y | P(x,y) \ |
|
1461 | 325 |
\ --> Q(x,y)); succ(j)<a |] \ |
326 |
\ ==> F(j)<=X & (ALL x<a. x<j | P(x,j) --> Q(x,j))"; |
|
1196 | 327 |
by (dresolve_tac [succI1 RSN (2, bspec)] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
328 |
by (etac impE 1); |
1196 | 329 |
by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl) RS lt_trans] 1 |
1461 | 330 |
THEN (REPEAT (assume_tac 1))); |
1196 | 331 |
val lemma6 = result(); |
332 |
||
333 |
goal thy "!!j. [| F(j)<=X; (ALL x<a. x<j | P(x,j) --> Q(x,j)); succ(j)<a |] \ |
|
1461 | 334 |
\ ==> P(j,j) --> F(j) <= X & (ALL x<a. x le j | P(x,j) --> Q(x,j))"; |
1196 | 335 |
by (fast_tac (AC_cs addSEs [leE]) 1); |
336 |
val lemma7 = result(); |
|
337 |
||
338 |
(* ********************************************************************** *) |
|
339 |
(* Lemmas needded to prove ex_next_set which means that for any successor *) |
|
1461 | 340 |
(* ordinal there is a set satisfying certain properties *) |
1196 | 341 |
(* ********************************************************************** *) |
342 |
||
343 |
goal thy "!!A. [| A eqpoll a; ~ Finite(a); Ord(a); m:nat |] \ |
|
1461 | 344 |
\ ==> EX X:Pow(A). X eqpoll m"; |
1196 | 345 |
by (eresolve_tac [Ord_nat RSN (2, ltI) RS |
1461 | 346 |
(nat_le_infinite_Ord RSN (2, lt_trans2)) RS |
347 |
leI RS le_imp_lepoll RS |
|
348 |
((eqpoll_sym RS eqpoll_imp_lepoll) RSN (2, lepoll_trans)) RS |
|
349 |
lepoll_imp_eqpoll_subset RS exE] 1 |
|
350 |
THEN REPEAT (assume_tac 1)); |
|
1196 | 351 |
by (fast_tac (AC_cs addSEs [eqpoll_sym]) 1); |
352 |
val ex_subset_eqpoll = result(); |
|
353 |
||
354 |
goal thy "!!A. [| A <= B Un C; A Int C = 0 |] ==> A <= B"; |
|
355 |
by (fast_tac (AC_cs addDs [equals0D]) 1); |
|
356 |
val subset_Un_disjoint = result(); |
|
357 |
||
358 |
goal thy "!!F. [| X:Pow(A - Union(B) -C); T:B; F<=T |] ==> F Int X = 0"; |
|
359 |
by (fast_tac (AC_cs addSIs [equals0I]) 1); |
|
360 |
val Int_empty = result(); |
|
361 |
||
362 |
(* ********************************************************************** *) |
|
1461 | 363 |
(* equipollent subset (and finite) is the whole set *) |
1196 | 364 |
(* ********************************************************************** *) |
365 |
||
366 |
goal thy "!!A. [| A <= B; a : A; A - {a} = B - {a} |] ==> A = B"; |
|
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
367 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
1196 | 368 |
val Diffs_eq_imp_eq = result(); |
369 |
||
370 |
goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
371 |
by (etac nat_induct 1); |
1196 | 372 |
by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1); |
373 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
374 |
by (REPEAT (etac conjE 1)); |
1196 | 375 |
by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1 |
1461 | 376 |
THEN (assume_tac 1)); |
1196 | 377 |
by (forward_tac [subsetD RS Diff_sing_lepoll] 1 |
1461 | 378 |
THEN REPEAT (assume_tac 1)); |
1196 | 379 |
by (forward_tac [lepoll_Diff_sing] 1); |
380 |
by (REPEAT (eresolve_tac [allE, impE] 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
381 |
by (rtac conjI 1); |
1196 | 382 |
by (fast_tac AC_cs 2); |
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
383 |
by (fast_tac (eq_cs addSEs [singletonE]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
384 |
by (etac Diffs_eq_imp_eq 1 |
1461 | 385 |
THEN REPEAT (assume_tac 1)); |
1196 | 386 |
val subset_imp_eq_lemma = result(); |
387 |
||
388 |
goal thy "!!A. [| A <= B; m lepoll A; B lepoll m; m:nat |] ==> A=B"; |
|
389 |
by (fast_tac (FOL_cs addSDs [subset_imp_eq_lemma]) 1); |
|
390 |
val subset_imp_eq = result(); |
|
391 |
||
392 |
goal thy "!!f. [| f:bij(a, {Y:X. Y eqpoll succ(k)}); k:nat; f`b<=f`y; b<a; \ |
|
1461 | 393 |
\ y<a |] ==> b=y"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
394 |
by (dtac subset_imp_eq 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
395 |
by (etac nat_succI 3); |
1196 | 396 |
by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS |
1461 | 397 |
CollectE, eqpoll_sym RS eqpoll_imp_lepoll]) 1); |
1196 | 398 |
by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS |
1461 | 399 |
CollectE, eqpoll_imp_lepoll]) 1); |
1196 | 400 |
by (rewrite_goals_tac [bij_def, inj_def]); |
401 |
by (fast_tac (AC_cs addSDs [ltD]) 1); |
|
402 |
val bij_imp_arg_eq = result(); |
|
403 |
||
404 |
goal thy |
|
405 |
"!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \ |
|
1461 | 406 |
\ Card(a); ~ Finite(a); A eqpoll a; \ |
407 |
\ k : nat; m : nat; y<a; \ |
|
408 |
\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}); \ |
|
409 |
\ ~ (EX Y:recfunAC16(f, fa, y, a). fa`y <= Y) |] \ |
|
410 |
\ ==> EX X:{Y: Pow(A). Y eqpoll succ(k #+ m)}. fa`y <= X & \ |
|
411 |
\ (ALL b<a. fa`b <= X --> \ |
|
412 |
\ (ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))"; |
|
1196 | 413 |
by (eresolve_tac [dbl_Diff_eqpoll RS ex_subset_eqpoll RS bexE] 1 |
1461 | 414 |
THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
415 |
by (etac Card_is_Ord 1); |
1196 | 416 |
by (forward_tac [Un_in_Collect] 2 THEN REPEAT (assume_tac 2)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
417 |
by (etac CollectE 4); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
418 |
by (rtac bexI 4); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
419 |
by (rtac CollectI 5); |
1196 | 420 |
by (assume_tac 5); |
421 |
by (eresolve_tac [add_succ RS subst] 5); |
|
422 |
by (assume_tac 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
423 |
by (etac nat_succI 1); |
1196 | 424 |
by (assume_tac 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
425 |
by (rtac conjI 1); |
1196 | 426 |
by (fast_tac AC_cs 1); |
427 |
by (REPEAT (resolve_tac [ballI, impI, oallI, notI] 1)); |
|
428 |
by (dresolve_tac [Int_empty RSN (2, subset_Un_disjoint)] 1 |
|
1461 | 429 |
THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
430 |
by (dtac bij_imp_arg_eq 1 THEN REPEAT (assume_tac 1)); |
1196 | 431 |
by (hyp_subst_tac 1); |
432 |
by (eresolve_tac [bexI RSN (2, notE)] 1 THEN TRYALL assume_tac); |
|
433 |
val ex_next_set = result(); |
|
434 |
||
435 |
(* ********************************************************************** *) |
|
1461 | 436 |
(* Lemma ex_next_Ord states that for any successor *) |
437 |
(* ordinal there is a number of the set satisfying certain properties *) |
|
1196 | 438 |
(* ********************************************************************** *) |
439 |
||
440 |
goal thy |
|
441 |
"!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \ |
|
1461 | 442 |
\ Card(a); ~ Finite(a); A eqpoll a; \ |
443 |
\ k : nat; m : nat; y<a; \ |
|
444 |
\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}); \ |
|
445 |
\ f : bij(a, {Y: Pow(A). Y eqpoll succ(k #+ m)}); \ |
|
446 |
\ ~ (EX Y:recfunAC16(f, fa, y, a). fa`y <= Y) |] \ |
|
447 |
\ ==> EX c<a. fa`y <= f`c & \ |
|
448 |
\ (ALL b<a. fa`b <= f`c --> \ |
|
449 |
\ (ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
450 |
by (dtac ex_next_set 1 THEN REPEAT (assume_tac 1)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
451 |
by (etac bexE 1); |
1196 | 452 |
by (resolve_tac [bij_converse_bij RS bij_is_fun RS apply_type RS ltI RSN |
1461 | 453 |
(2, oexI)] 1); |
1196 | 454 |
by (resolve_tac [right_inverse_bij RS ssubst] 1 |
1461 | 455 |
THEN REPEAT (ares_tac [Card_is_Ord] 1)); |
1196 | 456 |
val ex_next_Ord = result(); |
457 |
||
458 |
goal thy "!!Z. [| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y:Z Un {W} & P(Y)"; |
|
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
459 |
by (fast_tac ZF_cs 1); |
1196 | 460 |
val ex1_in_Un_sing = result(); |
461 |
||
462 |
(* ********************************************************************** *) |
|
1461 | 463 |
(* Lemma simplifying assumptions *) |
1196 | 464 |
(* ********************************************************************** *) |
465 |
||
466 |
goal thy "!!j. [| ALL x<a. x<j | (EX xa:F(j). P(x, xa)) \ |
|
1461 | 467 |
\ --> (EX! Y. Y:F(j) & P(x, Y)); F(j) <= X; \ |
468 |
\ L : X; P(j, L) & (ALL x<a. P(x, L) --> (ALL xa:F(j). ~P(x, xa))) |] \ |
|
469 |
\ ==> F(j) Un {L} <= X & \ |
|
470 |
\ (ALL x<a. x le j | (EX xa:F(j) Un {L}. P(x, xa)) --> \ |
|
471 |
\ (EX! Y. Y:F(j) Un {L} & P(x, Y)))"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
472 |
by (rtac conjI 1); |
1196 | 473 |
by (fast_tac (AC_cs addSIs [singleton_subsetI]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
474 |
by (rtac oallI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
475 |
by (etac oallE 1 THEN (contr_tac 2)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
476 |
by (rtac impI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
477 |
by (etac disjE 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
478 |
by (etac leE 1); |
1196 | 479 |
by (eresolve_tac [disjI1 RSN (2, impE)] 1 THEN (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
480 |
by (rtac ex1E 1 THEN (assume_tac 1)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
481 |
by (etac ex1_in_Un_sing 1); |
1196 | 482 |
by (fast_tac AC_cs 1); |
483 |
by (fast_tac AC_cs 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
484 |
by (etac bexE 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
485 |
by (etac UnE 1); |
1196 | 486 |
by (fast_tac (AC_cs addSEs [ex1_in_Un_sing]) 1); |
487 |
by (fast_tac AC_cs 1); |
|
488 |
val lemma8 = result(); |
|
489 |
||
490 |
(* ********************************************************************** *) |
|
491 |
(* The main part of the proof: inductive proof of the property of T_gamma *) |
|
1461 | 492 |
(* lemma main_induct *) |
1196 | 493 |
(* ********************************************************************** *) |
494 |
||
495 |
goal thy |
|
1461 | 496 |
"!!a. [| b < a; f : bij(a, {Y: Pow(A) . Y eqpoll succ(k #+ m)}); \ |
497 |
\ fa : bij(a, {Y: Pow(A) . Y eqpoll succ(k)}); \ |
|
498 |
\ ~Finite(a); Card(a); A eqpoll a; k : nat; m : nat |] \ |
|
499 |
\ ==> recfunAC16(f, fa, b, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)} & \ |
|
500 |
\ (ALL x<a. x < b | (EX Y:recfunAC16(f, fa, b, a). fa ` x <= Y) --> \ |
|
501 |
\ (EX! Y. Y:recfunAC16(f, fa, b, a) & fa ` x <= Y))"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
502 |
by (rtac impE 1 THEN (REPEAT (assume_tac 2))); |
1196 | 503 |
by (eresolve_tac [lt_Ord RS trans_induct] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
504 |
by (rtac impI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
505 |
by (etac Ord_cases 1); |
1196 | 506 |
(* case 0 *) |
507 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0]) 1); |
|
508 |
by (fast_tac (AC_cs addSEs [ltE]) 1); |
|
509 |
(* case Limit *) |
|
510 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 2); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
511 |
by (etac lemma5 2 THEN (REPEAT (assume_tac 2))); |
1196 | 512 |
by (fast_tac (FOL_cs addSEs [recfunAC16_mono]) 2); |
513 |
(* case succ *) |
|
514 |
by (hyp_subst_tac 1); |
|
515 |
by (eresolve_tac [lemma6 RS conjE] 1 THEN (assume_tac 1)); |
|
516 |
by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1); |
|
517 |
by (resolve_tac [conjI RS (expand_if RS iffD2)] 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
518 |
by (etac lemma7 1 THEN (REPEAT (assume_tac 1))); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
519 |
by (rtac impI 1); |
1196 | 520 |
by (resolve_tac [ex_next_Ord RS oexE] 1 |
1461 | 521 |
THEN REPEAT (ares_tac [le_refl RS lt_trans] 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
522 |
by (etac lemma8 1 THEN (assume_tac 1)); |
1196 | 523 |
by (resolve_tac [bij_is_fun RS apply_type] 1 THEN (assume_tac 1)); |
524 |
by (eresolve_tac [Least_le RS lt_trans2 RS ltD] 1 |
|
1461 | 525 |
THEN REPEAT (ares_tac [lt_Ord, succ_leI] 1)); |
1196 | 526 |
by (eresolve_tac [lt_Ord RSN (2, LeastI)] 1 THEN (assume_tac 1)); |
527 |
val main_induct = result(); |
|
528 |
||
529 |
(* ********************************************************************** *) |
|
1461 | 530 |
(* Lemma to simplify the inductive proof *) |
1200 | 531 |
(* - the desired property is a consequence of the inductive assumption *) |
1196 | 532 |
(* ********************************************************************** *) |
533 |
||
534 |
val [prem1, prem2, prem3, prem4] = goal thy |
|
1461 | 535 |
"[| (!!b. b<a ==> F(b) <= S & (ALL x<a. (x<b | (EX Y:F(b). f`x <= Y)) \ |
536 |
\ --> (EX! Y. Y : F(b) & f`x <= Y))); \ |
|
537 |
\ f:a->f``(a); Limit(a); (!!i j. i le j ==> F(i) <= F(j)) |] \ |
|
538 |
\ ==> (UN j<a. F(j)) <= S & \ |
|
539 |
\ (ALL x:f``a. EX! Y. Y : (UN j<a. F(j)) & x <= Y)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
540 |
by (rtac conjI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
541 |
by (rtac subsetI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
542 |
by (etac OUN_E 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
543 |
by (dtac prem1 1); |
1196 | 544 |
by (fast_tac AC_cs 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
545 |
by (rtac ballI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
546 |
by (etac imageE 1); |
1196 | 547 |
by (dresolve_tac [prem3 RS Limit_is_Ord RSN (2, ltI) RS |
1461 | 548 |
(prem3 RS Limit_has_succ)] 1); |
1196 | 549 |
by (forward_tac [prem1] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
550 |
by (etac conjE 1); |
1196 | 551 |
by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
552 |
by (etac impE 1); |
1196 | 553 |
by (fast_tac (AC_cs addSEs [leI RS succ_leE RS lt_Ord RS le_refl]) 1); |
554 |
by (dresolve_tac [prem2 RSN (2, apply_equality)] 1); |
|
555 |
by (REPEAT (eresolve_tac [conjE, ex1E] 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
556 |
by (rtac ex1I 1); |
1196 | 557 |
by (fast_tac (AC_cs addSIs [OUN_I]) 1); |
558 |
by (REPEAT (eresolve_tac [conjE, OUN_E] 1)); |
|
559 |
by (eresolve_tac [lt_Ord RSN (2, lt_Ord RS Ord_linear_le)] 1 THEN (assume_tac 1)); |
|
560 |
by (dresolve_tac [prem4 RS subsetD] 2 THEN (assume_tac 2)); |
|
1200 | 561 |
by (fast_tac FOL_cs 2); |
1196 | 562 |
by (forward_tac [prem1] 1); |
563 |
by (forward_tac [succ_leE] 1); |
|
564 |
by (dresolve_tac [prem4 RS subsetD] 1 THEN (assume_tac 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
565 |
by (etac conjE 1); |
1196 | 566 |
by (dresolve_tac [lt_trans RSN (2, ospec)] 1 THEN (TRYALL assume_tac)); |
567 |
by (dresolve_tac [disjI1 RSN (2, mp)] 1 THEN (assume_tac 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
568 |
by (etac ex1_two_eq 1); |
1200 | 569 |
by (REPEAT (fast_tac FOL_cs 1)); |
1196 | 570 |
val lemma_simp_induct = result(); |
571 |
||
572 |
(* ********************************************************************** *) |
|
1461 | 573 |
(* The target theorem *) |
1196 | 574 |
(* ********************************************************************** *) |
575 |
||
576 |
goalw thy [AC16_def] |
|
1461 | 577 |
"!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
578 |
by (rtac allI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
579 |
by (rtac impI 1); |
1196 | 580 |
by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 THEN (REPEAT (assume_tac 1))); |
581 |
by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1 |
|
1461 | 582 |
THEN (REPEAT (ares_tac [add_type] 1))); |
1196 | 583 |
by (forward_tac [WO2_imp_ex_Card] 1); |
584 |
by (REPEAT (eresolve_tac [exE,conjE] 1)); |
|
585 |
by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS |
|
1461 | 586 |
def_imp_iff RS iffD1)] 1 THEN (assume_tac 1)); |
1196 | 587 |
by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS |
1461 | 588 |
def_imp_iff RS iffD1)] 1 THEN (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
589 |
by (REPEAT (etac exE 1)); |
1196 | 590 |
by (res_inst_tac [("x","UN j<a. recfunAC16(fa,f,j,a)")] exI 1); |
591 |
by (res_inst_tac [("P","%z. ?Y & (ALL x:z. ?Z(x))")] |
|
1461 | 592 |
(bij_is_surj RS surj_image_eq RS subst) 1 |
593 |
THEN (assume_tac 1)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
594 |
by (rtac lemma_simp_induct 1); |
1196 | 595 |
by (eresolve_tac [bij_is_fun RS surj_image RS surj_is_fun] 2); |
596 |
by (eresolve_tac [eqpoll_imp_lepoll RS lepoll_infinite RS |
|
1461 | 597 |
infinite_Card_is_InfCard RS InfCard_is_Limit] 2 |
598 |
THEN REPEAT (assume_tac 2)); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
599 |
by (etac recfunAC16_mono 2); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
600 |
by (rtac main_induct 1 |
1461 | 601 |
THEN REPEAT (ares_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1)); |
1196 | 602 |
qed "WO2_AC16"; |