15 (** Lemma: Banach's Decomposition Theorem **) |
15 (** Lemma: Banach's Decomposition Theorem **) |
16 |
16 |
17 goal Cardinal.thy "bnd_mono(X, %W. X - g``(Y - f``W))"; |
17 goal Cardinal.thy "bnd_mono(X, %W. X - g``(Y - f``W))"; |
18 by (rtac bnd_monoI 1); |
18 by (rtac bnd_monoI 1); |
19 by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); |
19 by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); |
20 val decomp_bnd_mono = result(); |
20 qed "decomp_bnd_mono"; |
21 |
21 |
22 val [gfun] = goal Cardinal.thy |
22 val [gfun] = goal Cardinal.thy |
23 "g: Y->X ==> \ |
23 "g: Y->X ==> \ |
24 \ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \ |
24 \ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \ |
25 \ X - lfp(X, %W. X - g``(Y - f``W)) "; |
25 \ X - lfp(X, %W. X - g``(Y - f``W)) "; |
26 by (res_inst_tac [("P", "%u. ?v = X-u")] |
26 by (res_inst_tac [("P", "%u. ?v = X-u")] |
27 (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); |
27 (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); |
28 by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, |
28 by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, |
29 gfun RS fun_is_rel RS image_subset]) 1); |
29 gfun RS fun_is_rel RS image_subset]) 1); |
30 val Banach_last_equation = result(); |
30 qed "Banach_last_equation"; |
31 |
31 |
32 val prems = goal Cardinal.thy |
32 val prems = goal Cardinal.thy |
33 "[| f: X->Y; g: Y->X |] ==> \ |
33 "[| f: X->Y; g: Y->X |] ==> \ |
34 \ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ |
34 \ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ |
35 \ (YA Int YB = 0) & (YA Un YB = Y) & \ |
35 \ (YA Int YB = 0) & (YA Un YB = Y) & \ |
37 by (REPEAT |
37 by (REPEAT |
38 (FIRSTGOAL |
38 (FIRSTGOAL |
39 (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); |
39 (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); |
40 by (rtac Banach_last_equation 3); |
40 by (rtac Banach_last_equation 3); |
41 by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); |
41 by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); |
42 val decomposition = result(); |
42 qed "decomposition"; |
43 |
43 |
44 val prems = goal Cardinal.thy |
44 val prems = goal Cardinal.thy |
45 "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"; |
45 "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"; |
46 by (cut_facts_tac prems 1); |
46 by (cut_facts_tac prems 1); |
47 by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); |
47 by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); |
48 by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] |
48 by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] |
49 addIs [bij_converse_bij]) 1); |
49 addIs [bij_converse_bij]) 1); |
50 (* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" |
50 (* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" |
51 is forced by the context!! *) |
51 is forced by the context!! *) |
52 val schroeder_bernstein = result(); |
52 qed "schroeder_bernstein"; |
53 |
53 |
54 |
54 |
55 (** Equipollence is an equivalence relation **) |
55 (** Equipollence is an equivalence relation **) |
56 |
56 |
57 goalw Cardinal.thy [eqpoll_def] "X eqpoll X"; |
57 goalw Cardinal.thy [eqpoll_def] "X eqpoll X"; |
58 by (rtac exI 1); |
58 by (rtac exI 1); |
59 by (rtac id_bij 1); |
59 by (rtac id_bij 1); |
60 val eqpoll_refl = result(); |
60 qed "eqpoll_refl"; |
61 |
61 |
62 goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X"; |
62 goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X"; |
63 by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1); |
63 by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1); |
64 val eqpoll_sym = result(); |
64 qed "eqpoll_sym"; |
65 |
65 |
66 goalw Cardinal.thy [eqpoll_def] |
66 goalw Cardinal.thy [eqpoll_def] |
67 "!!X Y. [| X eqpoll Y; Y eqpoll Z |] ==> X eqpoll Z"; |
67 "!!X Y. [| X eqpoll Y; Y eqpoll Z |] ==> X eqpoll Z"; |
68 by (fast_tac (ZF_cs addIs [comp_bij]) 1); |
68 by (fast_tac (ZF_cs addIs [comp_bij]) 1); |
69 val eqpoll_trans = result(); |
69 qed "eqpoll_trans"; |
70 |
70 |
71 (** Le-pollence is a partial ordering **) |
71 (** Le-pollence is a partial ordering **) |
72 |
72 |
73 goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y"; |
73 goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y"; |
74 by (rtac exI 1); |
74 by (rtac exI 1); |
75 by (etac id_subset_inj 1); |
75 by (etac id_subset_inj 1); |
76 val subset_imp_lepoll = result(); |
76 qed "subset_imp_lepoll"; |
77 |
77 |
78 val lepoll_refl = subset_refl RS subset_imp_lepoll; |
78 val lepoll_refl = subset_refl RS subset_imp_lepoll; |
79 |
79 |
80 goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def] |
80 goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def] |
81 "!!X Y. X eqpoll Y ==> X lepoll Y"; |
81 "!!X Y. X eqpoll Y ==> X lepoll Y"; |
82 by (fast_tac ZF_cs 1); |
82 by (fast_tac ZF_cs 1); |
83 val eqpoll_imp_lepoll = result(); |
83 qed "eqpoll_imp_lepoll"; |
84 |
84 |
85 goalw Cardinal.thy [lepoll_def] |
85 goalw Cardinal.thy [lepoll_def] |
86 "!!X Y. [| X lepoll Y; Y lepoll Z |] ==> X lepoll Z"; |
86 "!!X Y. [| X lepoll Y; Y lepoll Z |] ==> X lepoll Z"; |
87 by (fast_tac (ZF_cs addIs [comp_inj]) 1); |
87 by (fast_tac (ZF_cs addIs [comp_inj]) 1); |
88 val lepoll_trans = result(); |
88 qed "lepoll_trans"; |
89 |
89 |
90 (*Asymmetry law*) |
90 (*Asymmetry law*) |
91 goalw Cardinal.thy [lepoll_def,eqpoll_def] |
91 goalw Cardinal.thy [lepoll_def,eqpoll_def] |
92 "!!X Y. [| X lepoll Y; Y lepoll X |] ==> X eqpoll Y"; |
92 "!!X Y. [| X lepoll Y; Y lepoll X |] ==> X eqpoll Y"; |
93 by (REPEAT (etac exE 1)); |
93 by (REPEAT (etac exE 1)); |
94 by (rtac schroeder_bernstein 1); |
94 by (rtac schroeder_bernstein 1); |
95 by (REPEAT (assume_tac 1)); |
95 by (REPEAT (assume_tac 1)); |
96 val eqpollI = result(); |
96 qed "eqpollI"; |
97 |
97 |
98 val [major,minor] = goal Cardinal.thy |
98 val [major,minor] = goal Cardinal.thy |
99 "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P"; |
99 "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P"; |
100 by (rtac minor 1); |
100 by (rtac minor 1); |
101 by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1)); |
101 by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1)); |
102 val eqpollE = result(); |
102 qed "eqpollE"; |
103 |
103 |
104 goal Cardinal.thy "X eqpoll Y <-> X lepoll Y & Y lepoll X"; |
104 goal Cardinal.thy "X eqpoll Y <-> X lepoll Y & Y lepoll X"; |
105 by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1); |
105 by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1); |
106 val eqpoll_iff = result(); |
106 qed "eqpoll_iff"; |
107 |
107 |
108 |
108 |
109 (** LEAST -- the least number operator [from HOL/Univ.ML] **) |
109 (** LEAST -- the least number operator [from HOL/Univ.ML] **) |
110 |
110 |
111 val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def] |
111 val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def] |
113 by (rtac the_equality 1); |
113 by (rtac the_equality 1); |
114 by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1); |
114 by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1); |
115 by (REPEAT (etac conjE 1)); |
115 by (REPEAT (etac conjE 1)); |
116 by (etac (premOrd RS Ord_linear_lt) 1); |
116 by (etac (premOrd RS Ord_linear_lt) 1); |
117 by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot]))); |
117 by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot]))); |
118 val Least_equality = result(); |
118 qed "Least_equality"; |
119 |
119 |
120 goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> P(LEAST x.P(x))"; |
120 goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> P(LEAST x.P(x))"; |
121 by (etac rev_mp 1); |
121 by (etac rev_mp 1); |
122 by (trans_ind_tac "i" [] 1); |
122 by (trans_ind_tac "i" [] 1); |
123 by (rtac impI 1); |
123 by (rtac impI 1); |
124 by (rtac classical 1); |
124 by (rtac classical 1); |
125 by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); |
125 by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); |
126 by (assume_tac 2); |
126 by (assume_tac 2); |
127 by (fast_tac (ZF_cs addSEs [ltE]) 1); |
127 by (fast_tac (ZF_cs addSEs [ltE]) 1); |
128 val LeastI = result(); |
128 qed "LeastI"; |
129 |
129 |
130 (*Proof is almost identical to the one above!*) |
130 (*Proof is almost identical to the one above!*) |
131 goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> (LEAST x.P(x)) le i"; |
131 goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> (LEAST x.P(x)) le i"; |
132 by (etac rev_mp 1); |
132 by (etac rev_mp 1); |
133 by (trans_ind_tac "i" [] 1); |
133 by (trans_ind_tac "i" [] 1); |
134 by (rtac impI 1); |
134 by (rtac impI 1); |
135 by (rtac classical 1); |
135 by (rtac classical 1); |
136 by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); |
136 by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); |
137 by (etac le_refl 2); |
137 by (etac le_refl 2); |
138 by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1); |
138 by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1); |
139 val Least_le = result(); |
139 qed "Least_le"; |
140 |
140 |
141 (*LEAST really is the smallest*) |
141 (*LEAST really is the smallest*) |
142 goal Cardinal.thy "!!i. [| P(i); i < (LEAST x.P(x)) |] ==> Q"; |
142 goal Cardinal.thy "!!i. [| P(i); i < (LEAST x.P(x)) |] ==> Q"; |
143 by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1); |
143 by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1); |
144 by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); |
144 by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); |
145 val less_LeastE = result(); |
145 qed "less_LeastE"; |
146 |
146 |
147 (*If there is no such P then LEAST is vacuously 0*) |
147 (*If there is no such P then LEAST is vacuously 0*) |
148 goalw Cardinal.thy [Least_def] |
148 goalw Cardinal.thy [Least_def] |
149 "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x.P(x)) = 0"; |
149 "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x.P(x)) = 0"; |
150 by (rtac the_0 1); |
150 by (rtac the_0 1); |
151 by (fast_tac ZF_cs 1); |
151 by (fast_tac ZF_cs 1); |
152 val Least_0 = result(); |
152 qed "Least_0"; |
153 |
153 |
154 goal Cardinal.thy "Ord(LEAST x.P(x))"; |
154 goal Cardinal.thy "Ord(LEAST x.P(x))"; |
155 by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1); |
155 by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1); |
156 by (safe_tac ZF_cs); |
156 by (safe_tac ZF_cs); |
157 by (rtac (Least_le RS ltE) 2); |
157 by (rtac (Least_le RS ltE) 2); |
158 by (REPEAT_SOME assume_tac); |
158 by (REPEAT_SOME assume_tac); |
159 by (etac (Least_0 RS ssubst) 1); |
159 by (etac (Least_0 RS ssubst) 1); |
160 by (rtac Ord_0 1); |
160 by (rtac Ord_0 1); |
161 val Ord_Least = result(); |
161 qed "Ord_Least"; |
162 |
162 |
163 |
163 |
164 (** Basic properties of cardinals **) |
164 (** Basic properties of cardinals **) |
165 |
165 |
166 (*Not needed for simplification, but helpful below*) |
166 (*Not needed for simplification, but helpful below*) |
167 val prems = goal Cardinal.thy |
167 val prems = goal Cardinal.thy |
168 "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))"; |
168 "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))"; |
169 by (simp_tac (FOL_ss addsimps prems) 1); |
169 by (simp_tac (FOL_ss addsimps prems) 1); |
170 val Least_cong = result(); |
170 qed "Least_cong"; |
171 |
171 |
172 (*Need AC to prove X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le *) |
172 (*Need AC to prove X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le *) |
173 goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|"; |
173 goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|"; |
174 by (rtac Least_cong 1); |
174 by (rtac Least_cong 1); |
175 by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); |
175 by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); |
176 val cardinal_cong = result(); |
176 qed "cardinal_cong"; |
177 |
177 |
178 (*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*) |
178 (*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*) |
179 goalw Cardinal.thy [eqpoll_def, cardinal_def] |
179 goalw Cardinal.thy [eqpoll_def, cardinal_def] |
180 "!!A. well_ord(A,r) ==> |A| eqpoll A"; |
180 "!!A. well_ord(A,r) ==> |A| eqpoll A"; |
181 by (rtac LeastI 1); |
181 by (rtac LeastI 1); |
182 by (etac Ord_ordertype 2); |
182 by (etac Ord_ordertype 2); |
183 by (rtac exI 1); |
183 by (rtac exI 1); |
184 by (etac (ordermap_bij RS bij_converse_bij) 1); |
184 by (etac (ordermap_bij RS bij_converse_bij) 1); |
185 val well_ord_cardinal_eqpoll = result(); |
185 qed "well_ord_cardinal_eqpoll"; |
186 |
186 |
187 val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll |
187 val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll |
188 |> standard; |
188 |> standard; |
189 |
189 |
190 goal Cardinal.thy |
190 goal Cardinal.thy |
191 "!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y"; |
191 "!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y"; |
192 by (rtac (eqpoll_sym RS eqpoll_trans) 1); |
192 by (rtac (eqpoll_sym RS eqpoll_trans) 1); |
193 by (etac well_ord_cardinal_eqpoll 1); |
193 by (etac well_ord_cardinal_eqpoll 1); |
194 by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); |
194 by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); |
195 val well_ord_cardinal_eqE = result(); |
195 qed "well_ord_cardinal_eqE"; |
196 |
196 |
197 |
197 |
198 (** Observations from Kunen, page 28 **) |
198 (** Observations from Kunen, page 28 **) |
199 |
199 |
200 goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i"; |
200 goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i"; |
201 by (etac (eqpoll_refl RS Least_le) 1); |
201 by (etac (eqpoll_refl RS Least_le) 1); |
202 val Ord_cardinal_le = result(); |
202 qed "Ord_cardinal_le"; |
203 |
203 |
204 goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> |K| = K"; |
204 goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> |K| = K"; |
205 by (etac sym 1); |
205 by (etac sym 1); |
206 val Card_cardinal_eq = result(); |
206 qed "Card_cardinal_eq"; |
207 |
207 |
208 val prems = goalw Cardinal.thy [Card_def,cardinal_def] |
208 val prems = goalw Cardinal.thy [Card_def,cardinal_def] |
209 "[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)"; |
209 "[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)"; |
210 by (rtac (Least_equality RS ssubst) 1); |
210 by (rtac (Least_equality RS ssubst) 1); |
211 by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); |
211 by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); |
212 val CardI = result(); |
212 qed "CardI"; |
213 |
213 |
214 goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; |
214 goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; |
215 by (etac ssubst 1); |
215 by (etac ssubst 1); |
216 by (rtac Ord_Least 1); |
216 by (rtac Ord_Least 1); |
217 val Card_is_Ord = result(); |
217 qed "Card_is_Ord"; |
218 |
218 |
219 goalw Cardinal.thy [cardinal_def] "Ord(|A|)"; |
219 goalw Cardinal.thy [cardinal_def] "Ord(|A|)"; |
220 by (rtac Ord_Least 1); |
220 by (rtac Ord_Least 1); |
221 val Ord_cardinal = result(); |
221 qed "Ord_cardinal"; |
222 |
222 |
223 goal Cardinal.thy "Card(0)"; |
223 goal Cardinal.thy "Card(0)"; |
224 by (rtac (Ord_0 RS CardI) 1); |
224 by (rtac (Ord_0 RS CardI) 1); |
225 by (fast_tac (ZF_cs addSEs [ltE]) 1); |
225 by (fast_tac (ZF_cs addSEs [ltE]) 1); |
226 val Card_0 = result(); |
226 qed "Card_0"; |
227 |
227 |
228 val [premK,premL] = goal Cardinal.thy |
228 val [premK,premL] = goal Cardinal.thy |
229 "[| Card(K); Card(L) |] ==> Card(K Un L)"; |
229 "[| Card(K); Card(L) |] ==> Card(K Un L)"; |
230 by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1); |
230 by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1); |
231 by (asm_simp_tac |
231 by (asm_simp_tac |
232 (ZF_ss addsimps [premL, le_imp_subset, subset_Un_iff RS iffD1]) 1); |
232 (ZF_ss addsimps [premL, le_imp_subset, subset_Un_iff RS iffD1]) 1); |
233 by (asm_simp_tac |
233 by (asm_simp_tac |
234 (ZF_ss addsimps [premK, le_imp_subset, subset_Un_iff2 RS iffD1]) 1); |
234 (ZF_ss addsimps [premK, le_imp_subset, subset_Un_iff2 RS iffD1]) 1); |
235 val Card_Un = result(); |
235 qed "Card_Un"; |
236 |
236 |
237 (*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*) |
237 (*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*) |
238 |
238 |
239 goalw Cardinal.thy [cardinal_def] "Card(|A|)"; |
239 goalw Cardinal.thy [cardinal_def] "Card(|A|)"; |
240 by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1); |
240 by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1); |
243 by (safe_tac ZF_cs); |
243 by (safe_tac ZF_cs); |
244 by (rtac less_LeastE 1); |
244 by (rtac less_LeastE 1); |
245 by (assume_tac 2); |
245 by (assume_tac 2); |
246 by (etac eqpoll_trans 1); |
246 by (etac eqpoll_trans 1); |
247 by (REPEAT (ares_tac [LeastI] 1)); |
247 by (REPEAT (ares_tac [LeastI] 1)); |
248 val Card_cardinal = result(); |
248 qed "Card_cardinal"; |
249 |
249 |
250 (*Kunen's Lemma 10.5*) |
250 (*Kunen's Lemma 10.5*) |
251 goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|"; |
251 goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|"; |
252 by (rtac (eqpollI RS cardinal_cong) 1); |
252 by (rtac (eqpollI RS cardinal_cong) 1); |
253 by (etac (le_imp_subset RS subset_imp_lepoll) 1); |
253 by (etac (le_imp_subset RS subset_imp_lepoll) 1); |
254 by (rtac lepoll_trans 1); |
254 by (rtac lepoll_trans 1); |
255 by (etac (le_imp_subset RS subset_imp_lepoll) 2); |
255 by (etac (le_imp_subset RS subset_imp_lepoll) 2); |
256 by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1); |
256 by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1); |
257 by (rtac Ord_cardinal_eqpoll 1); |
257 by (rtac Ord_cardinal_eqpoll 1); |
258 by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); |
258 by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); |
259 val cardinal_eq_lemma = result(); |
259 qed "cardinal_eq_lemma"; |
260 |
260 |
261 goal Cardinal.thy "!!i j. i le j ==> |i| le |j|"; |
261 goal Cardinal.thy "!!i j. i le j ==> |i| le |j|"; |
262 by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1); |
262 by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1); |
263 by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); |
263 by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); |
264 by (rtac cardinal_eq_lemma 1); |
264 by (rtac cardinal_eq_lemma 1); |
265 by (assume_tac 2); |
265 by (assume_tac 2); |
266 by (etac le_trans 1); |
266 by (etac le_trans 1); |
267 by (etac ltE 1); |
267 by (etac ltE 1); |
268 by (etac Ord_cardinal_le 1); |
268 by (etac Ord_cardinal_le 1); |
269 val cardinal_mono = result(); |
269 qed "cardinal_mono"; |
270 |
270 |
271 (*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*) |
271 (*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*) |
272 goal Cardinal.thy "!!i j. [| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"; |
272 goal Cardinal.thy "!!i j. [| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"; |
273 by (rtac Ord_linear2 1); |
273 by (rtac Ord_linear2 1); |
274 by (REPEAT_SOME assume_tac); |
274 by (REPEAT_SOME assume_tac); |
275 by (etac (lt_trans2 RS lt_irrefl) 1); |
275 by (etac (lt_trans2 RS lt_irrefl) 1); |
276 by (etac cardinal_mono 1); |
276 by (etac cardinal_mono 1); |
277 val cardinal_lt_imp_lt = result(); |
277 qed "cardinal_lt_imp_lt"; |
278 |
278 |
279 goal Cardinal.thy "!!i j. [| |i| < K; Ord(i); Card(K) |] ==> i < K"; |
279 goal Cardinal.thy "!!i j. [| |i| < K; Ord(i); Card(K) |] ==> i < K"; |
280 by (asm_simp_tac (ZF_ss addsimps |
280 by (asm_simp_tac (ZF_ss addsimps |
281 [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); |
281 [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); |
282 val Card_lt_imp_lt = result(); |
282 qed "Card_lt_imp_lt"; |
283 |
283 |
284 goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)"; |
284 goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)"; |
285 by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1); |
285 by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1); |
286 val Card_lt_iff = result(); |
286 qed "Card_lt_iff"; |
287 |
287 |
288 goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)"; |
288 goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)"; |
289 by (asm_simp_tac (ZF_ss addsimps |
289 by (asm_simp_tac (ZF_ss addsimps |
290 [Card_lt_iff, Card_is_Ord, Ord_cardinal, |
290 [Card_lt_iff, Card_is_Ord, Ord_cardinal, |
291 not_lt_iff_le RS iff_sym]) 1); |
291 not_lt_iff_le RS iff_sym]) 1); |
292 val Card_le_iff = result(); |
292 qed "Card_le_iff"; |
293 |
293 |
294 |
294 |
295 (** The swap operator [NOT USED] **) |
295 (** The swap operator [NOT USED] **) |
296 |
296 |
297 goalw Cardinal.thy [swap_def] |
297 goalw Cardinal.thy [swap_def] |
298 "!!A. [| x:A; y:A |] ==> swap(A,x,y) : A->A"; |
298 "!!A. [| x:A; y:A |] ==> swap(A,x,y) : A->A"; |
299 by (REPEAT (ares_tac [lam_type,if_type] 1)); |
299 by (REPEAT (ares_tac [lam_type,if_type] 1)); |
300 val swap_type = result(); |
300 qed "swap_type"; |
301 |
301 |
302 goalw Cardinal.thy [swap_def] |
302 goalw Cardinal.thy [swap_def] |
303 "!!A. [| x:A; y:A; z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z"; |
303 "!!A. [| x:A; y:A; z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z"; |
304 by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
304 by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
305 val swap_swap_identity = result(); |
305 qed "swap_swap_identity"; |
306 |
306 |
307 goal Cardinal.thy "!!A. [| x:A; y:A |] ==> swap(A,x,y) : bij(A,A)"; |
307 goal Cardinal.thy "!!A. [| x:A; y:A |] ==> swap(A,x,y) : bij(A,A)"; |
308 by (rtac nilpotent_imp_bijective 1); |
308 by (rtac nilpotent_imp_bijective 1); |
309 by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2, |
309 by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2, |
310 ballI, swap_swap_identity] 1)); |
310 ballI, swap_swap_identity] 1)); |
311 val swap_bij = result(); |
311 qed "swap_bij"; |
312 |
312 |
313 (*** The finite cardinals ***) |
313 (*** The finite cardinals ***) |
314 |
314 |
315 (*Lemma suggested by Mike Fourman*) |
315 (*Lemma suggested by Mike Fourman*) |
316 val [prem] = goalw Cardinal.thy [inj_def] |
316 val [prem] = goalw Cardinal.thy [inj_def] |
324 (*Proving it's injective*) |
324 (*Proving it's injective*) |
325 by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
325 by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
326 (*Adding prem earlier would cause the simplifier to loop*) |
326 (*Adding prem earlier would cause the simplifier to loop*) |
327 by (cut_facts_tac [prem] 1); |
327 by (cut_facts_tac [prem] 1); |
328 by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1); |
328 by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1); |
329 val inj_succ_succD = result(); |
329 qed "inj_succ_succD"; |
330 |
330 |
331 val [prem] = goalw Cardinal.thy [lepoll_def] |
331 val [prem] = goalw Cardinal.thy [lepoll_def] |
332 "m:nat ==> ALL n: nat. m lepoll n --> m le n"; |
332 "m:nat ==> ALL n: nat. m lepoll n --> m le n"; |
333 by (nat_ind_tac "m" [prem] 1); |
333 by (nat_ind_tac "m" [prem] 1); |
334 by (fast_tac (ZF_cs addSIs [nat_0_le]) 1); |
334 by (fast_tac (ZF_cs addSIs [nat_0_le]) 1); |
335 by (rtac ballI 1); |
335 by (rtac ballI 1); |
336 by (eres_inst_tac [("n","n")] natE 1); |
336 by (eres_inst_tac [("n","n")] natE 1); |
337 by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1); |
337 by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1); |
338 by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1); |
338 by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1); |
339 val nat_lepoll_imp_le_lemma = result(); |
339 qed "nat_lepoll_imp_le_lemma"; |
340 val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard; |
340 val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard; |
341 |
341 |
342 goal Cardinal.thy |
342 goal Cardinal.thy |
343 "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n"; |
343 "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n"; |
344 by (rtac iffI 1); |
344 by (rtac iffI 1); |
345 by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); |
345 by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); |
346 by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym] |
346 by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym] |
347 addSEs [eqpollE]) 1); |
347 addSEs [eqpollE]) 1); |
348 val nat_eqpoll_iff = result(); |
348 qed "nat_eqpoll_iff"; |
349 |
349 |
350 goalw Cardinal.thy [Card_def,cardinal_def] |
350 goalw Cardinal.thy [Card_def,cardinal_def] |
351 "!!n. n: nat ==> Card(n)"; |
351 "!!n. n: nat ==> Card(n)"; |
352 by (rtac (Least_equality RS ssubst) 1); |
352 by (rtac (Least_equality RS ssubst) 1); |
353 by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); |
353 by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); |
354 by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); |
354 by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); |
355 by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1); |
355 by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1); |
356 val nat_into_Card = result(); |
356 qed "nat_into_Card"; |
357 |
357 |
358 (*Part of Kunen's Lemma 10.6*) |
358 (*Part of Kunen's Lemma 10.6*) |
359 goal Cardinal.thy "!!n. [| succ(n) lepoll n; n:nat |] ==> P"; |
359 goal Cardinal.thy "!!n. [| succ(n) lepoll n; n:nat |] ==> P"; |
360 by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); |
360 by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); |
361 by (REPEAT (ares_tac [nat_succI] 1)); |
361 by (REPEAT (ares_tac [nat_succI] 1)); |
362 val succ_lepoll_natE = result(); |
362 qed "succ_lepoll_natE"; |
363 |
363 |
364 |
364 |
365 (*** The first infinite cardinal: Omega, or nat ***) |
365 (*** The first infinite cardinal: Omega, or nat ***) |
366 |
366 |
367 (*This implies Kunen's Lemma 10.6*) |
367 (*This implies Kunen's Lemma 10.6*) |
369 by (rtac notI 1); |
369 by (rtac notI 1); |
370 by (rtac succ_lepoll_natE 1 THEN assume_tac 2); |
370 by (rtac succ_lepoll_natE 1 THEN assume_tac 2); |
371 by (rtac lepoll_trans 1 THEN assume_tac 2); |
371 by (rtac lepoll_trans 1 THEN assume_tac 2); |
372 by (etac ltE 1); |
372 by (etac ltE 1); |
373 by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); |
373 by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); |
374 val lt_not_lepoll = result(); |
374 qed "lt_not_lepoll"; |
375 |
375 |
376 goal Cardinal.thy "!!i n. [| Ord(i); n:nat |] ==> i eqpoll n <-> i=n"; |
376 goal Cardinal.thy "!!i n. [| Ord(i); n:nat |] ==> i eqpoll n <-> i=n"; |
377 by (rtac iffI 1); |
377 by (rtac iffI 1); |
378 by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); |
378 by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); |
379 by (rtac Ord_linear_lt 1); |
379 by (rtac Ord_linear_lt 1); |
380 by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord])); |
380 by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord])); |
381 by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN |
381 by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN |
382 REPEAT (assume_tac 1)); |
382 REPEAT (assume_tac 1)); |
383 by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1))); |
383 by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1))); |
384 by (etac eqpoll_imp_lepoll 1); |
384 by (etac eqpoll_imp_lepoll 1); |
385 val Ord_nat_eqpoll_iff = result(); |
385 qed "Ord_nat_eqpoll_iff"; |
386 |
386 |
387 goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)"; |
387 goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)"; |
388 by (rtac (Least_equality RS ssubst) 1); |
388 by (rtac (Least_equality RS ssubst) 1); |
389 by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl])); |
389 by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl])); |
390 by (etac ltE 1); |
390 by (etac ltE 1); |
391 by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1); |
391 by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1); |
392 val Card_nat = result(); |
392 qed "Card_nat"; |
393 |
393 |
394 (*Allows showing that |i| is a limit cardinal*) |
394 (*Allows showing that |i| is a limit cardinal*) |
395 goal Cardinal.thy "!!i. nat le i ==> nat le |i|"; |
395 goal Cardinal.thy "!!i. nat le i ==> nat le |i|"; |
396 by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1); |
396 by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1); |
397 by (etac cardinal_mono 1); |
397 by (etac cardinal_mono 1); |
398 val nat_le_cardinal = result(); |
398 qed "nat_le_cardinal"; |
399 |
399 |
400 |
400 |
401 (*** Towards Cardinal Arithmetic ***) |
401 (*** Towards Cardinal Arithmetic ***) |
402 (** Congruence laws for successor, cardinal addition and multiplication **) |
402 (** Congruence laws for successor, cardinal addition and multiplication **) |
403 |
403 |