author | paulson |
Thu, 10 Sep 1998 17:42:44 +0200 | |
changeset 5470 | 855654b691db |
parent 5147 | 825877190618 |
child 6070 | 032babd0120b |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/AC16_lemmas.ML |
1196 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1196 | 4 |
|
5 |
Lemmas used in the proofs concerning AC16 |
|
6 |
*) |
|
7 |
||
8 |
open AC16_lemmas; |
|
9 |
||
5137 | 10 |
Goal "a~:A ==> cons(a,A)-{a}=A"; |
2496 | 11 |
by (Fast_tac 1); |
3731 | 12 |
qed "cons_Diff_eq"; |
1196 | 13 |
|
5068 | 14 |
Goalw [lepoll_def] "1 lepoll X <-> (EX x. x:X)"; |
1206 | 15 |
by (rtac iffI 1); |
4091 | 16 |
by (fast_tac (claset() addIs [inj_is_fun RS apply_type]) 1); |
1206 | 17 |
by (etac exE 1); |
1196 | 18 |
by (res_inst_tac [("x","lam a:1. x")] exI 1); |
4091 | 19 |
by (fast_tac (claset() addSIs [lam_injective]) 1); |
3731 | 20 |
qed "nat_1_lepoll_iff"; |
1196 | 21 |
|
5068 | 22 |
Goal "X eqpoll 1 <-> (EX x. X={x})"; |
1206 | 23 |
by (rtac iffI 1); |
24 |
by (etac eqpollE 1); |
|
1196 | 25 |
by (dresolve_tac [nat_1_lepoll_iff RS iffD1] 1); |
4091 | 26 |
by (fast_tac (claset() addSIs [lepoll_1_is_sing]) 1); |
27 |
by (fast_tac (claset() addSIs [singleton_eqpoll_1]) 1); |
|
3731 | 28 |
qed "eqpoll_1_iff_singleton"; |
1196 | 29 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
30 |
Goalw [succ_def] "[| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)"; |
4091 | 31 |
by (fast_tac (claset() addSEs [cons_eqpoll_cong, mem_irrefl]) 1); |
3731 | 32 |
qed "cons_eqpoll_succ"; |
1196 | 33 |
|
5068 | 34 |
Goal "{Y:Pow(X). Y eqpoll 1} = {{x}. x:X}"; |
1206 | 35 |
by (rtac equalityI 1); |
36 |
by (rtac subsetI 1); |
|
37 |
by (etac CollectE 1); |
|
1196 | 38 |
by (dresolve_tac [eqpoll_1_iff_singleton RS iffD1] 1); |
4091 | 39 |
by (fast_tac (claset() addSIs [RepFunI]) 1); |
1206 | 40 |
by (rtac subsetI 1); |
41 |
by (etac RepFunE 1); |
|
42 |
by (rtac CollectI 1); |
|
2469 | 43 |
by (Fast_tac 1); |
4091 | 44 |
by (fast_tac (claset() addSIs [singleton_eqpoll_1]) 1); |
3731 | 45 |
qed "subsets_eqpoll_1_eq"; |
1196 | 46 |
|
5068 | 47 |
Goalw [eqpoll_def, bij_def] "X eqpoll {{x}. x:X}"; |
1196 | 48 |
by (res_inst_tac [("x","lam x:X. {x}")] exI 1); |
1206 | 49 |
by (rtac IntI 1); |
1196 | 50 |
by (rewrite_goals_tac [inj_def, surj_def]); |
2469 | 51 |
by (Asm_full_simp_tac 1); |
4091 | 52 |
by (fast_tac (claset() addSIs [lam_type, RepFunI] |
1461 | 53 |
addIs [singleton_eq_iff RS iffD1]) 1); |
2469 | 54 |
by (Asm_full_simp_tac 1); |
4091 | 55 |
by (fast_tac (claset() addSIs [lam_type]) 1); |
3731 | 56 |
qed "eqpoll_RepFun_sing"; |
1196 | 57 |
|
5068 | 58 |
Goal "{Y:Pow(X). Y eqpoll 1} eqpoll X"; |
1196 | 59 |
by (resolve_tac [subsets_eqpoll_1_eq RS ssubst] 1); |
60 |
by (resolve_tac [eqpoll_RepFun_sing RS eqpoll_sym] 1); |
|
3731 | 61 |
qed "subsets_eqpoll_1_eqpoll"; |
1196 | 62 |
|
5137 | 63 |
Goal "[| InfCard(x); y:Pow(x); y eqpoll succ(z) |] \ |
1461 | 64 |
\ ==> (LEAST i. i:y) : y"; |
1196 | 65 |
by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS |
1461 | 66 |
succ_lepoll_imp_not_empty RS not_emptyE] 1); |
4091 | 67 |
by (fast_tac (claset() addIs [LeastI] |
1461 | 68 |
addSDs [InfCard_is_Card RS Card_is_Ord, PowD RS subsetD] |
69 |
addEs [Ord_in_Ord]) 1); |
|
3731 | 70 |
qed "InfCard_Least_in"; |
1196 | 71 |
|
5137 | 72 |
Goalw [lepoll_def] "[| InfCard(x); n:nat |] ==> \ |
1461 | 73 |
\ {y:Pow(x). y eqpoll succ(succ(n))} lepoll \ |
74 |
\ x*{y:Pow(x). y eqpoll succ(n)}"; |
|
1196 | 75 |
by (res_inst_tac [("x","lam y:{y:Pow(x). y eqpoll succ(succ(n))}. \ |
1461 | 76 |
\ <LEAST i. i:y, y-{LEAST i. i:y}>")] exI 1); |
1196 | 77 |
by (res_inst_tac [("d","%z. cons(fst(z),snd(z))")] lam_injective 1); |
1206 | 78 |
by (rtac SigmaI 1); |
79 |
by (etac CollectE 1); |
|
2469 | 80 |
by (Asm_full_simp_tac 3); |
1206 | 81 |
by (rtac equalityI 3); |
2469 | 82 |
by (Fast_tac 4); |
1206 | 83 |
by (rtac subsetI 3); |
84 |
by (etac consE 3); |
|
2469 | 85 |
by (Fast_tac 4); |
1206 | 86 |
by (rtac CollectI 2); |
2469 | 87 |
by (Fast_tac 2); |
1196 | 88 |
by (resolve_tac [PowD RS subsetD] 1 THEN (assume_tac 1)); |
4091 | 89 |
by (REPEAT (fast_tac (claset() addSIs [Diff_sing_eqpoll] |
1461 | 90 |
addIs [InfCard_Least_in]) 1)); |
3731 | 91 |
qed "subsets_lepoll_lemma1"; |
1196 | 92 |
|
93 |
val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))"; |
|
1206 | 94 |
by (rtac subsetI 1); |
1196 | 95 |
by (res_inst_tac [("Q","ALL y:z. y<=x")] (excluded_middle RS disjE) 1); |
2496 | 96 |
by (Fast_tac 2); |
1206 | 97 |
by (etac swap 1); |
98 |
by (rtac ballI 1); |
|
99 |
by (rtac Ord_linear_le 1); |
|
100 |
by (dtac le_imp_subset 3 THEN (assume_tac 3)); |
|
4091 | 101 |
by (fast_tac (claset() addDs prems) 1); |
102 |
by (fast_tac (claset() addDs prems) 1); |
|
103 |
by (fast_tac (claset() addSEs [leE,ltE]) 1); |
|
3731 | 104 |
qed "set_of_Ord_succ_Union"; |
1196 | 105 |
|
5137 | 106 |
Goal "j<=i ==> i ~: j"; |
4091 | 107 |
by (fast_tac (claset() addSEs [mem_irrefl]) 1); |
3731 | 108 |
qed "subset_not_mem"; |
1196 | 109 |
|
110 |
val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> succ(Union(z)) ~: z"; |
|
111 |
by (resolve_tac [set_of_Ord_succ_Union RS subset_not_mem] 1); |
|
112 |
by (eresolve_tac prems 1); |
|
3731 | 113 |
qed "succ_Union_not_mem"; |
1196 | 114 |
|
5068 | 115 |
Goal "Union(cons(succ(Union(z)),z)) = succ(Union(z))"; |
2496 | 116 |
by (Fast_tac 1); |
3731 | 117 |
qed "Union_cons_eq_succ_Union"; |
1196 | 118 |
|
5137 | 119 |
Goal "[| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j"; |
4091 | 120 |
by (fast_tac (claset() addSDs [le_imp_subset] addEs [Ord_linear_le]) 1); |
3731 | 121 |
qed "Un_Ord_disj"; |
1196 | 122 |
|
5137 | 123 |
Goal "x:X ==> Union(X) = x Un Union(X-{x})"; |
2496 | 124 |
by (Fast_tac 1); |
3731 | 125 |
qed "Union_eq_Un"; |
1196 | 126 |
|
5137 | 127 |
Goal "n:nat ==> \ |
1461 | 128 |
\ ALL z. (ALL y:z. Ord(y)) & z eqpoll n & z~=0 --> Union(z) : z"; |
1206 | 129 |
by (etac nat_induct 1); |
4091 | 130 |
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); |
1196 | 131 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
1206 | 132 |
by (etac natE 1); |
4091 | 133 |
by (fast_tac (claset() addSDs [eqpoll_1_iff_singleton RS iffD1] |
1461 | 134 |
addSIs [Union_singleton]) 1); |
1196 | 135 |
by (hyp_subst_tac 1); |
136 |
by (REPEAT (eresolve_tac [conjE, not_emptyE] 1)); |
|
137 |
by (eres_inst_tac [("x","z-{xb}")] allE 1); |
|
1206 | 138 |
by (etac impE 1); |
4091 | 139 |
by (fast_tac (claset() addSEs [Diff_sing_eqpoll, |
1461 | 140 |
Diff_sing_eqpoll RS eqpoll_succ_imp_not_empty]) 1); |
1196 | 141 |
by (resolve_tac [Union_eq_Un RSN (2, subst_elem)] 1 THEN (assume_tac 2)); |
142 |
by (forward_tac [bspec] 1 THEN (assume_tac 1)); |
|
143 |
by (dresolve_tac [Diff_subset RS subsetD RSN (2, bspec)] 1 THEN (assume_tac 1)); |
|
1206 | 144 |
by (dtac Un_Ord_disj 1 THEN (assume_tac 1)); |
145 |
by (etac DiffE 1); |
|
146 |
by (etac disjE 1); |
|
147 |
by (etac subst_elem 1 THEN (assume_tac 1)); |
|
148 |
by (rtac subst_elem 1 THEN (TRYALL assume_tac)); |
|
3731 | 149 |
qed "Union_in_lemma"; |
1196 | 150 |
|
5137 | 151 |
Goal "[| ALL x:z. Ord(x); z eqpoll n; z~=0; n:nat |] \ |
1461 | 152 |
\ ==> Union(z) : z"; |
1206 | 153 |
by (dtac Union_in_lemma 1); |
1196 | 154 |
by (fast_tac FOL_cs 1); |
3731 | 155 |
qed "Union_in"; |
1196 | 156 |
|
5137 | 157 |
Goal "[| InfCard(x); z:Pow(x); z eqpoll n; n:nat |] \ |
1461 | 158 |
\ ==> succ(Union(z)) : x"; |
1196 | 159 |
by (resolve_tac [Limit_has_succ RS ltE] 1 THEN (assume_tac 3)); |
1206 | 160 |
by (etac InfCard_is_Limit 1); |
1196 | 161 |
by (excluded_middle_tac "z=0" 1); |
4091 | 162 |
by (fast_tac (claset() addSIs [InfCard_is_Limit RS Limit_has_0] |
163 |
addss (simpset())) 2); |
|
1196 | 164 |
by (resolve_tac |
1461 | 165 |
[PowD RS subsetD RS (InfCard_is_Card RS Card_is_Ord RSN (2, ltI))] 1 |
166 |
THEN (TRYALL assume_tac)); |
|
4091 | 167 |
by (fast_tac (claset() addSIs [Union_in] |
2469 | 168 |
addSEs [PowD RS subsetD RSN |
169 |
(2, InfCard_is_Card RS Card_is_Ord RS Ord_in_Ord)]) 1); |
|
3731 | 170 |
qed "succ_Union_in_x"; |
1196 | 171 |
|
5137 | 172 |
Goalw [lepoll_def] "[| InfCard(x); n:nat |] ==> \ |
1461 | 173 |
\ {y:Pow(x). y eqpoll succ(n)} lepoll \ |
174 |
\ {y:Pow(x). y eqpoll succ(succ(n))}"; |
|
1196 | 175 |
by (res_inst_tac [("x","lam z:{y:Pow(x). y eqpoll succ(n)}. \ |
1461 | 176 |
\ cons(succ(Union(z)), z)")] exI 1); |
1196 | 177 |
by (res_inst_tac [("d","%z. z-{Union(z)}")] lam_injective 1); |
178 |
by (resolve_tac [Union_cons_eq_succ_Union RS ssubst] 2); |
|
1206 | 179 |
by (rtac cons_Diff_eq 2); |
4091 | 180 |
by (fast_tac (claset() addSDs [InfCard_is_Card RS Card_is_Ord] |
1461 | 181 |
addEs [Ord_in_Ord] addSIs [succ_Union_not_mem]) 2); |
1206 | 182 |
by (rtac CollectI 1); |
4091 | 183 |
by (fast_tac (claset() addSEs [cons_eqpoll_succ] |
1196 | 184 |
addSIs [succ_Union_not_mem] |
185 |
addSDs [InfCard_is_Card RS Card_is_Ord] |
|
186 |
addEs [Ord_in_Ord]) 2); |
|
5137 | 187 |
by (fast_tac (claset() addSIs [succ_Union_in_x]) 1); |
3731 | 188 |
qed "succ_lepoll_succ_succ"; |
1196 | 189 |
|
5137 | 190 |
Goal "[| InfCard(X); n:nat |] \ |
1461 | 191 |
\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X"; |
1206 | 192 |
by (etac nat_induct 1); |
193 |
by (rtac subsets_eqpoll_1_eqpoll 1); |
|
194 |
by (rtac eqpollI 1); |
|
1196 | 195 |
by (resolve_tac [subsets_lepoll_lemma1 RS lepoll_trans] 1 |
1461 | 196 |
THEN (REPEAT (assume_tac 1))); |
1196 | 197 |
by (resolve_tac [InfCard_is_Card RS Card_is_Ord RS well_ord_Memrel RS |
1461 | 198 |
well_ord_InfCard_square_eq RS eqpoll_imp_lepoll |
199 |
RSN (2, lepoll_trans)] 1 THEN (assume_tac 2)); |
|
1196 | 200 |
by (resolve_tac [InfCard_is_Card RS Card_cardinal_eq RS ssubst] 2 |
1461 | 201 |
THEN (REPEAT (assume_tac 2))); |
1196 | 202 |
by (eresolve_tac [eqpoll_refl RS prod_eqpoll_cong RS eqpoll_imp_lepoll] 1); |
4091 | 203 |
by (fast_tac (claset() addEs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans] |
1461 | 204 |
addSIs [succ_lepoll_succ_succ]) 1); |
3731 | 205 |
qed "subsets_eqpoll_X"; |
1196 | 206 |
|
5137 | 207 |
Goalw [surj_def] "[| f:surj(A,B); y<=B |] \ |
1461 | 208 |
\ ==> f``(converse(f)``y) = y"; |
4091 | 209 |
by (fast_tac (claset() addDs [apply_equality2] |
2496 | 210 |
addEs [apply_iff RS iffD2]) 1); |
3731 | 211 |
qed "image_vimage_eq"; |
1196 | 212 |
|
5137 | 213 |
Goal "[| f:inj(A,B); y<=A |] ==> converse(f)``(f``y) = y"; |
4091 | 214 |
by (fast_tac (claset() addSEs [inj_is_fun RS apply_Pair] |
1461 | 215 |
addDs [inj_equality]) 1); |
3731 | 216 |
qed "vimage_image_eq"; |
1196 | 217 |
|
5137 | 218 |
Goalw [eqpoll_def] "A eqpoll B \ |
1461 | 219 |
\ ==> {Y:Pow(A). Y eqpoll n} eqpoll {Y:Pow(B). Y eqpoll n}"; |
1206 | 220 |
by (etac exE 1); |
1196 | 221 |
by (res_inst_tac [("x","lam X:{Y:Pow(A). EX f. f : bij(Y, n)}. f``X")] exI 1); |
222 |
by (res_inst_tac [("d","%Z. converse(f)``Z")] lam_bijective 1); |
|
4091 | 223 |
by (fast_tac (claset() |
1461 | 224 |
addSIs [bij_is_inj RS restrict_bij RS bij_converse_bij RS comp_bij] |
1196 | 225 |
addSEs [bij_is_fun RS fun_is_rel RS image_subset RS PowI]) 1); |
4091 | 226 |
by (fast_tac (claset() addSIs [bij_converse_bij RS bij_is_inj RS restrict_bij |
1461 | 227 |
RS bij_converse_bij RS comp_bij] |
1196 | 228 |
addSEs [bij_converse_bij RS bij_is_fun RS fun_is_rel |
1461 | 229 |
RS image_subset RS PowI]) 1); |
4091 | 230 |
by (fast_tac (claset() addSEs [bij_is_inj RS vimage_image_eq]) 1); |
231 |
by (fast_tac (claset() addSEs [bij_is_surj RS image_vimage_eq]) 1); |
|
3731 | 232 |
qed "subsets_eqpoll"; |
1196 | 233 |
|
5137 | 234 |
Goalw [WO2_def] "WO2 ==> EX a. Card(a) & X eqpoll a"; |
1196 | 235 |
by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); |
4091 | 236 |
by (fast_tac (claset() addSEs [well_ord_Memrel RS well_ord_cardinal_eqpoll RS |
1461 | 237 |
(eqpoll_sym RSN (2, eqpoll_trans)) RS eqpoll_sym] |
238 |
addSIs [Card_cardinal]) 1); |
|
3731 | 239 |
qed "WO2_imp_ex_Card"; |
1196 | 240 |
|
5137 | 241 |
Goal "[| X lepoll Y; ~Finite(X) |] ==> ~Finite(Y)"; |
1196 | 242 |
by (fast_tac (empty_cs addEs [notE, lepoll_Finite] addSIs [notI]) 1); |
3731 | 243 |
qed "lepoll_infinite"; |
1196 | 244 |
|
5137 | 245 |
Goalw [InfCard_def] "[| ~Finite(X); Card(X) |] ==> InfCard(X)"; |
4091 | 246 |
by (fast_tac (claset() addSEs [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
3731 | 247 |
qed "infinite_Card_is_InfCard"; |
1196 | 248 |
|
5137 | 249 |
Goal "[| WO2; n:nat; ~Finite(X) |] \ |
1461 | 250 |
\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X"; |
1206 | 251 |
by (dtac WO2_imp_ex_Card 1); |
1196 | 252 |
by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); |
253 |
by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1)); |
|
1206 | 254 |
by (dtac infinite_Card_is_InfCard 1 THEN (assume_tac 1)); |
1196 | 255 |
by (resolve_tac [eqpoll_trans RS eqpoll_trans] 1); |
1206 | 256 |
by (etac subsets_eqpoll 1); |
257 |
by (etac subsets_eqpoll_X 1 THEN (assume_tac 1)); |
|
258 |
by (etac eqpoll_sym 1); |
|
3731 | 259 |
qed "WO2_infinite_subsets_eqpoll_X"; |
1196 | 260 |
|
5137 | 261 |
Goal "well_ord(X,R) ==> EX a. Card(a) & X eqpoll a"; |
4091 | 262 |
by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll RS eqpoll_sym] |
1461 | 263 |
addSIs [Card_cardinal]) 1); |
3731 | 264 |
qed "well_ord_imp_ex_Card"; |
1196 | 265 |
|
5137 | 266 |
Goal "[| well_ord(X,R); n:nat; ~Finite(X) |] \ |
1461 | 267 |
\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X"; |
1206 | 268 |
by (dtac well_ord_imp_ex_Card 1); |
1196 | 269 |
by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); |
270 |
by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1)); |
|
1206 | 271 |
by (dtac infinite_Card_is_InfCard 1 THEN (assume_tac 1)); |
1196 | 272 |
by (resolve_tac [eqpoll_trans RS eqpoll_trans] 1); |
1206 | 273 |
by (etac subsets_eqpoll 1); |
274 |
by (etac subsets_eqpoll_X 1 THEN (assume_tac 1)); |
|
275 |
by (etac eqpoll_sym 1); |
|
3731 | 276 |
qed "well_ord_infinite_subsets_eqpoll_X"; |
1196 | 277 |