19 by (etac exE 1); |
19 by (etac exE 1); |
20 by (res_inst_tac [("x","n")] exI 1); |
20 by (res_inst_tac [("x","n")] exI 1); |
21 by (res_inst_tac [("x","lam i:n. {f`i}")] exI 1); |
21 by (res_inst_tac [("x","lam i:n. {f`i}")] exI 1); |
22 by (Asm_full_simp_tac 1); |
22 by (Asm_full_simp_tac 1); |
23 by (rewrite_goals_tac [bij_def, surj_def]); |
23 by (rewrite_goals_tac [bij_def, surj_def]); |
24 by (fast_tac (!claset addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun, |
24 by (fast_tac (claset() addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun, |
25 equalityI, singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
25 equalityI, singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
26 nat_1_lepoll_iff RS iffD2] |
26 nat_1_lepoll_iff RS iffD2] |
27 addSEs [apply_type, ltE]) 1); |
27 addSEs [apply_type, ltE]) 1); |
28 val lemma1 = result(); |
28 val lemma1 = result(); |
29 |
29 |
33 |
33 |
34 (* well_ord(x,r) ==> well_ord({{y,z}. y:x}, Something(x,z)) **) |
34 (* well_ord(x,r) ==> well_ord({{y,z}. y:x}, Something(x,z)) **) |
35 bind_thm ("well_ord_paired", (paired_bij RS bij_is_inj RS well_ord_rvimage)); |
35 bind_thm ("well_ord_paired", (paired_bij RS bij_is_inj RS well_ord_rvimage)); |
36 |
36 |
37 goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C"; |
37 goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C"; |
38 by (fast_tac (!claset addEs [notE, lepoll_trans]) 1); |
38 by (fast_tac (claset() addEs [notE, lepoll_trans]) 1); |
39 qed "lepoll_trans1"; |
39 qed "lepoll_trans1"; |
40 |
40 |
41 goalw thy [lepoll_def] |
41 goalw thy [lepoll_def] |
42 "!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)"; |
42 "!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)"; |
43 by (fast_tac (!claset addSEs [well_ord_rvimage]) 1); |
43 by (fast_tac (claset() addSEs [well_ord_rvimage]) 1); |
44 qed "well_ord_lepoll"; |
44 qed "well_ord_lepoll"; |
45 |
45 |
46 goal thy "!!X. [| well_ord(X,R); well_ord(Y,S) \ |
46 goal thy "!!X. [| well_ord(X,R); well_ord(Y,S) \ |
47 \ |] ==> EX T. well_ord(X Un Y, T)"; |
47 \ |] ==> EX T. well_ord(X Un Y, T)"; |
48 by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS well_ord_lepoll)] 1); |
48 by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS well_ord_lepoll)] 1); |
55 |
55 |
56 goal thy "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)"; |
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); |
57 by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1); |
58 by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS |
58 by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS |
59 well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); |
59 well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); |
60 by (fast_tac (!claset addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, |
60 by (fast_tac (claset() addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, |
61 equals0I, HartogI RSN (2, lepoll_trans1), |
61 equals0I, HartogI RSN (2, lepoll_trans1), |
62 subset_imp_lepoll RS (paired_eqpoll RS eqpoll_sym RS |
62 subset_imp_lepoll RS (paired_eqpoll RS eqpoll_sym RS |
63 eqpoll_imp_lepoll RSN (2, lepoll_trans))] |
63 eqpoll_imp_lepoll RSN (2, lepoll_trans))] |
64 addSEs [RepFunE, nat_not_Finite RS notE] addEs [mem_asym] |
64 addSEs [RepFunE, nat_not_Finite RS notE] addEs [mem_asym] |
65 addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite, |
65 addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite, |
66 paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
66 paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
67 RS lepoll_Finite]) 1); |
67 RS lepoll_Finite]) 1); |
68 val lemma2 = result(); |
68 val lemma2 = result(); |
69 |
69 |
70 val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)"; |
70 val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)"; |
71 by (fast_tac (!claset |
71 by (fast_tac (claset() |
72 addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1); |
72 addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1); |
73 qed "infinite_Un"; |
73 qed "infinite_Un"; |
74 |
74 |
75 (* ********************************************************************** *) |
75 (* ********************************************************************** *) |
76 (* There is a v : s_u such that k lepoll x Int y (in our case succ(k)) *) |
76 (* There is a v : s_u such that k lepoll x Int y (in our case succ(k)) *) |
88 goal thy "!!A. [| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \ |
88 goal thy "!!A. [| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \ |
89 \ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)"; |
89 \ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)"; |
90 by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); |
90 by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); |
91 by (ALLGOALS |
91 by (ALLGOALS |
92 (asm_simp_tac |
92 (asm_simp_tac |
93 (!simpset addsimps [inj_is_fun RS apply_type, left_inverse] |
93 (simpset() addsimps [inj_is_fun RS apply_type, left_inverse] |
94 setloop (split_tac [expand_if] ORELSE' Step_tac)))); |
94 setloop (split_tac [expand_if] ORELSE' Step_tac)))); |
95 qed "succ_not_lepoll_lemma"; |
95 qed "succ_not_lepoll_lemma"; |
96 |
96 |
97 goalw thy [lepoll_def, eqpoll_def, bij_def, surj_def] |
97 goalw thy [lepoll_def, eqpoll_def, bij_def, surj_def] |
98 "!!A. [| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; |
98 "!!A. [| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; |
99 by (fast_tac (!claset addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |
99 by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |
100 qed "succ_not_lepoll_imp_eqpoll"; |
100 qed "succ_not_lepoll_imp_eqpoll"; |
101 |
101 |
102 val [prem] = goalw thy [s_u_def] |
102 val [prem] = goalw thy [s_u_def] |
103 "(ALL v:s_u(u, t_n, k, y). k eqpoll v Int y ==> False) \ |
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"; |
104 \ ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y"; |
106 by (resolve_tac [prem RS FalseE] 1); |
106 by (resolve_tac [prem RS FalseE] 1); |
107 by (rtac ballI 1); |
107 by (rtac ballI 1); |
108 by (etac CollectE 1); |
108 by (etac CollectE 1); |
109 by (etac conjE 1); |
109 by (etac conjE 1); |
110 by (etac swap 1); |
110 by (etac swap 1); |
111 by (fast_tac (!claset addSEs [succ_not_lepoll_imp_eqpoll]) 1); |
111 by (fast_tac (claset() addSEs [succ_not_lepoll_imp_eqpoll]) 1); |
112 qed "suppose_not"; |
112 qed "suppose_not"; |
113 |
113 |
114 (* ********************************************************************** *) |
114 (* ********************************************************************** *) |
115 (* There is a k-2 element subset of y *) |
115 (* There is a k-2 element subset of y *) |
116 (* ********************************************************************** *) |
116 (* ********************************************************************** *) |
128 goal thy "!!y. [| well_ord(y,R); ~Finite(y); n:nat \ |
128 goal thy "!!y. [| well_ord(y,R); ~Finite(y); n:nat \ |
129 \ |] ==> EX z. z<=y & n eqpoll z"; |
129 \ |] ==> EX z. z<=y & n eqpoll z"; |
130 by (etac nat_lepoll_imp_ex_eqpoll_n 1); |
130 by (etac nat_lepoll_imp_ex_eqpoll_n 1); |
131 by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
131 by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
132 RSN (2, lepoll_trans)] 1 THEN (assume_tac 2)); |
132 RSN (2, lepoll_trans)] 1 THEN (assume_tac 2)); |
133 by (fast_tac (!claset addSIs [nat_le_infinite_Ord RS le_imp_lepoll] |
133 by (fast_tac (claset() addSIs [nat_le_infinite_Ord RS le_imp_lepoll] |
134 addSEs [Ord_ordertype, ordertype_eqpoll RS eqpoll_imp_lepoll |
134 addSEs [Ord_ordertype, ordertype_eqpoll RS eqpoll_imp_lepoll |
135 RS lepoll_infinite]) 1); |
135 RS lepoll_infinite]) 1); |
136 qed "ex_subset_eqpoll_n"; |
136 qed "ex_subset_eqpoll_n"; |
137 |
137 |
138 goalw thy [lesspoll_def] "!!n. n: nat ==> n lesspoll nat"; |
138 goalw thy [lesspoll_def] "!!n. n: nat ==> n lesspoll nat"; |
139 by (fast_tac (!claset addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll, |
139 by (fast_tac (claset() addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll, |
140 eqpoll_sym RS eqpoll_imp_lepoll] |
140 eqpoll_sym RS eqpoll_imp_lepoll] |
141 addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI |
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); |
142 RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1); |
143 qed "n_lesspoll_nat"; |
143 qed "n_lesspoll_nat"; |
144 |
144 |
160 by (Fast_tac 1); |
160 by (Fast_tac 1); |
161 qed "cons_cons_subset"; |
161 qed "cons_cons_subset"; |
162 |
162 |
163 goal thy "!!x. [| a eqpoll k; a<=y; b:y-a; u:x; x Int y = 0 \ |
163 goal thy "!!x. [| a eqpoll k; a<=y; b:y-a; u:x; x Int y = 0 \ |
164 \ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))"; |
164 \ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))"; |
165 by (fast_tac (!claset addSIs [cons_eqpoll_succ] addEs [equals0D]) 1); |
165 by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0D]) 1); |
166 qed "cons_cons_eqpoll"; |
166 qed "cons_cons_eqpoll"; |
167 |
167 |
168 goalw thy [s_u_def] "s_u(u, t_n, k, y) <= t_n"; |
168 goalw thy [s_u_def] "s_u(u, t_n, k, y) <= t_n"; |
169 by (Fast_tac 1); |
169 by (Fast_tac 1); |
170 qed "s_u_subset"; |
170 qed "s_u_subset"; |
171 |
171 |
172 goalw thy [s_u_def, succ_def] |
172 goalw thy [s_u_def, succ_def] |
173 "!!w. [| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; k eqpoll a \ |
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)"; |
174 \ |] ==> w: s_u(u, t_n, succ(k), y)"; |
175 by (fast_tac (!claset addDs [eqpoll_imp_lepoll RS cons_lepoll_cong] |
175 by (fast_tac (claset() addDs [eqpoll_imp_lepoll RS cons_lepoll_cong] |
176 addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); |
176 addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); |
177 qed "s_uI"; |
177 qed "s_uI"; |
178 |
178 |
179 goalw thy [s_u_def] "!!v. v : s_u(u, t_n, k, y) ==> u : v"; |
179 goalw thy [s_u_def] "!!v. v : s_u(u, t_n, k, y) ==> u : v"; |
180 by (Fast_tac 1); |
180 by (Fast_tac 1); |
211 by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1); |
211 by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1); |
212 by (dresolve_tac [eqpoll_sym RS cons_eqpoll_succ] 1); |
212 by (dresolve_tac [eqpoll_sym RS cons_eqpoll_succ] 1); |
213 by (Fast_tac 1); |
213 by (Fast_tac 1); |
214 by (dtac cons_eqpoll_succ 1); |
214 by (dtac cons_eqpoll_succ 1); |
215 by (Fast_tac 1); |
215 by (Fast_tac 1); |
216 by (fast_tac (!claset addSIs [nat_succI] |
216 by (fast_tac (claset() addSIs [nat_succI] |
217 addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS |
217 addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS |
218 (lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1); |
218 (lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1); |
219 qed "set_eq_cons"; |
219 qed "set_eq_cons"; |
220 |
220 |
221 goal thy |
221 goal thy |
283 |
283 |
284 goal thy |
284 goal thy |
285 "!!k. [| k:nat; m:nat |] ==> \ |
285 "!!k. [| k:nat; m:nat |] ==> \ |
286 \ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m"; |
286 \ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m"; |
287 by (eres_inst_tac [("n","k")] nat_induct 1); |
287 by (eres_inst_tac [("n","k")] nat_induct 1); |
288 by (simp_tac (!simpset addsimps [add_0]) 1); |
288 by (simp_tac (simpset() addsimps [add_0]) 1); |
289 by (fast_tac (!claset addIs [eqpoll_imp_lepoll RS |
289 by (fast_tac (claset() addIs [eqpoll_imp_lepoll RS |
290 (Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1); |
290 (Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1); |
291 by (REPEAT (resolve_tac [allI,impI] 1)); |
291 by (REPEAT (resolve_tac [allI,impI] 1)); |
292 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
292 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
293 by (Fast_tac 1); |
293 by (Fast_tac 1); |
294 by (eres_inst_tac [("x","A - {xa}")] allE 1); |
294 by (eres_inst_tac [("x","A - {xa}")] allE 1); |
295 by (eres_inst_tac [("x","B - {xa}")] allE 1); |
295 by (eres_inst_tac [("x","B - {xa}")] allE 1); |
296 by (etac impE 1); |
296 by (etac impE 1); |
297 by (asm_full_simp_tac (!simpset addsimps [add_succ]) 1); |
297 by (asm_full_simp_tac (simpset() addsimps [add_succ]) 1); |
298 by (fast_tac (!claset addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1); |
298 by (fast_tac (claset() addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1); |
299 by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2)); |
299 by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2)); |
300 by (Fast_tac 1); |
300 by (Fast_tac 1); |
301 qed "eqpoll_sum_imp_Diff_lepoll_lemma"; |
301 qed "eqpoll_sum_imp_Diff_lepoll_lemma"; |
302 |
302 |
303 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; \ |
303 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; \ |
315 |
315 |
316 goal thy |
316 goal thy |
317 "!!k. [| k:nat; m:nat |] ==> \ |
317 "!!k. [| k:nat; m:nat |] ==> \ |
318 \ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m"; |
318 \ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m"; |
319 by (eres_inst_tac [("n","k")] nat_induct 1); |
319 by (eres_inst_tac [("n","k")] nat_induct 1); |
320 by (fast_tac (!claset addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] |
320 by (fast_tac (claset() addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] |
321 addss (!simpset addsimps [add_0])) 1); |
321 addss (simpset() addsimps [add_0])) 1); |
322 by (REPEAT (resolve_tac [allI,impI] 1)); |
322 by (REPEAT (resolve_tac [allI,impI] 1)); |
323 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
323 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
324 by (fast_tac (!claset addSEs [eqpoll_imp_lepoll]) 1); |
324 by (fast_tac (claset() addSEs [eqpoll_imp_lepoll]) 1); |
325 by (eres_inst_tac [("x","A - {xa}")] allE 1); |
325 by (eres_inst_tac [("x","A - {xa}")] allE 1); |
326 by (eres_inst_tac [("x","B - {xa}")] allE 1); |
326 by (eres_inst_tac [("x","B - {xa}")] allE 1); |
327 by (etac impE 1); |
327 by (etac impE 1); |
328 by (fast_tac (!claset addSIs [Diff_sing_eqpoll, |
328 by (fast_tac (claset() addSIs [Diff_sing_eqpoll, |
329 eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym] |
329 eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym] |
330 addss (!simpset addsimps [add_succ])) 1); |
330 addss (simpset() addsimps [add_succ])) 1); |
331 by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2)); |
331 by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2)); |
332 by (Fast_tac 1); |
332 by (Fast_tac 1); |
333 qed "eqpoll_sum_imp_Diff_eqpoll_lemma"; |
333 qed "eqpoll_sum_imp_Diff_eqpoll_lemma"; |
334 |
334 |
335 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; \ |
335 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; \ |
345 (* back to the second part *) |
345 (* back to the second part *) |
346 (* ********************************************************************** *) |
346 (* ********************************************************************** *) |
347 |
347 |
348 goal thy "!!w. [| x Int y = 0; w <= x Un y |] \ |
348 goal thy "!!w. [| x Int y = 0; w <= x Un y |] \ |
349 \ ==> w Int (x - {u}) = w - cons(u, w Int y)"; |
349 \ ==> w Int (x - {u}) = w - cons(u, w Int y)"; |
350 by (fast_tac (!claset addEs [equals0D]) 1); |
350 by (fast_tac (claset() addEs [equals0D]) 1); |
351 qed "w_Int_eq_w_Diff"; |
351 qed "w_Int_eq_w_Diff"; |
352 |
352 |
353 goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \ |
353 goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \ |
354 \ l eqpoll a; t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ |
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; \ |
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 \ |
356 \ ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y \ |
357 \ |] ==> w Int (x - {u}) eqpoll m"; |
357 \ |] ==> w Int (x - {u}) eqpoll m"; |
358 by (etac CollectE 1); |
358 by (etac CollectE 1); |
359 by (resolve_tac [w_Int_eq_w_Diff RS ssubst] 1 THEN (assume_tac 1)); |
359 by (resolve_tac [w_Int_eq_w_Diff RS ssubst] 1 THEN (assume_tac 1)); |
360 by (fast_tac (!claset addSDs [s_u_subset RS subsetD]) 1); |
360 by (fast_tac (claset() addSDs [s_u_subset RS subsetD]) 1); |
361 by (fast_tac (!claset addEs [equals0D] addSDs [bspec] |
361 by (fast_tac (claset() addEs [equals0D] addSDs [bspec] |
362 addDs [s_u_subset RS subsetD] |
362 addDs [s_u_subset RS subsetD] |
363 addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_u_imp_u_in] |
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); |
364 addSIs [nat_succI, eqpoll_sum_imp_Diff_eqpoll]) 1); |
365 qed "w_Int_eqpoll_m"; |
365 qed "w_Int_eqpoll_m"; |
366 |
366 |
370 qed "eqpoll_m_not_empty"; |
370 qed "eqpoll_m_not_empty"; |
371 |
371 |
372 goal thy |
372 goal thy |
373 "!!z. [| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x \ |
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))}"; |
374 \ |] ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}"; |
375 by (fast_tac (!claset addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1); |
375 by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1); |
376 qed "cons_cons_in"; |
376 qed "cons_cons_in"; |
377 |
377 |
378 (* ********************************************************************** *) |
378 (* ********************************************************************** *) |
379 (* 2. {v:s_u. a <= v} is less than or equipollent *) |
379 (* 2. {v:s_u. a <= v} is less than or equipollent *) |
380 (* to {v:Pow(x). v eqpoll n-k} *) |
380 (* to {v:Pow(x). v eqpoll n-k} *) |
396 by (rtac CollectI 1); |
396 by (rtac CollectI 1); |
397 by (rtac lam_type 1); |
397 by (rtac lam_type 1); |
398 by (rtac CollectI 1); |
398 by (rtac CollectI 1); |
399 by (Fast_tac 1); |
399 by (Fast_tac 1); |
400 by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1)); |
400 by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1)); |
401 by (simp_tac (!simpset delsimps ball_simps) 1); |
401 by (simp_tac (simpset() delsimps ball_simps) 1); |
402 by (REPEAT (resolve_tac [ballI, impI] 1)); |
402 by (REPEAT (resolve_tac [ballI, impI] 1)); |
403 (** LEVEL 9 **) |
403 (** LEVEL 9 **) |
404 by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1 |
404 by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1 |
405 THEN REPEAT (assume_tac 1)); |
405 THEN REPEAT (assume_tac 1)); |
406 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); |
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)); |
407 by (dresolve_tac [cons_cons_in RSN (2, bspec)] 1 THEN REPEAT (assume_tac 1)); |
408 by (etac ex1_two_eq 1); |
408 by (etac ex1_two_eq 1); |
409 by (fast_tac (!claset addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
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); |
410 by (fast_tac (claset() addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
411 qed "subset_s_u_lepoll_w"; |
411 qed "subset_s_u_lepoll_w"; |
412 |
412 |
413 goal thy "!!k. [| 0<k; k:nat |] ==> EX l:nat. k = succ(l)"; |
413 goal thy "!!k. [| 0<k; k:nat |] ==> EX l:nat. k = succ(l)"; |
414 by (etac natE 1); |
414 by (etac natE 1); |
415 by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1); |
415 by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1); |
437 (* ********************************************************************** *) |
437 (* ********************************************************************** *) |
438 (* LL can be well ordered *) |
438 (* LL can be well ordered *) |
439 (* ********************************************************************** *) |
439 (* ********************************************************************** *) |
440 |
440 |
441 goal thy "{x:Pow(X). x lepoll 0} = {0}"; |
441 goal thy "{x:Pow(X). x lepoll 0} = {0}"; |
442 by (fast_tac (!claset addSDs [lepoll_0_is_0] |
442 by (fast_tac (claset() addSDs [lepoll_0_is_0] |
443 addSIs [lepoll_refl]) 1); |
443 addSIs [lepoll_refl]) 1); |
444 qed "subsets_lepoll_0_eq_unit"; |
444 qed "subsets_lepoll_0_eq_unit"; |
445 |
445 |
446 goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \ |
446 goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \ |
447 \ ==> EX S. well_ord({Y: Pow(X) . Y eqpoll succ(n)}, S)"; |
447 \ ==> EX S. well_ord({Y: Pow(X) . Y eqpoll succ(n)}, S)"; |
448 by (resolve_tac [well_ord_infinite_subsets_eqpoll_X |
448 by (resolve_tac [well_ord_infinite_subsets_eqpoll_X |
449 RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1 |
449 RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1 |
450 THEN (REPEAT (assume_tac 1))); |
450 THEN (REPEAT (assume_tac 1))); |
451 by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
451 by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
452 qed "well_ord_subsets_eqpoll_n"; |
452 qed "well_ord_subsets_eqpoll_n"; |
453 |
453 |
454 goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ |
454 goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ |
455 \ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; |
455 \ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; |
456 by (fast_tac (!claset addIs [le_refl, leI, le_imp_lepoll] |
456 by (fast_tac (claset() addIs [le_refl, leI, le_imp_lepoll] |
457 addSDs [lepoll_succ_disj] |
457 addSDs [lepoll_succ_disj] |
458 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
458 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
459 qed "subsets_lepoll_succ"; |
459 qed "subsets_lepoll_succ"; |
460 |
460 |
461 goal thy "!!n. n:nat ==> \ |
461 goal thy "!!n. n:nat ==> \ |
462 \ {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0"; |
462 \ {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0"; |
463 by (fast_tac (!claset addSEs [eqpoll_sym RS eqpoll_imp_lepoll |
463 by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_imp_lepoll |
464 RS lepoll_trans RS succ_lepoll_natE] |
464 RS lepoll_trans RS succ_lepoll_natE] |
465 addSIs [equals0I]) 1); |
465 addSIs [equals0I]) 1); |
466 qed "Int_empty"; |
466 qed "Int_empty"; |
467 |
467 |
468 (* ********************************************************************** *) |
468 (* ********************************************************************** *) |
477 goalw thy [wf_on_def, wf_def] "wf[{a}](0)"; |
477 goalw thy [wf_on_def, wf_def] "wf[{a}](0)"; |
478 by (Fast_tac 1); |
478 by (Fast_tac 1); |
479 qed "wf_on_unit"; |
479 qed "wf_on_unit"; |
480 |
480 |
481 goalw thy [well_ord_def] "well_ord({a},0)"; |
481 goalw thy [well_ord_def] "well_ord({a},0)"; |
482 by (simp_tac (!simpset addsimps [tot_ord_unit, wf_on_unit]) 1); |
482 by (simp_tac (simpset() addsimps [tot_ord_unit, wf_on_unit]) 1); |
483 qed "well_ord_unit"; |
483 qed "well_ord_unit"; |
484 |
484 |
485 (* ********************************************************************** *) |
485 (* ********************************************************************** *) |
486 (* well_ord_subsets_lepoll_n *) |
486 (* well_ord_subsets_lepoll_n *) |
487 (* ********************************************************************** *) |
487 (* ********************************************************************** *) |
488 |
488 |
489 goal thy "!!y r. [| well_ord(y,r); ~Finite(y); n:nat |] ==> \ |
489 goal thy "!!y r. [| well_ord(y,r); ~Finite(y); n:nat |] ==> \ |
490 \ EX R. well_ord({z:Pow(y). z lepoll n}, R)"; |
490 \ EX R. well_ord({z:Pow(y). z lepoll n}, R)"; |
491 by (etac nat_induct 1); |
491 by (etac nat_induct 1); |
492 by (fast_tac (!claset addSIs [well_ord_unit] |
492 by (fast_tac (claset() addSIs [well_ord_unit] |
493 addss (!simpset addsimps [subsets_lepoll_0_eq_unit])) 1); |
493 addss (simpset() addsimps [subsets_lepoll_0_eq_unit])) 1); |
494 by (etac exE 1); |
494 by (etac exE 1); |
495 by (eresolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 |
495 by (eresolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 |
496 THEN REPEAT (assume_tac 1)); |
496 THEN REPEAT (assume_tac 1)); |
497 by (asm_simp_tac (!simpset addsimps [subsets_lepoll_succ]) 1); |
497 by (asm_simp_tac (simpset() addsimps [subsets_lepoll_succ]) 1); |
498 by (dtac well_ord_radd 1 THEN (assume_tac 1)); |
498 by (dtac well_ord_radd 1 THEN (assume_tac 1)); |
499 by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS |
499 by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS |
500 (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
500 (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
501 by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
501 by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
502 qed "well_ord_subsets_lepoll_n"; |
502 qed "well_ord_subsets_lepoll_n"; |
503 |
503 |
504 goalw thy [LL_def, MM_def] |
504 goalw thy [LL_def, MM_def] |
505 "!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \ |
505 "!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \ |
506 \ ==> LL(t_n, k, y) <= {z:Pow(y). z lepoll n}"; |
506 \ ==> LL(t_n, k, y) <= {z:Pow(y). z lepoll n}"; |
507 by (fast_tac (!claset addSEs [RepFunE] |
507 by (fast_tac (claset() addSEs [RepFunE] |
508 addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll |
508 addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll |
509 RSN (2, lepoll_trans))]) 1); |
509 RSN (2, lepoll_trans))]) 1); |
510 qed "LL_subset"; |
510 qed "LL_subset"; |
511 |
511 |
512 goal thy "!!x. [| t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
512 goal thy "!!x. [| t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
524 goalw thy [MM_def, LL_def] |
524 goalw thy [MM_def, LL_def] |
525 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
525 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
526 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
526 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
527 \ v:LL(t_n, k, y) \ |
527 \ v:LL(t_n, k, y) \ |
528 \ |] ==> EX! w. w:MM(t_n, k, y) & v<=w"; |
528 \ |] ==> EX! w. w:MM(t_n, k, y) & v<=w"; |
529 by (safe_tac (!claset addSEs [RepFunE])); |
529 by (safe_tac (claset() addSEs [RepFunE])); |
530 by (Fast_tac 1); |
530 by (Fast_tac 1); |
531 by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1)); |
531 by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1)); |
532 by (eres_inst_tac [("x","xa")] ballE 1); |
532 by (eres_inst_tac [("x","xa")] ballE 1); |
533 by (fast_tac (!claset addSEs [eqpoll_sym]) 2); |
533 by (fast_tac (claset() addSEs [eqpoll_sym]) 2); |
534 by (etac alt_ex1E 1); |
534 by (etac alt_ex1E 1); |
535 by (dtac spec 1); |
535 by (dtac spec 1); |
536 by (dtac spec 1); |
536 by (dtac spec 1); |
537 by (etac mp 1); |
537 by (etac mp 1); |
538 by (Fast_tac 1); |
538 by (Fast_tac 1); |
577 by (forward_tac [exists_in_MM] 1 THEN REPEAT (assume_tac 1)); |
577 by (forward_tac [exists_in_MM] 1 THEN REPEAT (assume_tac 1)); |
578 by (etac bexE 1); |
578 by (etac bexE 1); |
579 by (res_inst_tac [("x","w Int y")] bexI 1); |
579 by (res_inst_tac [("x","w Int y")] bexI 1); |
580 by (etac Int_in_LL 2); |
580 by (etac Int_in_LL 2); |
581 by (rewtac GG_def); |
581 by (rewtac GG_def); |
582 by (asm_full_simp_tac (!simpset delsimps ball_simps addsimps [Int_in_LL]) 1); |
582 by (asm_full_simp_tac (simpset() delsimps ball_simps addsimps [Int_in_LL]) 1); |
583 by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1 |
583 by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1 |
584 THEN (assume_tac 1)); |
584 THEN (assume_tac 1)); |
585 by (REPEAT (fast_tac (!claset addEs [equals0D] addSEs [Int_in_LL]) 1)); |
585 by (REPEAT (fast_tac (claset() addEs [equals0D] addSEs [Int_in_LL]) 1)); |
586 qed "exists_in_LL"; |
586 qed "exists_in_LL"; |
587 |
587 |
588 goalw thy [LL_def] |
588 goalw thy [LL_def] |
589 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
589 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
590 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
590 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
591 \ v : LL(t_n, k, y) |] \ |
591 \ v : LL(t_n, k, y) |] \ |
592 \ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y"; |
592 \ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y"; |
593 by (fast_tac (!claset addSEs [Int_in_LL, |
593 by (fast_tac (claset() addSEs [Int_in_LL, |
594 unique_superset_in_MM RS the_equality2 RS ssubst]) 1); |
594 unique_superset_in_MM RS the_equality2 RS ssubst]) 1); |
595 qed "in_LL_eq_Int"; |
595 qed "in_LL_eq_Int"; |
596 |
596 |
597 goal thy |
597 goal thy |
598 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
598 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
599 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
599 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
600 \ v : LL(t_n, k, y) |] \ |
600 \ v : LL(t_n, k, y) |] \ |
601 \ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y"; |
601 \ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y"; |
602 by (fast_tac (!claset addSDs [unique_superset_in_MM RS theI RS conjunct1 RS |
602 by (fast_tac (claset() addSDs [unique_superset_in_MM RS theI RS conjunct1 RS |
603 (MM_subset RS subsetD)]) 1); |
603 (MM_subset RS subsetD)]) 1); |
604 qed "the_in_MM_subset"; |
604 qed "the_in_MM_subset"; |
605 |
605 |
606 goalw thy [GG_def] |
606 goalw thy [GG_def] |
607 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
607 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
612 by (dtac in_LL_eq_Int 1 THEN REPEAT (assume_tac 1)); |
612 by (dtac in_LL_eq_Int 1 THEN REPEAT (assume_tac 1)); |
613 by (Asm_full_simp_tac 1); |
613 by (Asm_full_simp_tac 1); |
614 by (rtac subsetI 1); |
614 by (rtac subsetI 1); |
615 by (etac DiffE 1); |
615 by (etac DiffE 1); |
616 by (etac swap 1); |
616 by (etac swap 1); |
617 by (fast_tac (!claset addEs [ssubst]) 1); |
617 by (fast_tac (claset() addEs [ssubst]) 1); |
618 qed "GG_subset"; |
618 qed "GG_subset"; |
619 |
619 |
620 goal thy |
620 goal thy |
621 "!!x. [| well_ord(LL(t_n, succ(k), y), S); \ |
621 "!!x. [| well_ord(LL(t_n, succ(k), y), S); \ |
622 \ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ |
622 \ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ |
665 \ ==> ALL b<ordertype(LL(t_n, succ(k), y), S). \ |
665 \ ==> ALL b<ordertype(LL(t_n, succ(k), y), S). \ |
666 \ (GG(t_n, succ(k), y)) ` \ |
666 \ (GG(t_n, succ(k), y)) ` \ |
667 \ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b) lepoll m"; |
667 \ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b) lepoll m"; |
668 by (rtac oallI 1); |
668 by (rtac oallI 1); |
669 by (asm_full_simp_tac |
669 by (asm_full_simp_tac |
670 (!simpset delsimps ball_simps |
670 (simpset() delsimps ball_simps |
671 addsimps [ltD, |
671 addsimps [ltD, |
672 ordermap_bij RS bij_converse_bij RS |
672 ordermap_bij RS bij_converse_bij RS |
673 bij_is_fun RS apply_type]) 1); |
673 bij_is_fun RS apply_type]) 1); |
674 by (rtac eqpoll_sum_imp_Diff_lepoll 1); |
674 by (rtac eqpoll_sum_imp_Diff_lepoll 1); |
675 by (REPEAT (fast_tac |
675 by (REPEAT (fast_tac |
693 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
693 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
694 by (eres_inst_tac [("x","A Un y")] allE 1); |
694 by (eres_inst_tac [("x","A Un y")] allE 1); |
695 by (forward_tac [infinite_Un] 1 THEN (mp_tac 1)); |
695 by (forward_tac [infinite_Un] 1 THEN (mp_tac 1)); |
696 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
696 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
697 by (resolve_tac [well_ord_LL RS exE] 1 THEN REPEAT (assume_tac 1)); |
697 by (resolve_tac [well_ord_LL RS exE] 1 THEN REPEAT (assume_tac 1)); |
698 by (fast_tac (!claset addSIs [nat_succI, add_type]) 1); |
698 by (fast_tac (claset() addSIs [nat_succI, add_type]) 1); |
699 by (res_inst_tac [("x","ordertype(LL(T, succ(k), y), x)")] exI 1); |
699 by (res_inst_tac [("x","ordertype(LL(T, succ(k), y), x)")] exI 1); |
700 by (res_inst_tac [("x","lam b:ordertype(LL(T, succ(k), y), x). \ |
700 by (res_inst_tac [("x","lam b:ordertype(LL(T, succ(k), y), x). \ |
701 \ (GG(T, succ(k), y)) ` \ |
701 \ (GG(T, succ(k), y)) ` \ |
702 \ (converse(ordermap(LL(T, succ(k), y), x)) ` b)")] exI 1); |
702 \ (converse(ordermap(LL(T, succ(k), y), x)) ` b)")] exI 1); |
703 by (Simp_tac 1); |
703 by (Simp_tac 1); |