1 (* Title: ZF/AC/AC16_WO4.ML |
1 (* Title: ZF/AC/AC16_WO4.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 The proof of AC16(n, k) ==> WO4(n-k) |
5 The proof of AC16(n, k) ==> WO4(n-k) |
6 *) |
6 *) |
7 |
7 |
8 open AC16_WO4; |
8 open AC16_WO4; |
9 |
9 |
10 (* ********************************************************************** *) |
10 (* ********************************************************************** *) |
11 (* The case of finite set *) |
11 (* The case of finite set *) |
12 (* ********************************************************************** *) |
12 (* ********************************************************************** *) |
13 |
13 |
14 goalw thy [Finite_def] "!!A. [| Finite(A); 0<m; m:nat |] ==> \ |
14 goalw thy [Finite_def] "!!A. [| Finite(A); 0<m; m:nat |] ==> \ |
15 \ EX a f. Ord(a) & domain(f) = a & \ |
15 \ EX a f. Ord(a) & domain(f) = a & \ |
16 \ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"; |
16 \ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"; |
17 by (etac bexE 1); |
17 by (etac bexE 1); |
18 by (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1); |
18 by (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1); |
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 AC_ss 1); |
22 by (asm_full_simp_tac AC_ss 1); |
23 by (rewrite_goals_tac [bij_def, surj_def]); |
23 by (rewrite_goals_tac [bij_def, surj_def]); |
24 by (fast_tac (AC_cs addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun, |
24 by (fast_tac (AC_cs 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 [singletonE, apply_type, ltE]) 1); |
27 addSEs [singletonE, apply_type, ltE]) 1); |
28 val lemma1 = result(); |
28 val lemma1 = result(); |
29 |
29 |
30 (* ********************************************************************** *) |
30 (* ********************************************************************** *) |
31 (* The case of infinite set *) |
31 (* The case of infinite set *) |
32 (* ********************************************************************** *) |
32 (* ********************************************************************** *) |
33 |
33 |
34 goal thy "!!x. well_ord(x,r) ==> well_ord({{y,z}. y:x},?s(x,z))"; |
34 goal thy "!!x. well_ord(x,r) ==> well_ord({{y,z}. y:x},?s(x,z))"; |
35 by (eresolve_tac [paired_bij RS bij_is_inj RS well_ord_rvimage] 1); |
35 by (eresolve_tac [paired_bij RS bij_is_inj RS well_ord_rvimage] 1); |
36 val well_ord_paired = uresult(); |
36 val well_ord_paired = uresult(); |
38 goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C"; |
38 goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C"; |
39 by (fast_tac (FOL_cs addEs [notE, lepoll_trans]) 1); |
39 by (fast_tac (FOL_cs addEs [notE, lepoll_trans]) 1); |
40 val lepoll_trans1 = result(); |
40 val lepoll_trans1 = result(); |
41 |
41 |
42 goalw thy [lepoll_def] |
42 goalw thy [lepoll_def] |
43 "!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)"; |
43 "!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)"; |
44 by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1); |
44 by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1); |
45 val well_ord_lepoll = result(); |
45 val well_ord_lepoll = result(); |
46 |
46 |
47 goal thy "!!X. [| well_ord(X,R); well_ord(Y,S) \ |
47 goal thy "!!X. [| well_ord(X,R); well_ord(Y,S) \ |
48 \ |] ==> EX T. well_ord(X Un Y, T)"; |
48 \ |] ==> EX T. well_ord(X Un Y, T)"; |
49 by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS well_ord_lepoll)] 1); |
49 by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS well_ord_lepoll)] 1); |
50 by (assume_tac 1); |
50 by (assume_tac 1); |
51 val well_ord_Un = result(); |
51 val well_ord_Un = result(); |
52 |
52 |
53 (* ********************************************************************** *) |
53 (* ********************************************************************** *) |
54 (* There exists a well ordered set y such that ... *) |
54 (* There exists a well ordered set y such that ... *) |
55 (* ********************************************************************** *) |
55 (* ********************************************************************** *) |
56 |
56 |
57 goal thy "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)"; |
57 goal thy "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)"; |
58 by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1); |
58 by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1); |
59 by (resolve_tac [Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS |
59 by (resolve_tac [Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS |
60 well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); |
60 well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); |
61 by (fast_tac (AC_cs addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, |
61 by (fast_tac (AC_cs addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, |
62 equals0I, HartogI RSN (2, lepoll_trans1), |
62 equals0I, HartogI RSN (2, lepoll_trans1), |
63 subset_imp_lepoll RS (paired_eqpoll RS eqpoll_sym RS |
63 subset_imp_lepoll RS (paired_eqpoll RS eqpoll_sym RS |
64 eqpoll_imp_lepoll RSN (2, lepoll_trans))] |
64 eqpoll_imp_lepoll RSN (2, lepoll_trans))] |
65 addSEs [RepFunE, nat_not_Finite RS notE] addEs [mem_asym] |
65 addSEs [RepFunE, nat_not_Finite RS notE] addEs [mem_asym] |
66 addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite, |
66 addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite, |
67 paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
67 paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
68 RS lepoll_Finite]) 1); |
68 RS lepoll_Finite]) 1); |
69 val lemma2 = result(); |
69 val lemma2 = result(); |
70 |
70 |
71 val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)"; |
71 val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)"; |
72 by (fast_tac (AC_cs |
72 by (fast_tac (AC_cs |
73 addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1); |
73 addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1); |
74 val infinite_Un = result(); |
74 val infinite_Un = result(); |
75 |
75 |
76 (* ********************************************************************** *) |
76 (* ********************************************************************** *) |
77 (* There is a v : s_u such that k lepoll x Int y (in our case succ(k)) *) |
77 (* There is a v : s_u such that k lepoll x Int y (in our case succ(k)) *) |
78 (* The idea of the proof is the following : *) |
78 (* The idea of the proof is the following : *) |
79 (* Suppose not, i.e. every element of s_u has exactly k-1 elements of y *) |
79 (* Suppose not, i.e. every element of s_u has exactly k-1 elements of y *) |
80 (* Thence y is less than or equipollent to {v:Pow(x). v eqpoll n#-k} *) |
80 (* Thence y is less than or equipollent to {v:Pow(x). v eqpoll n#-k} *) |
81 (* We have obtained this result in two steps : *) |
81 (* We have obtained this result in two steps : *) |
82 (* 1. y is less than or equipollent to {v:s_u. a <= v} *) |
82 (* 1. y is less than or equipollent to {v:s_u. a <= v} *) |
83 (* where a is certain k-2 element subset of y *) |
83 (* where a is certain k-2 element subset of y *) |
84 (* 2. {v:s_u. a <= v} is less than or equipollent *) |
84 (* 2. {v:s_u. a <= v} is less than or equipollent *) |
85 (* to {v:Pow(x). v eqpoll n-k} *) |
85 (* to {v:Pow(x). v eqpoll n-k} *) |
86 (* ********************************************************************** *) |
86 (* ********************************************************************** *) |
87 |
87 |
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 (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] |
91 by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] |
92 addIs [expand_if RS iffD2]) 1); |
92 addIs [expand_if RS iffD2]) 1); |
93 by (REPEAT (split_tac [expand_if] 1)); |
93 by (REPEAT (split_tac [expand_if] 1)); |
94 by (fast_tac (AC_cs addSEs [left_inverse]) 1); |
94 by (fast_tac (AC_cs addSEs [left_inverse]) 1); |
95 val succ_not_lepoll_lemma = result(); |
95 val succ_not_lepoll_lemma = result(); |
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 (AC_cs addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |
99 by (fast_tac (AC_cs addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |
100 val succ_not_lepoll_imp_eqpoll = result(); |
100 val succ_not_lepoll_imp_eqpoll = result(); |
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"; |
105 by (excluded_middle_tac "?P" 1 THEN (assume_tac 2)); |
105 by (excluded_middle_tac "?P" 1 THEN (assume_tac 2)); |
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 (AC_cs addSEs [succ_not_lepoll_imp_eqpoll]) 1); |
111 by (fast_tac (AC_cs addSEs [succ_not_lepoll_imp_eqpoll]) 1); |
112 val suppose_not = result(); |
112 val suppose_not = result(); |
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 (* ********************************************************************** *) |
117 |
117 |
118 goalw thy [lepoll_def, eqpoll_def] |
118 goalw thy [lepoll_def, eqpoll_def] |
119 "!!X. [| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y"; |
119 "!!X. [| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y"; |
120 by (fast_tac (FOL_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)] |
120 by (fast_tac (FOL_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)] |
121 addSIs [subset_refl] |
121 addSIs [subset_refl] |
122 addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1); |
122 addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1); |
123 val nat_lepoll_imp_ex_eqpoll_n = result(); |
123 val nat_lepoll_imp_ex_eqpoll_n = result(); |
124 |
124 |
125 val ordertype_eqpoll = |
125 val ordertype_eqpoll = |
126 ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2)); |
126 ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2)); |
127 |
127 |
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 (AC_cs addSIs [nat_le_infinite_Ord RS le_imp_lepoll] |
133 by (fast_tac (AC_cs 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 val ex_subset_eqpoll_n = result(); |
136 val ex_subset_eqpoll_n = result(); |
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 (AC_cs addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll, |
139 by (fast_tac (AC_cs 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 val n_lesspoll_nat = result(); |
143 val n_lesspoll_nat = result(); |
144 |
144 |
145 goal thy "!!y. [| well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; k: nat |] \ |
145 goal thy "!!y. [| well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; k: nat |] \ |
146 \ ==> y - a eqpoll y"; |
146 \ ==> y - a eqpoll y"; |
147 by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll] |
147 by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll] |
148 addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans, |
148 addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans, |
149 Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord |
149 Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord |
150 RS le_imp_lepoll] |
150 RS le_imp_lepoll] |
151 addSEs [well_ord_cardinal_eqpoll, |
151 addSEs [well_ord_cardinal_eqpoll, |
152 well_ord_cardinal_eqpoll RS eqpoll_sym, |
152 well_ord_cardinal_eqpoll RS eqpoll_sym, |
153 eqpoll_sym RS eqpoll_imp_lepoll, |
153 eqpoll_sym RS eqpoll_imp_lepoll, |
154 n_lesspoll_nat RS lesspoll_lepoll_lesspoll, |
154 n_lesspoll_nat RS lesspoll_lepoll_lesspoll, |
155 well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
155 well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
156 RS lepoll_infinite]) 1); |
156 RS lepoll_infinite]) 1); |
157 val Diff_Finite_eqpoll = result(); |
157 val Diff_Finite_eqpoll = result(); |
158 |
158 |
159 goal thy "!!x. [| a<=y; b:y-a; u:x |] ==> cons(b, cons(u, a)) : Pow(x Un y)"; |
159 goal thy "!!x. [| a<=y; b:y-a; u:x |] ==> cons(b, cons(u, a)) : Pow(x Un y)"; |
160 by (fast_tac AC_cs 1); |
160 by (fast_tac AC_cs 1); |
161 val cons_cons_subset = result(); |
161 val cons_cons_subset = result(); |
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 (AC_cs addSIs [cons_eqpoll_succ] addEs [equals0D]) 1); |
165 by (fast_tac (AC_cs addSIs [cons_eqpoll_succ] addEs [equals0D]) 1); |
166 val cons_cons_eqpoll = result(); |
166 val cons_cons_eqpoll = result(); |
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 AC_cs 1); |
169 by (fast_tac AC_cs 1); |
170 val s_u_subset = result(); |
170 val s_u_subset = result(); |
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 (AC_cs addDs [eqpoll_imp_lepoll RS cons_lepoll_cong] |
175 by (fast_tac (AC_cs 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 val s_uI = result(); |
177 val s_uI = result(); |
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 AC_cs 1); |
180 by (fast_tac AC_cs 1); |
181 val in_s_u_imp_u_in = result(); |
181 val in_s_u_imp_u_in = result(); |
182 |
182 |
183 goal thy |
183 goal thy |
184 "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ |
184 "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ |
185 \ EX! w. w:t_n & z <= w; \ |
185 \ EX! w. w:t_n & z <= w; \ |
186 \ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0 |] \ |
186 \ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0 |] \ |
187 \ ==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c"; |
187 \ ==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c"; |
188 by (etac ballE 1); |
188 by (etac ballE 1); |
189 by (fast_tac (FOL_cs addSIs [CollectI, cons_cons_subset, |
189 by (fast_tac (FOL_cs addSIs [CollectI, cons_cons_subset, |
190 eqpoll_sym RS cons_cons_eqpoll]) 2); |
190 eqpoll_sym RS cons_cons_eqpoll]) 2); |
191 by (etac ex1E 1); |
191 by (etac ex1E 1); |
192 by (res_inst_tac [("a","w")] ex1I 1); |
192 by (res_inst_tac [("a","w")] ex1I 1); |
193 by (rtac conjI 1); |
193 by (rtac conjI 1); |
194 by (rtac CollectI 1); |
194 by (rtac CollectI 1); |
195 by (fast_tac (FOL_cs addSEs [s_uI]) 1); |
195 by (fast_tac (FOL_cs addSEs [s_uI]) 1); |
241 goal thy "!!a. [| a=b; a=c; b=d |] ==> c=d"; |
241 goal thy "!!a. [| a=b; a=c; b=d |] ==> c=d"; |
242 by (asm_full_simp_tac AC_ss 1); |
242 by (asm_full_simp_tac AC_ss 1); |
243 val msubst = result(); |
243 val msubst = result(); |
244 |
244 |
245 (* ********************************************************************** *) |
245 (* ********************************************************************** *) |
246 (* 1. y is less than or equipollent to {v:s_u. a <= v} *) |
246 (* 1. y is less than or equipollent to {v:s_u. a <= v} *) |
247 (* where a is certain k-2 element subset of y *) |
247 (* where a is certain k-2 element subset of y *) |
248 (* ********************************************************************** *) |
248 (* ********************************************************************** *) |
249 |
249 |
250 goal thy |
250 goal thy |
251 "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ |
251 "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ |
252 \ EX! w. w:t_n & z <= w; \ |
252 \ EX! w. w:t_n & z <= w; \ |
253 \ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \ |
253 \ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \ |
254 \ well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; \ |
254 \ well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; \ |
255 \ k:nat; u:x; x Int y = 0 |] \ |
255 \ k:nat; u:x; x Int y = 0 |] \ |
256 \ ==> y lepoll {v:s_u(u, t_n, succ(k), y). a <= v}"; |
256 \ ==> y lepoll {v:s_u(u, t_n, succ(k), y). a <= v}"; |
257 by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS |
257 by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS |
258 eqpoll_imp_lepoll RS lepoll_trans] 1 |
258 eqpoll_imp_lepoll RS lepoll_trans] 1 |
259 THEN REPEAT (assume_tac 1)); |
259 THEN REPEAT (assume_tac 1)); |
260 by (res_inst_tac [("f3","lam b:y-a. \ |
260 by (res_inst_tac [("f3","lam b:y-a. \ |
261 \ THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c")] |
261 \ THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c")] |
262 (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
262 (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
263 by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); |
263 by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); |
264 by (rtac CollectI 1); |
264 by (rtac CollectI 1); |
265 by (rtac lam_type 1); |
265 by (rtac lam_type 1); |
266 by (resolve_tac [ex1_superset_a RS theI RS conjunct1] 1 |
266 by (resolve_tac [ex1_superset_a RS theI RS conjunct1] 1 |
267 THEN REPEAT (assume_tac 1)); |
267 THEN REPEAT (assume_tac 1)); |
268 by (rtac ballI 1); |
268 by (rtac ballI 1); |
269 by (rtac ballI 1); |
269 by (rtac ballI 1); |
270 by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); |
270 by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); |
271 by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); |
271 by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); |
272 by (rtac impI 1); |
272 by (rtac impI 1); |
273 by (rtac cons_eqE 1); |
273 by (rtac cons_eqE 1); |
274 by (fast_tac AC_cs 2); |
274 by (fast_tac AC_cs 2); |
275 by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1); |
275 by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1); |
276 by (eresolve_tac [[asm_rl, the_eq_cons, the_eq_cons] MRS msubst] 1 |
276 by (eresolve_tac [[asm_rl, the_eq_cons, the_eq_cons] MRS msubst] 1 |
277 THEN REPEAT (assume_tac 1)); |
277 THEN REPEAT (assume_tac 1)); |
278 val y_lepoll_subset_s_u = result(); |
278 val y_lepoll_subset_s_u = result(); |
279 |
279 |
280 (* ********************************************************************** *) |
280 (* ********************************************************************** *) |
281 (* some arithmetic *) |
281 (* some arithmetic *) |
282 (* ********************************************************************** *) |
282 (* ********************************************************************** *) |
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 (AC_ss addsimps [add_0]) 1); |
288 by (simp_tac (AC_ss addsimps [add_0]) 1); |
289 by (fast_tac (AC_cs addIs [eqpoll_imp_lepoll RS |
289 by (fast_tac (AC_cs 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 AC_cs 1); |
293 by (fast_tac AC_cs 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); |
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 (AC_cs addSIs [equalityI]) 1); |
300 by (fast_tac (AC_cs addSIs [equalityI]) 1); |
301 val eqpoll_sum_imp_Diff_lepoll_lemma = result(); |
301 val eqpoll_sum_imp_Diff_lepoll_lemma = result(); |
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; \ |
304 \ k:nat; m:nat |] \ |
304 \ k:nat; m:nat |] \ |
305 \ ==> A-B lepoll m"; |
305 \ ==> A-B lepoll m"; |
306 by (dresolve_tac [add_succ RS ssubst] 1); |
306 by (dresolve_tac [add_succ RS ssubst] 1); |
307 by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_lepoll_lemma] 1 |
307 by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_lepoll_lemma] 1 |
308 THEN (REPEAT (assume_tac 1))); |
308 THEN (REPEAT (assume_tac 1))); |
309 by (fast_tac AC_cs 1); |
309 by (fast_tac AC_cs 1); |
310 val eqpoll_sum_imp_Diff_lepoll = result(); |
310 val eqpoll_sum_imp_Diff_lepoll = result(); |
311 |
311 |
312 (* ********************************************************************** *) |
312 (* ********************************************************************** *) |
313 (* similar properties for eqpoll *) |
313 (* similar properties for eqpoll *) |
314 (* ********************************************************************** *) |
314 (* ********************************************************************** *) |
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 (AC_cs addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] |
320 by (fast_tac (AC_cs addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] |
321 addss (AC_ss addsimps [add_0])) 1); |
321 addss (AC_ss 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 (AC_cs addSEs [eqpoll_imp_lepoll]) 1); |
324 by (fast_tac (AC_cs 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 (AC_cs addSIs [Diff_sing_eqpoll, |
328 by (fast_tac (AC_cs 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 (AC_ss addsimps [add_succ])) 1); |
330 addss (AC_ss 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 (AC_cs addSIs [equalityI]) 1); |
332 by (fast_tac (AC_cs addSIs [equalityI]) 1); |
333 val eqpoll_sum_imp_Diff_eqpoll_lemma = result(); |
333 val eqpoll_sum_imp_Diff_eqpoll_lemma = result(); |
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; \ |
336 \ k:nat; m:nat |] \ |
336 \ k:nat; m:nat |] \ |
337 \ ==> A-B eqpoll m"; |
337 \ ==> A-B eqpoll m"; |
338 by (dresolve_tac [add_succ RS ssubst] 1); |
338 by (dresolve_tac [add_succ RS ssubst] 1); |
339 by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_eqpoll_lemma] 1 |
339 by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_eqpoll_lemma] 1 |
340 THEN (REPEAT (assume_tac 1))); |
340 THEN (REPEAT (assume_tac 1))); |
341 by (fast_tac AC_cs 1); |
341 by (fast_tac AC_cs 1); |
342 val eqpoll_sum_imp_Diff_eqpoll = result(); |
342 val eqpoll_sum_imp_Diff_eqpoll = result(); |
343 |
343 |
344 (* ********************************************************************** *) |
344 (* ********************************************************************** *) |
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 (AC_cs addSIs [equalityI] addEs [equals0D]) 1); |
350 by (fast_tac (AC_cs addSIs [equalityI] addEs [equals0D]) 1); |
351 val w_Int_eq_w_Diff = result(); |
351 val w_Int_eq_w_Diff = result(); |
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 (AC_cs addSDs [s_u_subset RS subsetD]) 1); |
360 by (fast_tac (AC_cs addSDs [s_u_subset RS subsetD]) 1); |
361 by (fast_tac (AC_cs addEs [equals0D] addSDs [bspec] |
361 by (fast_tac (AC_cs 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 val w_Int_eqpoll_m = result(); |
365 val w_Int_eqpoll_m = result(); |
366 |
366 |
367 goal thy "!!m. [| 0<m; x eqpoll m; m:nat |] ==> x ~= 0"; |
367 goal thy "!!m. [| 0<m; x eqpoll m; m:nat |] ==> x ~= 0"; |
368 by (fast_tac (empty_cs |
368 by (fast_tac (empty_cs |
369 addSEs [mem_irrefl, ltE, eqpoll_succ_imp_not_empty, natE]) 1); |
369 addSEs [mem_irrefl, ltE, eqpoll_succ_imp_not_empty, natE]) 1); |
370 val eqpoll_m_not_empty = result(); |
370 val eqpoll_m_not_empty = result(); |
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 (AC_cs addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1); |
375 by (fast_tac (AC_cs addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1); |
376 val cons_cons_in = result(); |
376 val cons_cons_in = result(); |
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} *) |
381 (* ********************************************************************** *) |
381 (* ********************************************************************** *) |
382 |
382 |
383 goal thy |
383 goal thy |
384 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \ |
384 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \ |
385 \ EX! w. w:t_n & z <= w; \ |
385 \ EX! w. w:t_n & z <= w; \ |
386 \ t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ |
386 \ t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ |
387 \ 0<m; m:nat; l:nat; \ |
387 \ 0<m; m:nat; l:nat; \ |
388 \ ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y; \ |
388 \ ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y; \ |
389 \ a <= y; l eqpoll a; x Int y = 0; u : x \ |
389 \ a <= y; l eqpoll a; x Int y = 0; u : x \ |
390 \ |] ==> {v:s_u(u, t_n, succ(l), y). a <= v} \ |
390 \ |] ==> {v:s_u(u, t_n, succ(l), y). a <= v} \ |
391 \ lepoll {v:Pow(x). v eqpoll m}"; |
391 \ lepoll {v:Pow(x). v eqpoll m}"; |
392 by (res_inst_tac [("f3","lam w:{v:s_u(u, t_n, succ(l), y). a <= v}. \ |
392 by (res_inst_tac [("f3","lam w:{v:s_u(u, t_n, succ(l), y). a <= v}. \ |
393 \ w Int (x - {u})")] |
393 \ w Int (x - {u})")] |
394 (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
394 (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
395 by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); |
395 by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); |
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 AC_cs 1); |
399 by (fast_tac AC_cs 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 AC_ss 1); |
401 by (simp_tac AC_ss 1); |
402 by (REPEAT (resolve_tac [ballI, impI] 1)); |
402 by (REPEAT (resolve_tac [ballI, impI] 1)); |
403 by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1 |
403 by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1 |
404 THEN REPEAT (assume_tac 1)); |
404 THEN REPEAT (assume_tac 1)); |
405 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); |
405 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); |
406 by (dresolve_tac [cons_cons_in RSN (2, bspec)] 1 THEN REPEAT (assume_tac 1)); |
406 by (dresolve_tac [cons_cons_in RSN (2, bspec)] 1 THEN REPEAT (assume_tac 1)); |
407 by (etac ex1_two_eq 1); |
407 by (etac ex1_two_eq 1); |
408 by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
408 by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
409 by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
409 by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); |
414 by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1); |
414 by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1); |
415 by (fast_tac (empty_cs addSIs [refl, bexI]) 1); |
415 by (fast_tac (empty_cs addSIs [refl, bexI]) 1); |
416 val ex_eq_succ = result(); |
416 val ex_eq_succ = result(); |
417 |
417 |
418 goal thy |
418 goal thy |
419 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ |
419 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ |
420 \ EX! w. w:t_n & z <= w; \ |
420 \ EX! w. w:t_n & z <= w; \ |
421 \ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ |
421 \ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ |
422 \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
422 \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
423 \ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
423 \ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
424 \ |] ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y"; |
424 \ |] ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y"; |
425 by (rtac suppose_not 1); |
425 by (rtac suppose_not 1); |
426 by (eresolve_tac [ex_eq_succ RS bexE] 1 THEN (assume_tac 1)); |
426 by (eresolve_tac [ex_eq_succ RS bexE] 1 THEN (assume_tac 1)); |
427 by (hyp_subst_tac 1); |
427 by (hyp_subst_tac 1); |
428 by (res_inst_tac [("n1","xa")] (ex_subset_eqpoll_n RS exE) 1 |
428 by (res_inst_tac [("n1","xa")] (ex_subset_eqpoll_n RS exE) 1 |
429 THEN REPEAT (assume_tac 1)); |
429 THEN REPEAT (assume_tac 1)); |
430 by (etac conjE 1); |
430 by (etac conjE 1); |
431 by (forward_tac [[y_lepoll_subset_s_u, subset_s_u_lepoll_w] MRS lepoll_trans] 1 |
431 by (forward_tac [[y_lepoll_subset_s_u, subset_s_u_lepoll_w] MRS lepoll_trans] 1 |
432 THEN REPEAT (assume_tac 1)); |
432 THEN REPEAT (assume_tac 1)); |
433 by (contr_tac 1); |
433 by (contr_tac 1); |
434 val exists_proper_in_s_u = result(); |
434 val exists_proper_in_s_u = result(); |
435 |
435 |
436 (* ********************************************************************** *) |
436 (* ********************************************************************** *) |
437 (* LL can be well ordered *) |
437 (* LL can be well ordered *) |
438 (* ********************************************************************** *) |
438 (* ********************************************************************** *) |
439 |
439 |
440 goal thy "{x:Pow(X). x lepoll 0} = {0}"; |
440 goal thy "{x:Pow(X). x lepoll 0} = {0}"; |
441 by (fast_tac (AC_cs addSDs [lepoll_0_is_0] |
441 by (fast_tac (AC_cs addSDs [lepoll_0_is_0] |
442 addSIs [singletonI, lepoll_refl, equalityI] |
442 addSIs [singletonI, lepoll_refl, equalityI] |
443 addSEs [singletonE]) 1); |
443 addSEs [singletonE]) 1); |
444 val subsets_lepoll_0_eq_unit = result(); |
444 val subsets_lepoll_0_eq_unit = result(); |
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 (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
451 by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
452 val well_ord_subsets_eqpoll_n = result(); |
452 val well_ord_subsets_eqpoll_n = result(); |
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 (ZF_cs addIs [le_refl, leI, |
456 by (fast_tac (ZF_cs addIs [le_refl, leI, |
457 le_imp_lepoll, equalityI] |
457 le_imp_lepoll, equalityI] |
458 addSDs [lepoll_succ_disj] |
458 addSDs [lepoll_succ_disj] |
459 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
459 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
460 val subsets_lepoll_succ = result(); |
460 val subsets_lepoll_succ = result(); |
461 |
461 |
462 goal thy "!!n. n:nat ==> \ |
462 goal thy "!!n. n:nat ==> \ |
463 \ {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0"; |
463 \ {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0"; |
464 by (fast_tac (ZF_cs addSEs [eqpoll_sym RS eqpoll_imp_lepoll |
464 by (fast_tac (ZF_cs addSEs [eqpoll_sym RS eqpoll_imp_lepoll |
465 RS lepoll_trans RS succ_lepoll_natE] |
465 RS lepoll_trans RS succ_lepoll_natE] |
466 addSIs [equals0I]) 1); |
466 addSIs [equals0I]) 1); |
467 val Int_empty = result(); |
467 val Int_empty = result(); |
468 |
468 |
469 (* ********************************************************************** *) |
469 (* ********************************************************************** *) |
470 (* unit set is well-ordered by the empty relation *) |
470 (* unit set is well-ordered by the empty relation *) |
471 (* ********************************************************************** *) |
471 (* ********************************************************************** *) |
472 |
472 |
473 goalw thy [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def] |
473 goalw thy [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def] |
474 "tot_ord({a},0)"; |
474 "tot_ord({a},0)"; |
475 by (simp_tac ZF_ss 1); |
475 by (simp_tac ZF_ss 1); |
476 val tot_ord_unit = result(); |
476 val tot_ord_unit = result(); |
477 |
477 |
478 goalw thy [wf_on_def, wf_def] "wf[{a}](0)"; |
478 goalw thy [wf_on_def, wf_def] "wf[{a}](0)"; |
479 by (fast_tac (ZF_cs addSIs [equalityI]) 1); |
479 by (fast_tac (ZF_cs addSIs [equalityI]) 1); |
482 goalw thy [well_ord_def] "well_ord({a},0)"; |
482 goalw thy [well_ord_def] "well_ord({a},0)"; |
483 by (simp_tac (ZF_ss addsimps [tot_ord_unit, wf_on_unit]) 1); |
483 by (simp_tac (ZF_ss addsimps [tot_ord_unit, wf_on_unit]) 1); |
484 val well_ord_unit = result(); |
484 val well_ord_unit = result(); |
485 |
485 |
486 (* ********************************************************************** *) |
486 (* ********************************************************************** *) |
487 (* well_ord_subsets_lepoll_n *) |
487 (* well_ord_subsets_lepoll_n *) |
488 (* ********************************************************************** *) |
488 (* ********************************************************************** *) |
489 |
489 |
490 goal thy "!!y r. [| well_ord(y,r); ~Finite(y); n:nat |] ==> \ |
490 goal thy "!!y r. [| well_ord(y,r); ~Finite(y); n:nat |] ==> \ |
491 \ EX R. well_ord({z:Pow(y). z lepoll n}, R)"; |
491 \ EX R. well_ord({z:Pow(y). z lepoll n}, R)"; |
492 by (etac nat_induct 1); |
492 by (etac nat_induct 1); |
493 by (fast_tac (ZF_cs addSIs [well_ord_unit] |
493 by (fast_tac (ZF_cs addSIs [well_ord_unit] |
494 addss (ZF_ss addsimps [subsets_lepoll_0_eq_unit])) 1); |
494 addss (ZF_ss addsimps [subsets_lepoll_0_eq_unit])) 1); |
495 by (etac exE 1); |
495 by (etac exE 1); |
496 by (eresolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 |
496 by (eresolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 |
497 THEN REPEAT (assume_tac 1)); |
497 THEN REPEAT (assume_tac 1)); |
498 by (asm_simp_tac (ZF_ss addsimps [subsets_lepoll_succ]) 1); |
498 by (asm_simp_tac (ZF_ss addsimps [subsets_lepoll_succ]) 1); |
499 by (dtac well_ord_radd 1 THEN (assume_tac 1)); |
499 by (dtac well_ord_radd 1 THEN (assume_tac 1)); |
500 by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS |
500 by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS |
501 (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
501 (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
502 by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
502 by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
503 val well_ord_subsets_lepoll_n = result(); |
503 val well_ord_subsets_lepoll_n = result(); |
504 |
504 |
505 goalw thy [LL_def, MM_def] |
505 goalw thy [LL_def, MM_def] |
506 "!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \ |
506 "!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \ |
507 \ ==> LL(t_n, k, y) <= {z:Pow(y). z lepoll n}"; |
507 \ ==> LL(t_n, k, y) <= {z:Pow(y). z lepoll n}"; |
508 by (fast_tac (AC_cs addSEs [RepFunE] |
508 by (fast_tac (AC_cs addSEs [RepFunE] |
509 addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll |
509 addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll |
510 RSN (2, lepoll_trans))]) 1); |
510 RSN (2, lepoll_trans))]) 1); |
511 val LL_subset = result(); |
511 val LL_subset = result(); |
512 |
512 |
513 goal thy "!!x. [| t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
513 goal thy "!!x. [| t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
514 \ well_ord(y, R); ~Finite(y); n:nat \ |
514 \ well_ord(y, R); ~Finite(y); n:nat \ |
515 \ |] ==> EX S. well_ord(LL(t_n, k, y), S)"; |
515 \ |] ==> EX S. well_ord(LL(t_n, k, y), S)"; |
516 by (fast_tac (FOL_cs addIs [exI] |
516 by (fast_tac (FOL_cs addIs [exI] |
517 addSEs [LL_subset RSN (2, well_ord_subset)] |
517 addSEs [LL_subset RSN (2, well_ord_subset)] |
518 addEs [well_ord_subsets_lepoll_n RS exE]) 1); |
518 addEs [well_ord_subsets_lepoll_n RS exE]) 1); |
519 val well_ord_LL = result(); |
519 val well_ord_LL = result(); |
520 |
520 |
521 (* ********************************************************************** *) |
521 (* ********************************************************************** *) |
522 (* every element of LL is a contained in exactly one element of MM *) |
522 (* every element of LL is a contained in exactly one element of MM *) |
523 (* ********************************************************************** *) |
523 (* ********************************************************************** *) |
524 |
524 |
525 goalw thy [MM_def, LL_def] |
525 goalw thy [MM_def, LL_def] |
526 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
526 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
527 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
527 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
528 \ v:LL(t_n, k, y) \ |
528 \ v:LL(t_n, k, y) \ |
529 \ |] ==> EX! w. w:MM(t_n, k, y) & v<=w"; |
529 \ |] ==> EX! w. w:MM(t_n, k, y) & v<=w"; |
530 by (step_tac (AC_cs addSEs [RepFunE]) 1); |
530 by (step_tac (AC_cs addSEs [RepFunE]) 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 (AC_cs addSEs [eqpoll_sym]) 2); |
533 by (fast_tac (AC_cs addSEs [eqpoll_sym]) 2); |
534 by (res_inst_tac [("a","v")] ex1I 1); |
534 by (res_inst_tac [("a","v")] ex1I 1); |
567 goalw thy [MM_def] "MM(t_n, k, y) <= t_n"; |
567 goalw thy [MM_def] "MM(t_n, k, y) <= t_n"; |
568 by (fast_tac AC_cs 1); |
568 by (fast_tac AC_cs 1); |
569 val MM_subset = result(); |
569 val MM_subset = result(); |
570 |
570 |
571 goal thy |
571 goal thy |
572 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ |
572 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ |
573 \ EX! w. w:t_n & z <= w; \ |
573 \ EX! w. w:t_n & z <= w; \ |
574 \ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ |
574 \ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ |
575 \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
575 \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
576 \ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
576 \ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
577 \ |] ==> EX w:LL(t_n, succ(k), y). u:GG(t_n, succ(k), y)`w"; |
577 \ |] ==> EX w:LL(t_n, succ(k), y). u:GG(t_n, succ(k), y)`w"; |
578 by (forward_tac [exists_in_MM] 1 THEN REPEAT (assume_tac 1)); |
578 by (forward_tac [exists_in_MM] 1 THEN REPEAT (assume_tac 1)); |
579 by (etac bexE 1); |
579 by (etac bexE 1); |
580 by (res_inst_tac [("x","w Int y")] bexI 1); |
580 by (res_inst_tac [("x","w Int y")] bexI 1); |
581 by (etac Int_in_LL 2); |
581 by (etac Int_in_LL 2); |
582 by (rewtac GG_def); |
582 by (rewtac GG_def); |
583 by (asm_full_simp_tac (AC_ss addsimps [Int_in_LL]) 1); |
583 by (asm_full_simp_tac (AC_ss addsimps [Int_in_LL]) 1); |
584 by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1 |
584 by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1 |
585 THEN (assume_tac 1)); |
585 THEN (assume_tac 1)); |
586 by (REPEAT (fast_tac (AC_cs addEs [equals0D] addSEs [Int_in_LL]) 1)); |
586 by (REPEAT (fast_tac (AC_cs addEs [equals0D] addSEs [Int_in_LL]) 1)); |
587 val exists_in_LL = result(); |
587 val exists_in_LL = result(); |
588 |
588 |
589 goalw thy [LL_def] |
589 goalw thy [LL_def] |
590 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
590 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
591 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
591 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
592 \ v : LL(t_n, k, y) |] \ |
592 \ v : LL(t_n, k, y) |] \ |
593 \ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y"; |
593 \ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y"; |
594 by (fast_tac (AC_cs addSEs [Int_in_LL, |
594 by (fast_tac (AC_cs addSEs [Int_in_LL, |
595 unique_superset_in_MM RS the_equality2 RS ssubst]) 1); |
595 unique_superset_in_MM RS the_equality2 RS ssubst]) 1); |
596 val in_LL_eq_Int = result(); |
596 val in_LL_eq_Int = result(); |
597 |
597 |
598 goal thy |
598 goal thy |
599 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
599 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
600 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
600 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
601 \ v : LL(t_n, k, y) |] \ |
601 \ v : LL(t_n, k, y) |] \ |
602 \ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y"; |
602 \ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y"; |
603 by (fast_tac (AC_cs addSDs [unique_superset_in_MM RS theI RS conjunct1 RS |
603 by (fast_tac (AC_cs addSDs [unique_superset_in_MM RS theI RS conjunct1 RS |
604 (MM_subset RS subsetD)]) 1); |
604 (MM_subset RS subsetD)]) 1); |
605 val the_in_MM_subset = result(); |
605 val the_in_MM_subset = result(); |
606 |
606 |
607 goalw thy [GG_def] |
607 goalw thy [GG_def] |
608 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
608 "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ |
609 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
609 \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ |
610 \ v : LL(t_n, k, y) |] \ |
610 \ v : LL(t_n, k, y) |] \ |
611 \ ==> GG(t_n, k, y) ` v <= x"; |
611 \ ==> GG(t_n, k, y) ` v <= x"; |
612 by (asm_full_simp_tac AC_ss 1); |
612 by (asm_full_simp_tac AC_ss 1); |
613 by (forward_tac [the_in_MM_subset] 1 THEN REPEAT (assume_tac 1)); |
613 by (forward_tac [the_in_MM_subset] 1 THEN REPEAT (assume_tac 1)); |
614 by (dtac in_LL_eq_Int 1 THEN REPEAT (assume_tac 1)); |
614 by (dtac in_LL_eq_Int 1 THEN REPEAT (assume_tac 1)); |
615 by (rtac subsetI 1); |
615 by (rtac subsetI 1); |
616 by (etac DiffE 1); |
616 by (etac DiffE 1); |
617 by (etac swap 1); |
617 by (etac swap 1); |
618 by (fast_tac (AC_cs addEs [ssubst]) 1); |
618 by (fast_tac (AC_cs addEs [ssubst]) 1); |
619 val GG_subset = result(); |
619 val GG_subset = result(); |
620 |
620 |
621 goal thy |
621 goal thy |
622 "!!x. [| well_ord(LL(t_n, succ(k), y), S); \ |
622 "!!x. [| well_ord(LL(t_n, succ(k), y), S); \ |
623 \ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ |
623 \ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ |
624 \ well_ord(y,R); ~Finite(y); x Int y = 0; \ |
624 \ well_ord(y,R); ~Finite(y); x Int y = 0; \ |
625 \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
625 \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
626 \ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
626 \ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \ |
627 \ |] ==> (UN b<ordertype(LL(t_n, succ(k), y), S). \ |
627 \ |] ==> (UN b<ordertype(LL(t_n, succ(k), y), S). \ |
628 \ (GG(t_n, succ(k), y)) ` \ |
628 \ (GG(t_n, succ(k), y)) ` \ |
629 \ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b)) = x"; |
629 \ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b)) = x"; |
630 by (rtac equalityI 1); |
630 by (rtac equalityI 1); |
631 by (rtac subsetI 1); |
631 by (rtac subsetI 1); |
632 by (etac OUN_E 1); |
632 by (etac OUN_E 1); |
633 by (eresolve_tac [GG_subset RS subsetD] 1 THEN TRYALL assume_tac); |
633 by (eresolve_tac [GG_subset RS subsetD] 1 THEN TRYALL assume_tac); |
634 by (eresolve_tac [ordermap_bij RS bij_converse_bij RS |
634 by (eresolve_tac [ordermap_bij RS bij_converse_bij RS |
635 bij_is_fun RS apply_type] 1); |
635 bij_is_fun RS apply_type] 1); |
636 by (etac ltD 1); |
636 by (etac ltD 1); |
637 by (rtac subsetI 1); |
637 by (rtac subsetI 1); |
638 by (eresolve_tac [exists_in_LL RS bexE] 1 THEN REPEAT (assume_tac 1)); |
638 by (eresolve_tac [exists_in_LL RS bexE] 1 THEN REPEAT (assume_tac 1)); |
639 by (rtac OUN_I 1); |
639 by (rtac OUN_I 1); |
640 by (resolve_tac [Ord_ordertype RSN (2, ltI)] 1 THEN (assume_tac 2)); |
640 by (resolve_tac [Ord_ordertype RSN (2, ltI)] 1 THEN (assume_tac 2)); |
641 by (eresolve_tac [ordermap_type RS apply_type] 1); |
641 by (eresolve_tac [ordermap_type RS apply_type] 1); |
642 by (eresolve_tac [ordermap_bij RS bij_is_inj RS left_inverse RS ssubst] 1 |
642 by (eresolve_tac [ordermap_bij RS bij_is_inj RS left_inverse RS ssubst] 1 |
643 THEN REPEAT (assume_tac 1)); |
643 THEN REPEAT (assume_tac 1)); |
644 val OUN_eq_x = result(); |
644 val OUN_eq_x = result(); |
645 |
645 |
646 (* ********************************************************************** *) |
646 (* ********************************************************************** *) |
647 (* Every element of the family is less than or equipollent to n-k (m) *) |
647 (* Every element of the family is less than or equipollent to n-k (m) *) |
648 (* ********************************************************************** *) |
648 (* ********************************************************************** *) |
649 |
649 |
650 goalw thy [MM_def] |
650 goalw thy [MM_def] |
651 "!!w. [| w : MM(t_n, k, y); t_n <= {v:Pow(x Un y). v eqpoll n} \ |
651 "!!w. [| w : MM(t_n, k, y); t_n <= {v:Pow(x Un y). v eqpoll n} \ |
652 \ |] ==> w eqpoll n"; |
652 \ |] ==> w eqpoll n"; |
653 by (fast_tac AC_cs 1); |
653 by (fast_tac AC_cs 1); |
654 val in_MM_eqpoll_n = result(); |
654 val in_MM_eqpoll_n = result(); |
655 |
655 |
656 goalw thy [LL_def, MM_def] |
656 goalw thy [LL_def, MM_def] |
657 "!!w. w : LL(t_n, k, y) ==> k lepoll w"; |
657 "!!w. w : LL(t_n, k, y) ==> k lepoll w"; |
658 by (fast_tac AC_cs 1); |
658 by (fast_tac AC_cs 1); |
659 val in_LL_eqpoll_n = result(); |
659 val in_LL_eqpoll_n = result(); |
660 |
660 |
661 goalw thy [GG_def] |
661 goalw thy [GG_def] |
662 "!!x. [| \ |
662 "!!x. [| \ |
663 \ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ |
663 \ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ |
664 \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
664 \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ |
665 \ well_ord(LL(t_n, succ(k), y), S); k:nat; m:nat |] \ |
665 \ well_ord(LL(t_n, succ(k), y), S); k:nat; m:nat |] \ |
666 \ ==> ALL b<ordertype(LL(t_n, succ(k), y), S). \ |
666 \ ==> ALL b<ordertype(LL(t_n, succ(k), y), S). \ |
667 \ (GG(t_n, succ(k), y)) ` \ |
667 \ (GG(t_n, succ(k), y)) ` \ |
668 \ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b) lepoll m"; |
668 \ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b) lepoll m"; |
669 by (rtac oallI 1); |
669 by (rtac oallI 1); |
670 by (asm_full_simp_tac (AC_ss addsimps [ltD, |
670 by (asm_full_simp_tac (AC_ss addsimps [ltD, |
671 ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1); |
671 ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1); |
672 by (rtac eqpoll_sum_imp_Diff_lepoll 1); |
672 by (rtac eqpoll_sum_imp_Diff_lepoll 1); |
673 by (REPEAT (fast_tac (FOL_cs addSDs [ltD] |
673 by (REPEAT (fast_tac (FOL_cs addSDs [ltD] |
674 addSIs [eqpoll_sum_imp_Diff_lepoll, in_LL_eqpoll_n] |
674 addSIs [eqpoll_sum_imp_Diff_lepoll, in_LL_eqpoll_n] |
675 addEs [unique_superset_in_MM RS theI RS conjunct1 RS in_MM_eqpoll_n, |
675 addEs [unique_superset_in_MM RS theI RS conjunct1 RS in_MM_eqpoll_n, |
676 in_LL_eq_Int RS equalityD1 RS (Int_lower1 RSN (2, subset_trans)), |
676 in_LL_eq_Int RS equalityD1 RS (Int_lower1 RSN (2, subset_trans)), |
677 ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1)); |
677 ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1)); |
678 val all_in_lepoll_m = result(); |
678 val all_in_lepoll_m = result(); |
679 |
679 |
680 (* ********************************************************************** *) |
680 (* ********************************************************************** *) |
681 (* The main theorem AC16(n, k) ==> WO4(n-k) *) |
681 (* The main theorem AC16(n, k) ==> WO4(n-k) *) |
682 (* ********************************************************************** *) |
682 (* ********************************************************************** *) |
683 |
683 |
684 goalw thy [AC16_def,WO4_def] |
684 goalw thy [AC16_def,WO4_def] |
685 "!!n k. [| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)"; |
685 "!!n k. [| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)"; |
686 by (rtac allI 1); |
686 by (rtac allI 1); |
687 by (excluded_middle_tac "Finite(A)" 1); |
687 by (excluded_middle_tac "Finite(A)" 1); |
688 by (rtac lemma1 2 THEN REPEAT (assume_tac 2)); |
688 by (rtac lemma1 2 THEN REPEAT (assume_tac 2)); |
689 by (resolve_tac [lemma2 RS revcut_rl] 1); |
689 by (resolve_tac [lemma2 RS revcut_rl] 1); |
690 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
690 by (REPEAT (eresolve_tac [exE, conjE] 1)); |