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