1 (* Title: ZF/AC/Cardinal_aux.ML |
1 (* Title: ZF/AC/Cardinal_aux.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 Auxiliary lemmas concerning cardinalities |
5 Auxiliary lemmas concerning cardinalities |
6 *) |
6 *) |
7 |
7 |
8 open Cardinal_aux; |
8 open Cardinal_aux; |
9 |
9 |
10 (* ********************************************************************** *) |
10 (* ********************************************************************** *) |
11 (* Lemmas involving ordinals and cardinalities used in the proofs *) |
11 (* Lemmas involving ordinals and cardinalities used in the proofs *) |
12 (* concerning AC16 and DC *) |
12 (* concerning AC16 and DC *) |
13 (* ********************************************************************** *) |
13 (* ********************************************************************** *) |
14 |
14 |
15 val nat_0_in_2 = Ord_0 RS le_refl RS leI RS ltD; |
15 val nat_0_in_2 = Ord_0 RS le_refl RS leI RS ltD; |
16 |
16 |
17 goalw thy [InfCard_def] "!!i. [| ~Finite(i); Ord(i) |] ==> InfCard(|i|)"; |
17 goalw thy [InfCard_def] "!!i. [| ~Finite(i); Ord(i) |] ==> InfCard(|i|)"; |
18 by (rtac conjI 1); |
18 by (rtac conjI 1); |
19 by (rtac Card_cardinal 1); |
19 by (rtac Card_cardinal 1); |
20 by (resolve_tac [Card_nat RS (Card_def RS def_imp_iff RS iffD1 RS ssubst)] 1); |
20 by (resolve_tac [Card_nat RS (Card_def RS def_imp_iff RS iffD1 RS ssubst)] 1); |
21 by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll |
21 by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll |
22 RSN (2, well_ord_Memrel RS well_ord_lepoll_imp_Card_le)] 1 |
22 RSN (2, well_ord_Memrel RS well_ord_lepoll_imp_Card_le)] 1 |
23 THEN REPEAT (assume_tac 1)); |
23 THEN REPEAT (assume_tac 1)); |
24 val Inf_Ord_imp_InfCard_cardinal = result(); |
24 val Inf_Ord_imp_InfCard_cardinal = result(); |
25 |
25 |
26 goalw thy [lepoll_def] "A Un B lepoll A+B"; |
26 goalw thy [lepoll_def] "A Un B lepoll A+B"; |
27 by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1); |
27 by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1); |
32 by (asm_full_simp_tac (AC_ss addsimps [Inl_def, Inr_def]) 1); |
32 by (asm_full_simp_tac (AC_ss addsimps [Inl_def, Inr_def]) 1); |
33 val Un_lepoll_sum = result(); |
33 val Un_lepoll_sum = result(); |
34 |
34 |
35 goalw thy [sum_def] "A+A = 2*A"; |
35 goalw thy [sum_def] "A+A = 2*A"; |
36 by (fast_tac (AC_cs addIs [equalityI] |
36 by (fast_tac (AC_cs addIs [equalityI] |
37 addSIs [singletonI, nat_0_in_2, succI1] |
37 addSIs [singletonI, nat_0_in_2, succI1] |
38 addSEs [succE, singletonE]) 1); |
38 addSEs [succE, singletonE]) 1); |
39 val sum_eq_2_times = result(); |
39 val sum_eq_2_times = result(); |
40 |
40 |
41 val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll, |
41 val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll, |
42 asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans)) |
42 asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans)) |
43 |> standard; |
43 |> standard; |
44 |
44 |
45 goal thy "!!A. [| A lepoll B; 2 lepoll A |] ==> A+B lepoll A*B"; |
45 goal thy "!!A. [| A lepoll B; 2 lepoll A |] ==> A+B lepoll A*B"; |
46 by (REPEAT (ares_tac [[sum_lepoll_mono, sum_lepoll_prod] |
46 by (REPEAT (ares_tac [[sum_lepoll_mono, sum_lepoll_prod] |
47 MRS lepoll_trans, lepoll_refl] 1)); |
47 MRS lepoll_trans, lepoll_refl] 1)); |
48 val lepoll_imp_sum_lepoll_prod = result(); |
48 val lepoll_imp_sum_lepoll_prod = result(); |
49 |
49 |
50 goal thy "!!A. [| A eqpoll i; B eqpoll i; ~Finite(i); Ord(i) |] \ |
50 goal thy "!!A. [| A eqpoll i; B eqpoll i; ~Finite(i); Ord(i) |] \ |
51 \ ==> A Un B eqpoll i"; |
51 \ ==> A Un B eqpoll i"; |
52 by (rtac eqpollI 1); |
52 by (rtac eqpollI 1); |
53 by (eresolve_tac [subset_imp_lepoll RSN (2, eqpoll_sym RS eqpoll_imp_lepoll |
53 by (eresolve_tac [subset_imp_lepoll RSN (2, eqpoll_sym RS eqpoll_imp_lepoll |
54 RS lepoll_trans)] 2); |
54 RS lepoll_trans)] 2); |
55 by (fast_tac AC_cs 2); |
55 by (fast_tac AC_cs 2); |
56 by (resolve_tac [Un_lepoll_sum RS lepoll_trans] 1); |
56 by (resolve_tac [Un_lepoll_sum RS lepoll_trans] 1); |
57 by (resolve_tac [lepoll_imp_sum_lepoll_prod RS lepoll_trans] 1); |
57 by (resolve_tac [lepoll_imp_sum_lepoll_prod RS lepoll_trans] 1); |
58 by (eresolve_tac [eqpoll_sym RSN (2, eqpoll_trans) RS eqpoll_imp_lepoll] 1 |
58 by (eresolve_tac [eqpoll_sym RSN (2, eqpoll_trans) RS eqpoll_imp_lepoll] 1 |
59 THEN (assume_tac 1)); |
59 THEN (assume_tac 1)); |
60 by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll RS |
60 by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll RS |
61 (Ord_nat RS (nat_2I RS OrdmemD) RS subset_imp_lepoll RS lepoll_trans) |
61 (Ord_nat RS (nat_2I RS OrdmemD) RS subset_imp_lepoll RS lepoll_trans) |
62 RS (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans))] 1 |
62 RS (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans))] 1 |
63 THEN (REPEAT (assume_tac 1))); |
63 THEN (REPEAT (assume_tac 1))); |
64 by (eresolve_tac [prod_eqpoll_cong RS eqpoll_imp_lepoll RS lepoll_trans] 1 |
64 by (eresolve_tac [prod_eqpoll_cong RS eqpoll_imp_lepoll RS lepoll_trans] 1 |
65 THEN (assume_tac 1)); |
65 THEN (assume_tac 1)); |
66 by (resolve_tac [Inf_Ord_imp_InfCard_cardinal RSN (2, well_ord_Memrel RS |
66 by (resolve_tac [Inf_Ord_imp_InfCard_cardinal RSN (2, well_ord_Memrel RS |
67 well_ord_InfCard_square_eq) RS eqpoll_imp_lepoll] 1 |
67 well_ord_InfCard_square_eq) RS eqpoll_imp_lepoll] 1 |
68 THEN REPEAT (assume_tac 1)); |
68 THEN REPEAT (assume_tac 1)); |
69 val Un_eqpoll_Inf_Ord = result(); |
69 val Un_eqpoll_Inf_Ord = result(); |
70 |
70 |
71 goalw thy [lepoll_def] "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |] \ |
71 goalw thy [lepoll_def] "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |] \ |
72 \ ==> A Un C lepoll B Un D"; |
72 \ ==> A Un C lepoll B Un D"; |
73 by (REPEAT (etac exE 1)); |
73 by (REPEAT (etac exE 1)); |
74 by (res_inst_tac [("x","lam a: A Un C. if(a:A, f`a, fa`a)")] exI 1); |
74 by (res_inst_tac [("x","lam a: A Un C. if(a:A, f`a, fa`a)")] exI 1); |
75 by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(fa)`z)")] |
75 by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(fa)`z)")] |
76 lam_injective 1); |
76 lam_injective 1); |
77 by (split_tac [expand_if] 1); |
77 by (split_tac [expand_if] 1); |
78 by (etac UnE 1); |
78 by (etac UnE 1); |
79 by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); |
79 by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); |
80 by (rtac conjI 1); |
80 by (rtac conjI 1); |
81 by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); |
81 by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); |
82 by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] addSIs [UnI2]) 1); |
82 by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] addSIs [UnI2]) 1); |
83 by (REPEAT (split_tac [expand_if] 1)); |
83 by (REPEAT (split_tac [expand_if] 1)); |
84 by (rtac conjI 1); |
84 by (rtac conjI 1); |
85 by (fast_tac (AC_cs addSEs [left_inverse, inj_is_fun RS apply_type] |
85 by (fast_tac (AC_cs addSEs [left_inverse, inj_is_fun RS apply_type] |
86 addEs [swap]) 1); |
86 addEs [swap]) 1); |
87 by (rtac impI 1); |
87 by (rtac impI 1); |
88 by (etac UnE 1); |
88 by (etac UnE 1); |
89 by (contr_tac 1); |
89 by (contr_tac 1); |
90 by (rtac conjI 1); |
90 by (rtac conjI 1); |
91 by (rtac impI 1); |
91 by (rtac impI 1); |
100 |
100 |
101 goal ZF.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y"; |
101 goal ZF.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y"; |
102 by (split_tac [expand_if] 1); |
102 by (split_tac [expand_if] 1); |
103 by (asm_full_simp_tac (ZF_ss addsimps [double_Diff_sing, Diff_eq_0_iff]) 1); |
103 by (asm_full_simp_tac (ZF_ss addsimps [double_Diff_sing, Diff_eq_0_iff]) 1); |
104 by (fast_tac (ZF_cs addSIs [the_equality, equalityI, equals0I] |
104 by (fast_tac (ZF_cs addSIs [the_equality, equalityI, equals0I] |
105 addEs [equalityE] addSEs [singletonE]) 1); |
105 addEs [equalityE] addSEs [singletonE]) 1); |
106 val paired_bij_lemma = result(); |
106 val paired_bij_lemma = result(); |
107 |
107 |
108 goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w})) \ |
108 goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w})) \ |
109 \ : bij({{y,z}. y:x}, x)"; |
109 \ : bij({{y,z}. y:x}, x)"; |
110 by (res_inst_tac [("d","%a. {a,z}")] lam_bijective 1); |
110 by (res_inst_tac [("d","%a. {a,z}")] lam_bijective 1); |
111 by (TRYALL (fast_tac (AC_cs addSEs [RepFunE] addSIs [RepFunI] |
111 by (TRYALL (fast_tac (AC_cs addSEs [RepFunE] addSIs [RepFunI] |
112 addss (AC_ss addsimps [paired_bij_lemma])))); |
112 addss (AC_ss addsimps [paired_bij_lemma])))); |
113 val paired_bij = result(); |
113 val paired_bij = result(); |
114 |
114 |
115 goalw thy [eqpoll_def] "{{y,z}. y:x} eqpoll x"; |
115 goalw thy [eqpoll_def] "{{y,z}. y:x} eqpoll x"; |
116 by (fast_tac (AC_cs addSIs [paired_bij]) 1); |
116 by (fast_tac (AC_cs addSIs [paired_bij]) 1); |
117 val paired_eqpoll = result(); |
117 val paired_eqpoll = result(); |
119 goal thy "!!A. EX B. B eqpoll A & B Int C = 0"; |
119 goal thy "!!A. EX B. B eqpoll A & B Int C = 0"; |
120 by (fast_tac (AC_cs addSIs [paired_eqpoll, equals0I] addEs [mem_asym]) 1); |
120 by (fast_tac (AC_cs addSIs [paired_eqpoll, equals0I] addEs [mem_asym]) 1); |
121 val ex_eqpoll_disjoint = result(); |
121 val ex_eqpoll_disjoint = result(); |
122 |
122 |
123 goal thy "!!A. [| A lepoll i; B lepoll i; ~Finite(i); Ord(i) |] \ |
123 goal thy "!!A. [| A lepoll i; B lepoll i; ~Finite(i); Ord(i) |] \ |
124 \ ==> A Un B lepoll i"; |
124 \ ==> A Un B lepoll i"; |
125 by (res_inst_tac [("A1","i"), ("C1","i")] (ex_eqpoll_disjoint RS exE) 1); |
125 by (res_inst_tac [("A1","i"), ("C1","i")] (ex_eqpoll_disjoint RS exE) 1); |
126 by (etac conjE 1); |
126 by (etac conjE 1); |
127 by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans)] 1); |
127 by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans)] 1); |
128 by (assume_tac 1); |
128 by (assume_tac 1); |
129 by (resolve_tac [Un_lepoll_Un RS lepoll_trans] 1 THEN (REPEAT (assume_tac 1))); |
129 by (resolve_tac [Un_lepoll_Un RS lepoll_trans] 1 THEN (REPEAT (assume_tac 1))); |
130 by (eresolve_tac [eqpoll_refl RSN (2, Un_eqpoll_Inf_Ord) RS |
130 by (eresolve_tac [eqpoll_refl RSN (2, Un_eqpoll_Inf_Ord) RS |
131 eqpoll_imp_lepoll] 1 |
131 eqpoll_imp_lepoll] 1 |
132 THEN (REPEAT (assume_tac 1))); |
132 THEN (REPEAT (assume_tac 1))); |
133 val Un_lepoll_Inf_Ord = result(); |
133 val Un_lepoll_Inf_Ord = result(); |
134 |
134 |
135 goal thy "!!P. [| P(i); i:j; Ord(j) |] ==> (LEAST i. P(i)) : j"; |
135 goal thy "!!P. [| P(i); i:j; Ord(j) |] ==> (LEAST i. P(i)) : j"; |
136 by (eresolve_tac [Least_le RS leE] 1); |
136 by (eresolve_tac [Least_le RS leE] 1); |
137 by (etac Ord_in_Ord 1 THEN (assume_tac 1)); |
137 by (etac Ord_in_Ord 1 THEN (assume_tac 1)); |
139 by (fast_tac (AC_cs addDs [OrdmemD]) 1); |
139 by (fast_tac (AC_cs addDs [OrdmemD]) 1); |
140 by (etac subst_elem 1 THEN (assume_tac 1)); |
140 by (etac subst_elem 1 THEN (assume_tac 1)); |
141 val Least_in_Ord = result(); |
141 val Least_in_Ord = result(); |
142 |
142 |
143 goal thy "!!x. [| well_ord(x,r); y<=x; y lepoll succ(n); n:nat |] \ |
143 goal thy "!!x. [| well_ord(x,r); y<=x; y lepoll succ(n); n:nat |] \ |
144 \ ==> y-{THE b. first(b,y,r)} lepoll n"; |
144 \ ==> y-{THE b. first(b,y,r)} lepoll n"; |
145 by (res_inst_tac [("Q","y=0")] (excluded_middle RS disjE) 1); |
145 by (res_inst_tac [("Q","y=0")] (excluded_middle RS disjE) 1); |
146 by (fast_tac (AC_cs addSIs [Diff_sing_lepoll, the_first_in]) 1); |
146 by (fast_tac (AC_cs addSIs [Diff_sing_lepoll, the_first_in]) 1); |
147 by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1); |
147 by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1); |
148 by (rtac empty_lepollI 2); |
148 by (rtac empty_lepollI 2); |
149 by (fast_tac (AC_cs addSIs [equalityI]) 1); |
149 by (fast_tac (AC_cs addSIs [equalityI]) 1); |
181 by (rtac Un_lepoll_Inf_Ord 1 THEN (REPEAT_FIRST assume_tac)); |
181 by (rtac Un_lepoll_Inf_Ord 1 THEN (REPEAT_FIRST assume_tac)); |
182 by (etac UN_sing_lepoll 1); |
182 by (etac UN_sing_lepoll 1); |
183 val UN_fun_lepoll_lemma = result(); |
183 val UN_fun_lepoll_lemma = result(); |
184 |
184 |
185 goal thy "!!a f. [| ALL b:a. f`b lepoll n & f`b <= T; well_ord(T, R); \ |
185 goal thy "!!a f. [| ALL b:a. f`b lepoll n & f`b <= T; well_ord(T, R); \ |
186 \ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. f`b) lepoll a"; |
186 \ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. f`b) lepoll a"; |
187 by (eresolve_tac [UN_fun_lepoll_lemma RS allE] 1 THEN (REPEAT (assume_tac 1))); |
187 by (eresolve_tac [UN_fun_lepoll_lemma RS allE] 1 THEN (REPEAT (assume_tac 1))); |
188 by (fast_tac AC_cs 1); |
188 by (fast_tac AC_cs 1); |
189 val UN_fun_lepoll = result(); |
189 val UN_fun_lepoll = result(); |
190 |
190 |
191 goal thy "!!a f. [| ALL b:a. F(b) lepoll n & F(b) <= T; well_ord(T, R); \ |
191 goal thy "!!a f. [| ALL b:a. F(b) lepoll n & F(b) <= T; well_ord(T, R); \ |
192 \ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. F(b)) lepoll a"; |
192 \ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. F(b)) lepoll a"; |
193 by (rtac impE 1 THEN (assume_tac 3)); |
193 by (rtac impE 1 THEN (assume_tac 3)); |
194 by (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2 |
194 by (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2 |
195 THEN (TRYALL assume_tac)); |
195 THEN (TRYALL assume_tac)); |
196 by (simp_tac AC_ss 2); |
196 by (simp_tac AC_ss 2); |
197 by (asm_full_simp_tac AC_ss 1); |
197 by (asm_full_simp_tac AC_ss 1); |
198 val UN_lepoll = result(); |
198 val UN_lepoll = result(); |
199 |
199 |
200 goal thy "!!a. Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))"; |
200 goal thy "!!a. Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))"; |
221 by (TRYALL (asm_simp_tac sum_ss)); |
221 by (TRYALL (asm_simp_tac sum_ss)); |
222 by (fast_tac (AC_cs addDs [equals0D]) 1); |
222 by (fast_tac (AC_cs addDs [equals0D]) 1); |
223 val disj_Un_eqpoll_sum = result(); |
223 val disj_Un_eqpoll_sum = result(); |
224 |
224 |
225 goalw thy [lepoll_def, eqpoll_def] |
225 goalw thy [lepoll_def, eqpoll_def] |
226 "!!X a. a lepoll X ==> EX Y. Y<=X & a eqpoll Y"; |
226 "!!X a. a lepoll X ==> EX Y. Y<=X & a eqpoll Y"; |
227 by (etac exE 1); |
227 by (etac exE 1); |
228 by (forward_tac [subset_refl RSN (2, restrict_bij)] 1); |
228 by (forward_tac [subset_refl RSN (2, restrict_bij)] 1); |
229 by (res_inst_tac [("x","f``a")] exI 1); |
229 by (res_inst_tac [("x","f``a")] exI 1); |
230 by (fast_tac (AC_cs addSEs [inj_is_fun RS fun_is_rel RS image_subset]) 1); |
230 by (fast_tac (AC_cs addSEs [inj_is_fun RS fun_is_rel RS image_subset]) 1); |
231 val lepoll_imp_eqpoll_subset = result(); |
231 val lepoll_imp_eqpoll_subset = result(); |
232 |
232 |
233 (* ********************************************************************** *) |
233 (* ********************************************************************** *) |
234 (* Some other lemmas *) |
234 (* Some other lemmas *) |
235 (* ********************************************************************** *) |
235 (* ********************************************************************** *) |
236 |
236 |
237 goal thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; |
237 goal thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; |
238 by (rtac eqpoll_trans 1); |
238 by (rtac eqpoll_trans 1); |
239 by (eresolve_tac [nat_implies_well_ord RS ( |
239 by (eresolve_tac [nat_implies_well_ord RS ( |
243 by (eresolve_tac [nat_cadd_eq_add RS subst] 1 THEN (assume_tac 1)); |
243 by (eresolve_tac [nat_cadd_eq_add RS subst] 1 THEN (assume_tac 1)); |
244 by (asm_full_simp_tac (AC_ss addsimps [cadd_def, eqpoll_refl]) 1); |
244 by (asm_full_simp_tac (AC_ss addsimps [cadd_def, eqpoll_refl]) 1); |
245 val nat_sum_eqpoll_sum = result(); |
245 val nat_sum_eqpoll_sum = result(); |
246 |
246 |
247 val eqpoll_ordertype = |
247 val eqpoll_ordertype = |
248 ordermap_bij RS (exI RS (eqpoll_def RS (def_imp_iff RS iffD2))); |
248 ordermap_bij RS (exI RS (eqpoll_def RS (def_imp_iff RS iffD2))); |
249 |
249 |
250 goalw thy [lesspoll_def] |
250 goalw thy [lesspoll_def] |
251 "!!a. [| b lesspoll a; well_ord(a,r); well_ord(b,s) |] \ |
251 "!!a. [| b lesspoll a; well_ord(a,r); well_ord(b,s) |] \ |
252 \ ==> ordertype(b,s) < ordertype(a,r)"; |
252 \ ==> ordertype(b,s) < ordertype(a,r)"; |
253 by (forw_inst_tac [("A2","b")] |
253 by (forw_inst_tac [("A2","b")] |
254 ([Ord_ordertype, Ord_ordertype] MRS Ord_linear) 1 |
254 ([Ord_ordertype, Ord_ordertype] MRS Ord_linear) 1 |
255 THEN REPEAT (assume_tac 1)); |
255 THEN REPEAT (assume_tac 1)); |
256 by (etac disjE 1); |
256 by (etac disjE 1); |
257 by (etac ltI 1); |
257 by (etac ltI 1); |
258 by (etac Ord_ordertype 1); |
258 by (etac Ord_ordertype 1); |
259 by (etac disjE 1); |
259 by (etac disjE 1); |
260 by (REPEAT (eresolve_tac [conjE,notE] 1)); |
260 by (REPEAT (eresolve_tac [conjE,notE] 1)); |
274 goalw thy [lesspoll_def] "!!A. A lesspoll B ==> A lepoll B"; |
274 goalw thy [lesspoll_def] "!!A. A lesspoll B ==> A lepoll B"; |
275 by (fast_tac AC_cs 1); |
275 by (fast_tac AC_cs 1); |
276 val lesspoll_imp_lepoll = result(); |
276 val lesspoll_imp_lepoll = result(); |
277 |
277 |
278 goalw thy [lepoll_def] |
278 goalw thy [lepoll_def] |
279 "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)"; |
279 "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)"; |
280 by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1); |
280 by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1); |
281 val lepoll_well_ord = result(); |
281 val lepoll_well_ord = result(); |
282 |
282 |
283 goal thy "!!A a. [| A lesspoll a; Ord(a) |] ==> EX b. b<a & A eqpoll b"; |
283 goal thy "!!A a. [| A lesspoll a; Ord(a) |] ==> EX b. b<a & A eqpoll b"; |
284 by (resolve_tac [well_ord_Memrel RSN (2, |
284 by (resolve_tac [well_ord_Memrel RSN (2, |
285 lesspoll_imp_lepoll RS lepoll_well_ord) RS exE] 1 |
285 lesspoll_imp_lepoll RS lepoll_well_ord) RS exE] 1 |
286 THEN (REPEAT (assume_tac 1))); |
286 THEN (REPEAT (assume_tac 1))); |
287 by (dresolve_tac [well_ord_Memrel RSN (2, lesspoll_ordertype_lt)] 1 |
287 by (dresolve_tac [well_ord_Memrel RSN (2, lesspoll_ordertype_lt)] 1 |
288 THEN (REPEAT (assume_tac 1))); |
288 THEN (REPEAT (assume_tac 1))); |
289 by (fast_tac (AC_cs addSEs [eqpoll_ordertype] |
289 by (fast_tac (AC_cs addSEs [eqpoll_ordertype] |
290 addEs [ordertype_Memrel RS subst]) 1); |
290 addEs [ordertype_Memrel RS subst]) 1); |
291 val lesspoll_imp_ex_lt_eqpoll = result(); |
291 val lesspoll_imp_ex_lt_eqpoll = result(); |
292 |
292 |
293 goalw thy [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B"; |
293 goalw thy [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B"; |
294 by (fast_tac (AC_cs addSIs [eqpollI] addSEs [eqpollE]) 1); |
294 by (fast_tac (AC_cs addSIs [eqpollI] addSEs [eqpollE]) 1); |
295 val lepoll_iff_leqpoll = result(); |
295 val lepoll_iff_leqpoll = result(); |
300 by (fast_tac (AC_cs addSIs [le_refl]) 1); |
300 by (fast_tac (AC_cs addSIs [le_refl]) 1); |
301 val lepoll_imp_ex_le_eqpoll = result(); |
301 val lepoll_imp_ex_le_eqpoll = result(); |
302 |
302 |
303 goal thy "!!m. [| m le n; n:nat |] ==> m:nat"; |
303 goal thy "!!m. [| m le n; n:nat |] ==> m:nat"; |
304 by (fast_tac (AC_cs addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))] |
304 by (fast_tac (AC_cs addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))] |
305 addSEs [ltE]) 1); |
305 addSEs [ltE]) 1); |
306 val le_in_nat = result(); |
306 val le_in_nat = result(); |
307 |
307 |
308 goalw thy [Finite_def] "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)"; |
308 goalw thy [Finite_def] "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)"; |
309 by (REPEAT (etac bexE 1)); |
309 by (REPEAT (etac bexE 1)); |
310 by (REPEAT (dtac eqpoll_imp_lepoll 1)); |
310 by (REPEAT (dtac eqpoll_imp_lepoll 1)); |
311 by (dtac sum_lepoll_mono 1 THEN (assume_tac 1)); |
311 by (dtac sum_lepoll_mono 1 THEN (assume_tac 1)); |
312 by (dresolve_tac [nat_sum_eqpoll_sum RS eqpoll_imp_lepoll RSN (2, |
312 by (dresolve_tac [nat_sum_eqpoll_sum RS eqpoll_imp_lepoll RSN (2, |
313 Un_lepoll_sum RS lepoll_trans RS lepoll_trans)] 1 |
313 Un_lepoll_sum RS lepoll_trans RS lepoll_trans)] 1 |
314 THEN (REPEAT (assume_tac 1))); |
314 THEN (REPEAT (assume_tac 1))); |
315 by (forw_inst_tac [("n2","na")] |
315 by (forw_inst_tac [("n2","na")] |
316 (add_type RS nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll)) 1 |
316 (add_type RS nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll)) 1 |
317 THEN (REPEAT (assume_tac 1))); |
317 THEN (REPEAT (assume_tac 1))); |
318 by (fast_tac (AC_cs addSEs [add_type RSN (2, le_in_nat)]) 1); |
318 by (fast_tac (AC_cs addSEs [add_type RSN (2, le_in_nat)]) 1); |
319 val Finite_Un = result(); |
319 val Finite_Un = result(); |
320 |
320 |
321 goal thy "A <= B Un (A - B)"; |
321 goal thy "A <= B Un (A - B)"; |
322 by (fast_tac AC_cs 1); |
322 by (fast_tac AC_cs 1); |
326 by (dresolve_tac [Card_iff_initial RS iffD1] 1); |
326 by (dresolve_tac [Card_iff_initial RS iffD1] 1); |
327 by (fast_tac (AC_cs addSEs [leI RS le_imp_lepoll]) 1); |
327 by (fast_tac (AC_cs addSEs [leI RS le_imp_lepoll]) 1); |
328 val lt_Card_imp_lesspoll = result(); |
328 val lt_Card_imp_lesspoll = result(); |
329 |
329 |
330 (* ********************************************************************** *) |
330 (* ********************************************************************** *) |
331 (* Diff_lesspoll_eqpoll_Card *) |
331 (* Diff_lesspoll_eqpoll_Card *) |
332 (* ********************************************************************** *) |
332 (* ********************************************************************** *) |
333 |
333 |
334 goal thy "!!A B. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a; \ |
334 goal thy "!!A B. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a; \ |
335 \ A-B lesspoll a |] ==> P"; |
335 \ A-B lesspoll a |] ==> P"; |
336 by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE, |
336 by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE, |
337 Card_is_Ord, conjE] 1)); |
337 Card_is_Ord, conjE] 1)); |
338 by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper1_le))) 1 |
338 by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper1_le))) 1 |
339 THEN (assume_tac 1)); |
339 THEN (assume_tac 1)); |
340 by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper2_le))) 1 |
340 by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper2_le))) 1 |
341 THEN (assume_tac 1)); |
341 THEN (assume_tac 1)); |
342 by (dtac Un_least_lt 1 THEN (assume_tac 1)); |
342 by (dtac Un_least_lt 1 THEN (assume_tac 1)); |
343 by (dresolve_tac [le_imp_lepoll RSN |
343 by (dresolve_tac [le_imp_lepoll RSN |
344 (2, eqpoll_imp_lepoll RS lepoll_trans)] 1 |
344 (2, eqpoll_imp_lepoll RS lepoll_trans)] 1 |
345 THEN (assume_tac 1)); |
345 THEN (assume_tac 1)); |
346 by (dresolve_tac [le_imp_lepoll RSN |
346 by (dresolve_tac [le_imp_lepoll RSN |
347 (2, eqpoll_imp_lepoll RS lepoll_trans)] 1 |
347 (2, eqpoll_imp_lepoll RS lepoll_trans)] 1 |
348 THEN (assume_tac 1)); |
348 THEN (assume_tac 1)); |
349 by (res_inst_tac [("Q","Finite(x Un xa)")] (excluded_middle RS disjE) 1); |
349 by (res_inst_tac [("Q","Finite(x Un xa)")] (excluded_middle RS disjE) 1); |
350 by (dresolve_tac [[lepoll_Finite, lepoll_Finite] MRS Finite_Un] 2 |
350 by (dresolve_tac [[lepoll_Finite, lepoll_Finite] MRS Finite_Un] 2 |
351 THEN (REPEAT (assume_tac 2))); |
351 THEN (REPEAT (assume_tac 2))); |
352 by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_Finite] 2); |
352 by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_Finite] 2); |
353 by (fast_tac (AC_cs |
353 by (fast_tac (AC_cs |
354 addDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite]) 2); |
354 addDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite]) 2); |
355 by (dresolve_tac [ Un_lepoll_Inf_Ord] 1 |
355 by (dresolve_tac [ Un_lepoll_Inf_Ord] 1 |
356 THEN (REPEAT (assume_tac 1))); |
356 THEN (REPEAT (assume_tac 1))); |
357 by (fast_tac (AC_cs addSEs [ltE, Ord_in_Ord]) 1); |
357 by (fast_tac (AC_cs addSEs [ltE, Ord_in_Ord]) 1); |
358 by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RSN |
358 by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RSN |
359 (3, lt_Card_imp_lesspoll RS lepoll_lesspoll_lesspoll)] 1 |
359 (3, lt_Card_imp_lesspoll RS lepoll_lesspoll_lesspoll)] 1 |
360 THEN (TRYALL assume_tac)); |
360 THEN (TRYALL assume_tac)); |
361 by (fast_tac (AC_cs addSDs [lesspoll_def RS def_imp_iff RS iffD1]) 1); |
361 by (fast_tac (AC_cs addSDs [lesspoll_def RS def_imp_iff RS iffD1]) 1); |
362 val Diff_lesspoll_eqpoll_Card_lemma = result(); |
362 val Diff_lesspoll_eqpoll_Card_lemma = result(); |
363 |
363 |
364 goal thy "!!A. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a |] \ |
364 goal thy "!!A. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a |] \ |
365 \ ==> A - B eqpoll a"; |
365 \ ==> A - B eqpoll a"; |
366 by (rtac swap 1 THEN (fast_tac AC_cs 1)); |
366 by (rtac swap 1 THEN (fast_tac AC_cs 1)); |
367 by (rtac Diff_lesspoll_eqpoll_Card_lemma 1 THEN (REPEAT (assume_tac 1))); |
367 by (rtac Diff_lesspoll_eqpoll_Card_lemma 1 THEN (REPEAT (assume_tac 1))); |
368 by (fast_tac (AC_cs addSIs [lesspoll_def RS def_imp_iff RS iffD2, |
368 by (fast_tac (AC_cs addSIs [lesspoll_def RS def_imp_iff RS iffD2, |
369 subset_imp_lepoll RS (eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1); |
369 subset_imp_lepoll RS (eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1); |
370 val Diff_lesspoll_eqpoll_Card = result(); |
370 val Diff_lesspoll_eqpoll_Card = result(); |
371 |
371 |