1478
|
1 |
(* Title: ZF/Cardinal.thy
|
435
|
2 |
ID: $Id$
|
1478
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
435
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
|
13328
|
6 |
*)
|
13221
|
7 |
|
13328
|
8 |
header{*Cardinal Numbers Without the Axiom of Choice*}
|
435
|
9 |
|
13244
|
10 |
theory Cardinal = OrderType + Finite + Nat + Sum:
|
13221
|
11 |
|
|
12 |
constdefs
|
435
|
13 |
|
|
14 |
(*least ordinal operator*)
|
13221
|
15 |
Least :: "(i=>o) => i" (binder "LEAST " 10)
|
|
16 |
"Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
|
435
|
17 |
|
13221
|
18 |
eqpoll :: "[i,i] => o" (infixl "eqpoll" 50)
|
|
19 |
"A eqpoll B == EX f. f: bij(A,B)"
|
435
|
20 |
|
13221
|
21 |
lepoll :: "[i,i] => o" (infixl "lepoll" 50)
|
|
22 |
"A lepoll B == EX f. f: inj(A,B)"
|
435
|
23 |
|
13221
|
24 |
lesspoll :: "[i,i] => o" (infixl "lesspoll" 50)
|
|
25 |
"A lesspoll B == A lepoll B & ~(A eqpoll B)"
|
832
|
26 |
|
13221
|
27 |
cardinal :: "i=>i" ("|_|")
|
|
28 |
"|A| == LEAST i. i eqpoll A"
|
435
|
29 |
|
13221
|
30 |
Finite :: "i=>o"
|
|
31 |
"Finite(A) == EX n:nat. A eqpoll n"
|
435
|
32 |
|
13221
|
33 |
Card :: "i=>o"
|
|
34 |
"Card(i) == (i = |i|)"
|
435
|
35 |
|
9683
|
36 |
syntax (xsymbols)
|
13221
|
37 |
"eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50)
|
|
38 |
"lepoll" :: "[i,i] => o" (infixl "\<lesssim>" 50)
|
|
39 |
"lesspoll" :: "[i,i] => o" (infixl "\<prec>" 50)
|
|
40 |
"LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
|
|
41 |
|
13357
|
42 |
subsection{*The Schroeder-Bernstein Theorem*}
|
|
43 |
text{*See Davey and Priestly, page 106*}
|
13221
|
44 |
|
|
45 |
(** Lemma: Banach's Decomposition Theorem **)
|
|
46 |
|
|
47 |
lemma decomp_bnd_mono: "bnd_mono(X, %W. X - g``(Y - f``W))"
|
|
48 |
by (rule bnd_monoI, blast+)
|
|
49 |
|
|
50 |
lemma Banach_last_equation:
|
|
51 |
"g: Y->X
|
|
52 |
==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
|
|
53 |
X - lfp(X, %W. X - g``(Y - f``W))"
|
|
54 |
apply (rule_tac P = "%u. ?v = X-u"
|
|
55 |
in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
|
|
56 |
apply (simp add: double_complement fun_is_rel [THEN image_subset])
|
|
57 |
done
|
|
58 |
|
|
59 |
lemma decomposition:
|
|
60 |
"[| f: X->Y; g: Y->X |] ==>
|
|
61 |
EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &
|
|
62 |
(YA Int YB = 0) & (YA Un YB = Y) &
|
|
63 |
f``XA=YA & g``YB=XB"
|
|
64 |
apply (intro exI conjI)
|
|
65 |
apply (rule_tac [6] Banach_last_equation)
|
|
66 |
apply (rule_tac [5] refl)
|
|
67 |
apply (assumption |
|
|
68 |
rule Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+
|
|
69 |
done
|
|
70 |
|
|
71 |
lemma schroeder_bernstein:
|
|
72 |
"[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"
|
|
73 |
apply (insert decomposition [of f X Y g])
|
|
74 |
apply (simp add: inj_is_fun)
|
|
75 |
apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
|
|
76 |
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
|
|
77 |
is forced by the context!! *)
|
|
78 |
done
|
|
79 |
|
|
80 |
|
|
81 |
(** Equipollence is an equivalence relation **)
|
|
82 |
|
|
83 |
lemma bij_imp_eqpoll: "f: bij(A,B) ==> A \<approx> B"
|
|
84 |
apply (unfold eqpoll_def)
|
|
85 |
apply (erule exI)
|
|
86 |
done
|
|
87 |
|
|
88 |
(*A eqpoll A*)
|
|
89 |
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, standard, simp]
|
|
90 |
|
|
91 |
lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
|
|
92 |
apply (unfold eqpoll_def)
|
|
93 |
apply (blast intro: bij_converse_bij)
|
|
94 |
done
|
|
95 |
|
|
96 |
lemma eqpoll_trans:
|
|
97 |
"[| X \<approx> Y; Y \<approx> Z |] ==> X \<approx> Z"
|
|
98 |
apply (unfold eqpoll_def)
|
|
99 |
apply (blast intro: comp_bij)
|
|
100 |
done
|
|
101 |
|
|
102 |
(** Le-pollence is a partial ordering **)
|
|
103 |
|
|
104 |
lemma subset_imp_lepoll: "X<=Y ==> X \<lesssim> Y"
|
|
105 |
apply (unfold lepoll_def)
|
|
106 |
apply (rule exI)
|
|
107 |
apply (erule id_subset_inj)
|
|
108 |
done
|
|
109 |
|
|
110 |
lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, standard, simp]
|
|
111 |
|
|
112 |
lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll, standard]
|
|
113 |
|
|
114 |
lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
|
|
115 |
by (unfold eqpoll_def bij_def lepoll_def, blast)
|
|
116 |
|
|
117 |
lemma lepoll_trans: "[| X \<lesssim> Y; Y \<lesssim> Z |] ==> X \<lesssim> Z"
|
|
118 |
apply (unfold lepoll_def)
|
|
119 |
apply (blast intro: comp_inj)
|
|
120 |
done
|
|
121 |
|
|
122 |
(*Asymmetry law*)
|
|
123 |
lemma eqpollI: "[| X \<lesssim> Y; Y \<lesssim> X |] ==> X \<approx> Y"
|
|
124 |
apply (unfold lepoll_def eqpoll_def)
|
|
125 |
apply (elim exE)
|
|
126 |
apply (rule schroeder_bernstein, assumption+)
|
|
127 |
done
|
|
128 |
|
|
129 |
lemma eqpollE:
|
|
130 |
"[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
|
|
131 |
by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
|
|
132 |
|
|
133 |
lemma eqpoll_iff: "X \<approx> Y <-> X \<lesssim> Y & Y \<lesssim> X"
|
|
134 |
by (blast intro: eqpollI elim!: eqpollE)
|
|
135 |
|
|
136 |
lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
|
|
137 |
apply (unfold lepoll_def inj_def)
|
|
138 |
apply (blast dest: apply_type)
|
|
139 |
done
|
|
140 |
|
|
141 |
(*0 \<lesssim> Y*)
|
|
142 |
lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll, standard]
|
|
143 |
|
|
144 |
lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
|
|
145 |
by (blast intro: lepoll_0_is_0 lepoll_refl)
|
|
146 |
|
|
147 |
lemma Un_lepoll_Un:
|
|
148 |
"[| A \<lesssim> B; C \<lesssim> D; B Int D = 0 |] ==> A Un C \<lesssim> B Un D"
|
|
149 |
apply (unfold lepoll_def)
|
|
150 |
apply (blast intro: inj_disjoint_Un)
|
|
151 |
done
|
|
152 |
|
|
153 |
(*A eqpoll 0 ==> A=0*)
|
|
154 |
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0, standard]
|
|
155 |
|
|
156 |
lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
|
|
157 |
by (blast intro: eqpoll_0_is_0 eqpoll_refl)
|
|
158 |
|
|
159 |
lemma eqpoll_disjoint_Un:
|
|
160 |
"[| A \<approx> B; C \<approx> D; A Int C = 0; B Int D = 0 |]
|
|
161 |
==> A Un C \<approx> B Un D"
|
|
162 |
apply (unfold eqpoll_def)
|
|
163 |
apply (blast intro: bij_disjoint_Un)
|
|
164 |
done
|
|
165 |
|
|
166 |
|
13356
|
167 |
subsection{*lesspoll: contributions by Krzysztof Grabczewski *}
|
13221
|
168 |
|
|
169 |
lemma lesspoll_not_refl: "~ (i \<prec> i)"
|
|
170 |
by (simp add: lesspoll_def)
|
|
171 |
|
|
172 |
lemma lesspoll_irrefl [elim!]: "i \<prec> i ==> P"
|
|
173 |
by (simp add: lesspoll_def)
|
|
174 |
|
|
175 |
lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
|
|
176 |
by (unfold lesspoll_def, blast)
|
|
177 |
|
|
178 |
lemma lepoll_well_ord: "[| A \<lesssim> B; well_ord(B,r) |] ==> EX s. well_ord(A,s)"
|
|
179 |
apply (unfold lepoll_def)
|
|
180 |
apply (blast intro: well_ord_rvimage)
|
|
181 |
done
|
|
182 |
|
|
183 |
lemma lepoll_iff_leqpoll: "A \<lesssim> B <-> A \<prec> B | A \<approx> B"
|
|
184 |
apply (unfold lesspoll_def)
|
|
185 |
apply (blast intro!: eqpollI elim!: eqpollE)
|
|
186 |
done
|
|
187 |
|
|
188 |
lemma inj_not_surj_succ:
|
|
189 |
"[| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)"
|
|
190 |
apply (unfold inj_def surj_def)
|
|
191 |
apply (safe del: succE)
|
|
192 |
apply (erule swap, rule exI)
|
|
193 |
apply (rule_tac a = "lam z:A. if f`z=m then y else f`z" in CollectI)
|
|
194 |
txt{*the typing condition*}
|
|
195 |
apply (best intro!: if_type [THEN lam_type] elim: apply_funtype [THEN succE])
|
|
196 |
txt{*Proving it's injective*}
|
|
197 |
apply simp
|
|
198 |
apply blast
|
|
199 |
done
|
|
200 |
|
|
201 |
(** Variations on transitivity **)
|
|
202 |
|
|
203 |
lemma lesspoll_trans:
|
|
204 |
"[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
|
|
205 |
apply (unfold lesspoll_def)
|
|
206 |
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
|
|
207 |
done
|
|
208 |
|
|
209 |
lemma lesspoll_trans1:
|
|
210 |
"[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
|
|
211 |
apply (unfold lesspoll_def)
|
|
212 |
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
|
|
213 |
done
|
|
214 |
|
|
215 |
lemma lesspoll_trans2:
|
|
216 |
"[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
|
|
217 |
apply (unfold lesspoll_def)
|
|
218 |
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
|
|
219 |
done
|
|
220 |
|
|
221 |
|
|
222 |
(** LEAST -- the least number operator [from HOL/Univ.ML] **)
|
|
223 |
|
|
224 |
lemma Least_equality:
|
|
225 |
"[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i"
|
|
226 |
apply (unfold Least_def)
|
|
227 |
apply (rule the_equality, blast)
|
|
228 |
apply (elim conjE)
|
|
229 |
apply (erule Ord_linear_lt, assumption, blast+)
|
|
230 |
done
|
|
231 |
|
|
232 |
lemma LeastI: "[| P(i); Ord(i) |] ==> P(LEAST x. P(x))"
|
|
233 |
apply (erule rev_mp)
|
|
234 |
apply (erule_tac i=i in trans_induct)
|
|
235 |
apply (rule impI)
|
|
236 |
apply (rule classical)
|
|
237 |
apply (blast intro: Least_equality [THEN ssubst] elim!: ltE)
|
|
238 |
done
|
|
239 |
|
|
240 |
(*Proof is almost identical to the one above!*)
|
|
241 |
lemma Least_le: "[| P(i); Ord(i) |] ==> (LEAST x. P(x)) le i"
|
|
242 |
apply (erule rev_mp)
|
|
243 |
apply (erule_tac i=i in trans_induct)
|
|
244 |
apply (rule impI)
|
|
245 |
apply (rule classical)
|
|
246 |
apply (subst Least_equality, assumption+)
|
|
247 |
apply (erule_tac [2] le_refl)
|
|
248 |
apply (blast elim: ltE intro: leI ltI lt_trans1)
|
|
249 |
done
|
|
250 |
|
|
251 |
(*LEAST really is the smallest*)
|
|
252 |
lemma less_LeastE: "[| P(i); i < (LEAST x. P(x)) |] ==> Q"
|
|
253 |
apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
|
|
254 |
apply (simp add: lt_Ord)
|
|
255 |
done
|
|
256 |
|
|
257 |
(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
|
|
258 |
lemma LeastI2:
|
|
259 |
"[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
|
|
260 |
by (blast intro: LeastI )
|
|
261 |
|
|
262 |
(*If there is no such P then LEAST is vacuously 0*)
|
|
263 |
lemma Least_0:
|
|
264 |
"[| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x. P(x)) = 0"
|
|
265 |
apply (unfold Least_def)
|
|
266 |
apply (rule the_0, blast)
|
|
267 |
done
|
|
268 |
|
13356
|
269 |
lemma Ord_Least [intro,simp,TC]: "Ord(LEAST x. P(x))"
|
13221
|
270 |
apply (rule_tac P = "EX i. Ord(i) & P(i)" in case_split_thm)
|
|
271 |
(*case_tac method not available yet; needs "inductive"*)
|
|
272 |
apply safe
|
|
273 |
apply (rule Least_le [THEN ltE])
|
|
274 |
prefer 3 apply assumption+
|
|
275 |
apply (erule Least_0 [THEN ssubst])
|
|
276 |
apply (rule Ord_0)
|
|
277 |
done
|
|
278 |
|
|
279 |
|
|
280 |
(** Basic properties of cardinals **)
|
|
281 |
|
|
282 |
(*Not needed for simplification, but helpful below*)
|
|
283 |
lemma Least_cong:
|
|
284 |
"(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
|
|
285 |
by simp
|
|
286 |
|
|
287 |
(*Need AC to get X \<lesssim> Y ==> |X| le |Y|; see well_ord_lepoll_imp_Card_le
|
|
288 |
Converse also requires AC, but see well_ord_cardinal_eqE*)
|
|
289 |
lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
|
|
290 |
apply (unfold eqpoll_def cardinal_def)
|
|
291 |
apply (rule Least_cong)
|
|
292 |
apply (blast intro: comp_bij bij_converse_bij)
|
|
293 |
done
|
|
294 |
|
|
295 |
(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
|
|
296 |
lemma well_ord_cardinal_eqpoll:
|
|
297 |
"well_ord(A,r) ==> |A| \<approx> A"
|
|
298 |
apply (unfold cardinal_def)
|
|
299 |
apply (rule LeastI)
|
|
300 |
apply (erule_tac [2] Ord_ordertype)
|
|
301 |
apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_imp_eqpoll])
|
|
302 |
done
|
|
303 |
|
|
304 |
(* Ord(A) ==> |A| \<approx> A *)
|
|
305 |
lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
|
|
306 |
|
|
307 |
lemma well_ord_cardinal_eqE:
|
|
308 |
"[| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X \<approx> Y"
|
|
309 |
apply (rule eqpoll_sym [THEN eqpoll_trans])
|
|
310 |
apply (erule well_ord_cardinal_eqpoll)
|
|
311 |
apply (simp (no_asm_simp) add: well_ord_cardinal_eqpoll)
|
|
312 |
done
|
|
313 |
|
|
314 |
lemma well_ord_cardinal_eqpoll_iff:
|
|
315 |
"[| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| <-> X \<approx> Y"
|
|
316 |
by (blast intro: cardinal_cong well_ord_cardinal_eqE)
|
|
317 |
|
|
318 |
|
|
319 |
(** Observations from Kunen, page 28 **)
|
|
320 |
|
|
321 |
lemma Ord_cardinal_le: "Ord(i) ==> |i| le i"
|
|
322 |
apply (unfold cardinal_def)
|
|
323 |
apply (erule eqpoll_refl [THEN Least_le])
|
|
324 |
done
|
|
325 |
|
|
326 |
lemma Card_cardinal_eq: "Card(K) ==> |K| = K"
|
|
327 |
apply (unfold Card_def)
|
|
328 |
apply (erule sym)
|
|
329 |
done
|
|
330 |
|
|
331 |
(* Could replace the ~(j \<approx> i) by ~(i \<lesssim> j) *)
|
|
332 |
lemma CardI: "[| Ord(i); !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
|
|
333 |
apply (unfold Card_def cardinal_def)
|
|
334 |
apply (subst Least_equality)
|
|
335 |
apply (blast intro: eqpoll_refl )+
|
|
336 |
done
|
|
337 |
|
|
338 |
lemma Card_is_Ord: "Card(i) ==> Ord(i)"
|
|
339 |
apply (unfold Card_def cardinal_def)
|
|
340 |
apply (erule ssubst)
|
|
341 |
apply (rule Ord_Least)
|
|
342 |
done
|
|
343 |
|
|
344 |
lemma Card_cardinal_le: "Card(K) ==> K le |K|"
|
|
345 |
apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
|
|
346 |
done
|
|
347 |
|
|
348 |
lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
|
|
349 |
apply (unfold cardinal_def)
|
|
350 |
apply (rule Ord_Least)
|
|
351 |
done
|
|
352 |
|
|
353 |
(*The cardinals are the initial ordinals*)
|
|
354 |
lemma Card_iff_initial: "Card(K) <-> Ord(K) & (ALL j. j<K --> ~ j \<approx> K)"
|
|
355 |
apply (safe intro!: CardI Card_is_Ord)
|
|
356 |
prefer 2 apply blast
|
|
357 |
apply (unfold Card_def cardinal_def)
|
|
358 |
apply (rule less_LeastE)
|
|
359 |
apply (erule_tac [2] subst, assumption+)
|
|
360 |
done
|
|
361 |
|
|
362 |
lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a"
|
|
363 |
apply (unfold lesspoll_def)
|
|
364 |
apply (drule Card_iff_initial [THEN iffD1])
|
|
365 |
apply (blast intro!: leI [THEN le_imp_lepoll])
|
|
366 |
done
|
|
367 |
|
|
368 |
lemma Card_0: "Card(0)"
|
|
369 |
apply (rule Ord_0 [THEN CardI])
|
|
370 |
apply (blast elim!: ltE)
|
|
371 |
done
|
|
372 |
|
|
373 |
lemma Card_Un: "[| Card(K); Card(L) |] ==> Card(K Un L)"
|
|
374 |
apply (rule Ord_linear_le [of K L])
|
|
375 |
apply (simp_all add: subset_Un_iff [THEN iffD1] Card_is_Ord le_imp_subset
|
|
376 |
subset_Un_iff2 [THEN iffD1])
|
|
377 |
done
|
|
378 |
|
|
379 |
(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*)
|
|
380 |
|
|
381 |
lemma Card_cardinal: "Card(|A|)"
|
|
382 |
apply (unfold cardinal_def)
|
|
383 |
apply (rule_tac P = "EX i. Ord (i) & i \<approx> A" in case_split_thm)
|
|
384 |
txt{*degenerate case*}
|
|
385 |
prefer 2 apply (erule Least_0 [THEN ssubst], rule Card_0)
|
|
386 |
txt{*real case: A is isomorphic to some ordinal*}
|
|
387 |
apply (rule Ord_Least [THEN CardI], safe)
|
|
388 |
apply (rule less_LeastE)
|
|
389 |
prefer 2 apply assumption
|
|
390 |
apply (erule eqpoll_trans)
|
|
391 |
apply (best intro: LeastI )
|
|
392 |
done
|
|
393 |
|
|
394 |
(*Kunen's Lemma 10.5*)
|
|
395 |
lemma cardinal_eq_lemma: "[| |i| le j; j le i |] ==> |j| = |i|"
|
|
396 |
apply (rule eqpollI [THEN cardinal_cong])
|
|
397 |
apply (erule le_imp_lepoll)
|
|
398 |
apply (rule lepoll_trans)
|
|
399 |
apply (erule_tac [2] le_imp_lepoll)
|
|
400 |
apply (rule eqpoll_sym [THEN eqpoll_imp_lepoll])
|
|
401 |
apply (rule Ord_cardinal_eqpoll)
|
|
402 |
apply (elim ltE Ord_succD)
|
|
403 |
done
|
|
404 |
|
|
405 |
lemma cardinal_mono: "i le j ==> |i| le |j|"
|
|
406 |
apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le)
|
|
407 |
apply (safe intro!: Ord_cardinal le_eqI)
|
|
408 |
apply (rule cardinal_eq_lemma)
|
|
409 |
prefer 2 apply assumption
|
|
410 |
apply (erule le_trans)
|
|
411 |
apply (erule ltE)
|
|
412 |
apply (erule Ord_cardinal_le)
|
|
413 |
done
|
|
414 |
|
|
415 |
(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
|
|
416 |
lemma cardinal_lt_imp_lt: "[| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"
|
|
417 |
apply (rule Ord_linear2 [of i j], assumption+)
|
|
418 |
apply (erule lt_trans2 [THEN lt_irrefl])
|
|
419 |
apply (erule cardinal_mono)
|
|
420 |
done
|
|
421 |
|
|
422 |
lemma Card_lt_imp_lt: "[| |i| < K; Ord(i); Card(K) |] ==> i < K"
|
|
423 |
apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
|
|
424 |
done
|
|
425 |
|
|
426 |
lemma Card_lt_iff: "[| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)"
|
|
427 |
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
|
|
428 |
|
|
429 |
lemma Card_le_iff: "[| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)"
|
13269
|
430 |
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
|
13221
|
431 |
|
|
432 |
(*Can use AC or finiteness to discharge first premise*)
|
|
433 |
lemma well_ord_lepoll_imp_Card_le:
|
|
434 |
"[| well_ord(B,r); A \<lesssim> B |] ==> |A| le |B|"
|
|
435 |
apply (rule_tac i = "|A|" and j = "|B|" in Ord_linear_le)
|
|
436 |
apply (safe intro!: Ord_cardinal le_eqI)
|
|
437 |
apply (rule eqpollI [THEN cardinal_cong], assumption)
|
|
438 |
apply (rule lepoll_trans)
|
|
439 |
apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll], assumption)
|
|
440 |
apply (erule le_imp_lepoll [THEN lepoll_trans])
|
|
441 |
apply (rule eqpoll_imp_lepoll)
|
|
442 |
apply (unfold lepoll_def)
|
|
443 |
apply (erule exE)
|
|
444 |
apply (rule well_ord_cardinal_eqpoll)
|
|
445 |
apply (erule well_ord_rvimage, assumption)
|
|
446 |
done
|
|
447 |
|
|
448 |
|
|
449 |
lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| le i"
|
|
450 |
apply (rule le_trans)
|
|
451 |
apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
|
|
452 |
apply (erule Ord_cardinal_le)
|
|
453 |
done
|
|
454 |
|
|
455 |
lemma lepoll_Ord_imp_eqpoll: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<approx> A"
|
|
456 |
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
|
|
457 |
|
|
458 |
lemma lesspoll_imp_eqpoll:
|
|
459 |
"[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
|
|
460 |
apply (unfold lesspoll_def)
|
|
461 |
apply (blast intro: lepoll_Ord_imp_eqpoll)
|
|
462 |
done
|
|
463 |
|
|
464 |
|
13356
|
465 |
subsection{*The finite cardinals *}
|
13221
|
466 |
|
|
467 |
lemma cons_lepoll_consD:
|
|
468 |
"[| cons(u,A) \<lesssim> cons(v,B); u~:A; v~:B |] ==> A \<lesssim> B"
|
|
469 |
apply (unfold lepoll_def inj_def, safe)
|
|
470 |
apply (rule_tac x = "lam x:A. if f`x=v then f`u else f`x" in exI)
|
|
471 |
apply (rule CollectI)
|
|
472 |
(*Proving it's in the function space A->B*)
|
|
473 |
apply (rule if_type [THEN lam_type])
|
|
474 |
apply (blast dest: apply_funtype)
|
|
475 |
apply (blast elim!: mem_irrefl dest: apply_funtype)
|
|
476 |
(*Proving it's injective*)
|
|
477 |
apply (simp (no_asm_simp))
|
|
478 |
apply blast
|
|
479 |
done
|
|
480 |
|
|
481 |
lemma cons_eqpoll_consD: "[| cons(u,A) \<approx> cons(v,B); u~:A; v~:B |] ==> A \<approx> B"
|
|
482 |
apply (simp add: eqpoll_iff)
|
|
483 |
apply (blast intro: cons_lepoll_consD)
|
|
484 |
done
|
|
485 |
|
|
486 |
(*Lemma suggested by Mike Fourman*)
|
|
487 |
lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) ==> m \<lesssim> n"
|
|
488 |
apply (unfold succ_def)
|
|
489 |
apply (erule cons_lepoll_consD)
|
|
490 |
apply (rule mem_not_refl)+
|
|
491 |
done
|
|
492 |
|
|
493 |
lemma nat_lepoll_imp_le [rule_format]:
|
|
494 |
"m:nat ==> ALL n: nat. m \<lesssim> n --> m le n"
|
13244
|
495 |
apply (induct_tac m)
|
13221
|
496 |
apply (blast intro!: nat_0_le)
|
|
497 |
apply (rule ballI)
|
|
498 |
apply (erule_tac n = "n" in natE)
|
|
499 |
apply (simp (no_asm_simp) add: lepoll_def inj_def)
|
|
500 |
apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
|
|
501 |
done
|
|
502 |
|
|
503 |
lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n <-> m = n"
|
|
504 |
apply (rule iffI)
|
|
505 |
apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
|
|
506 |
apply (simp add: eqpoll_refl)
|
|
507 |
done
|
|
508 |
|
|
509 |
(*The object of all this work: every natural number is a (finite) cardinal*)
|
|
510 |
lemma nat_into_Card:
|
|
511 |
"n: nat ==> Card(n)"
|
|
512 |
apply (unfold Card_def cardinal_def)
|
|
513 |
apply (subst Least_equality)
|
|
514 |
apply (rule eqpoll_refl)
|
|
515 |
apply (erule nat_into_Ord)
|
|
516 |
apply (simp (no_asm_simp) add: lt_nat_in_nat [THEN nat_eqpoll_iff])
|
|
517 |
apply (blast elim!: lt_irrefl)+
|
|
518 |
done
|
|
519 |
|
|
520 |
lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
|
|
521 |
lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
|
|
522 |
|
|
523 |
|
|
524 |
(*Part of Kunen's Lemma 10.6*)
|
|
525 |
lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n; n:nat |] ==> P"
|
|
526 |
by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
|
|
527 |
|
|
528 |
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
|
|
529 |
apply (unfold lesspoll_def)
|
|
530 |
apply (fast elim!: Ord_nat [THEN [2] ltI [THEN leI, THEN le_imp_lepoll]]
|
|
531 |
eqpoll_sym [THEN eqpoll_imp_lepoll]
|
|
532 |
intro: Ord_nat [THEN [2] nat_succI [THEN ltI], THEN leI,
|
|
533 |
THEN le_imp_lepoll, THEN lepoll_trans, THEN succ_lepoll_natE])
|
|
534 |
done
|
|
535 |
|
|
536 |
lemma nat_lepoll_imp_ex_eqpoll_n:
|
|
537 |
"[| n \<in> nat; nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
|
|
538 |
apply (unfold lepoll_def eqpoll_def)
|
|
539 |
apply (fast del: subsetI subsetCE
|
|
540 |
intro!: subset_SIs
|
|
541 |
dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
|
|
542 |
elim!: restrict_bij
|
|
543 |
inj_is_fun [THEN fun_is_rel, THEN image_subset])
|
|
544 |
done
|
|
545 |
|
|
546 |
|
|
547 |
(** lepoll, \<prec> and natural numbers **)
|
|
548 |
|
|
549 |
lemma lepoll_imp_lesspoll_succ:
|
|
550 |
"[| A \<lesssim> m; m:nat |] ==> A \<prec> succ(m)"
|
|
551 |
apply (unfold lesspoll_def)
|
|
552 |
apply (rule conjI)
|
|
553 |
apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
|
|
554 |
apply (rule notI)
|
|
555 |
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
|
|
556 |
apply (drule lepoll_trans, assumption)
|
|
557 |
apply (erule succ_lepoll_natE, assumption)
|
|
558 |
done
|
|
559 |
|
|
560 |
lemma lesspoll_succ_imp_lepoll:
|
|
561 |
"[| A \<prec> succ(m); m:nat |] ==> A \<lesssim> m"
|
|
562 |
apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def, clarify)
|
|
563 |
apply (blast intro!: inj_not_surj_succ)
|
|
564 |
done
|
|
565 |
|
|
566 |
lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) <-> A \<lesssim> m"
|
|
567 |
by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
|
|
568 |
|
|
569 |
lemma lepoll_succ_disj: "[| A \<lesssim> succ(m); m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
|
|
570 |
apply (rule disjCI)
|
|
571 |
apply (rule lesspoll_succ_imp_lepoll)
|
|
572 |
prefer 2 apply assumption
|
|
573 |
apply (simp (no_asm_simp) add: lesspoll_def)
|
|
574 |
done
|
|
575 |
|
|
576 |
lemma lesspoll_cardinal_lt: "[| A \<prec> i; Ord(i) |] ==> |A| < i"
|
|
577 |
apply (unfold lesspoll_def, clarify)
|
|
578 |
apply (frule lepoll_cardinal_le, assumption)
|
|
579 |
apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
|
|
580 |
dest: lepoll_well_ord elim!: leE)
|
|
581 |
done
|
|
582 |
|
|
583 |
|
13356
|
584 |
subsection{*The first infinite cardinal: Omega, or nat *}
|
13221
|
585 |
|
|
586 |
(*This implies Kunen's Lemma 10.6*)
|
|
587 |
lemma lt_not_lepoll: "[| n<i; n:nat |] ==> ~ i \<lesssim> n"
|
|
588 |
apply (rule notI)
|
|
589 |
apply (rule succ_lepoll_natE [of n])
|
|
590 |
apply (rule lepoll_trans [of _ i])
|
|
591 |
apply (erule ltE)
|
|
592 |
apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+)
|
|
593 |
done
|
|
594 |
|
|
595 |
lemma Ord_nat_eqpoll_iff: "[| Ord(i); n:nat |] ==> i \<approx> n <-> i=n"
|
|
596 |
apply (rule iffI)
|
|
597 |
prefer 2 apply (simp add: eqpoll_refl)
|
|
598 |
apply (rule Ord_linear_lt [of i n])
|
|
599 |
apply (simp_all add: nat_into_Ord)
|
|
600 |
apply (erule lt_nat_in_nat [THEN nat_eqpoll_iff, THEN iffD1], assumption+)
|
|
601 |
apply (rule lt_not_lepoll [THEN notE], assumption+)
|
|
602 |
apply (erule eqpoll_imp_lepoll)
|
|
603 |
done
|
|
604 |
|
|
605 |
lemma Card_nat: "Card(nat)"
|
|
606 |
apply (unfold Card_def cardinal_def)
|
|
607 |
apply (subst Least_equality)
|
|
608 |
apply (rule eqpoll_refl)
|
|
609 |
apply (rule Ord_nat)
|
|
610 |
apply (erule ltE)
|
|
611 |
apply (simp_all add: eqpoll_iff lt_not_lepoll ltI)
|
|
612 |
done
|
|
613 |
|
|
614 |
(*Allows showing that |i| is a limit cardinal*)
|
|
615 |
lemma nat_le_cardinal: "nat le i ==> nat le |i|"
|
|
616 |
apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
|
|
617 |
apply (erule cardinal_mono)
|
|
618 |
done
|
|
619 |
|
|
620 |
|
13356
|
621 |
subsection{*Towards Cardinal Arithmetic *}
|
13221
|
622 |
(** Congruence laws for successor, cardinal addition and multiplication **)
|
|
623 |
|
|
624 |
(*Congruence law for cons under equipollence*)
|
|
625 |
lemma cons_lepoll_cong:
|
|
626 |
"[| A \<lesssim> B; b ~: B |] ==> cons(a,A) \<lesssim> cons(b,B)"
|
|
627 |
apply (unfold lepoll_def, safe)
|
|
628 |
apply (rule_tac x = "lam y: cons (a,A) . if y=a then b else f`y" in exI)
|
|
629 |
apply (rule_tac d = "%z. if z:B then converse (f) `z else a" in lam_injective)
|
|
630 |
apply (safe elim!: consE')
|
|
631 |
apply simp_all
|
|
632 |
apply (blast intro: inj_is_fun [THEN apply_type])+
|
|
633 |
done
|
|
634 |
|
|
635 |
lemma cons_eqpoll_cong:
|
|
636 |
"[| A \<approx> B; a ~: A; b ~: B |] ==> cons(a,A) \<approx> cons(b,B)"
|
|
637 |
by (simp add: eqpoll_iff cons_lepoll_cong)
|
|
638 |
|
|
639 |
lemma cons_lepoll_cons_iff:
|
|
640 |
"[| a ~: A; b ~: B |] ==> cons(a,A) \<lesssim> cons(b,B) <-> A \<lesssim> B"
|
|
641 |
by (blast intro: cons_lepoll_cong cons_lepoll_consD)
|
|
642 |
|
|
643 |
lemma cons_eqpoll_cons_iff:
|
|
644 |
"[| a ~: A; b ~: B |] ==> cons(a,A) \<approx> cons(b,B) <-> A \<approx> B"
|
|
645 |
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
|
|
646 |
|
|
647 |
lemma singleton_eqpoll_1: "{a} \<approx> 1"
|
|
648 |
apply (unfold succ_def)
|
|
649 |
apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
|
|
650 |
done
|
|
651 |
|
|
652 |
lemma cardinal_singleton: "|{a}| = 1"
|
|
653 |
apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans])
|
|
654 |
apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
|
|
655 |
done
|
|
656 |
|
|
657 |
lemma not_0_is_lepoll_1: "A ~= 0 ==> 1 \<lesssim> A"
|
|
658 |
apply (erule not_emptyE)
|
|
659 |
apply (rule_tac a = "cons (x, A-{x}) " in subst)
|
|
660 |
apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \<lesssim> cons (x, A-{x})" in subst)
|
|
661 |
prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto)
|
|
662 |
done
|
|
663 |
|
|
664 |
(*Congruence law for succ under equipollence*)
|
|
665 |
lemma succ_eqpoll_cong: "A \<approx> B ==> succ(A) \<approx> succ(B)"
|
|
666 |
apply (unfold succ_def)
|
|
667 |
apply (simp add: cons_eqpoll_cong mem_not_refl)
|
|
668 |
done
|
|
669 |
|
|
670 |
(*Congruence law for + under equipollence*)
|
|
671 |
lemma sum_eqpoll_cong: "[| A \<approx> C; B \<approx> D |] ==> A+B \<approx> C+D"
|
|
672 |
apply (unfold eqpoll_def)
|
|
673 |
apply (blast intro!: sum_bij)
|
|
674 |
done
|
|
675 |
|
|
676 |
(*Congruence law for * under equipollence*)
|
|
677 |
lemma prod_eqpoll_cong:
|
|
678 |
"[| A \<approx> C; B \<approx> D |] ==> A*B \<approx> C*D"
|
|
679 |
apply (unfold eqpoll_def)
|
|
680 |
apply (blast intro!: prod_bij)
|
|
681 |
done
|
|
682 |
|
|
683 |
lemma inj_disjoint_eqpoll:
|
|
684 |
"[| f: inj(A,B); A Int B = 0 |] ==> A Un (B - range(f)) \<approx> B"
|
|
685 |
apply (unfold eqpoll_def)
|
|
686 |
apply (rule exI)
|
|
687 |
apply (rule_tac c = "%x. if x:A then f`x else x"
|
|
688 |
and d = "%y. if y: range (f) then converse (f) `y else y"
|
|
689 |
in lam_bijective)
|
|
690 |
apply (blast intro!: if_type inj_is_fun [THEN apply_type])
|
|
691 |
apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
|
|
692 |
apply (safe elim!: UnE')
|
|
693 |
apply (simp_all add: inj_is_fun [THEN apply_rangeI])
|
|
694 |
apply (blast intro: inj_converse_fun [THEN apply_type])+
|
|
695 |
done
|
|
696 |
|
|
697 |
|
13356
|
698 |
subsection{*Lemmas by Krzysztof Grabczewski*}
|
|
699 |
|
|
700 |
(*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*)
|
13221
|
701 |
|
|
702 |
(*If A has at most n+1 elements and a:A then A-{a} has at most n.*)
|
|
703 |
lemma Diff_sing_lepoll:
|
|
704 |
"[| a:A; A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
|
|
705 |
apply (unfold succ_def)
|
|
706 |
apply (rule cons_lepoll_consD)
|
|
707 |
apply (rule_tac [3] mem_not_refl)
|
|
708 |
apply (erule cons_Diff [THEN ssubst], safe)
|
|
709 |
done
|
|
710 |
|
|
711 |
(*If A has at least n+1 elements then A-{a} has at least n.*)
|
|
712 |
lemma lepoll_Diff_sing:
|
|
713 |
"[| succ(n) \<lesssim> A |] ==> n \<lesssim> A - {a}"
|
|
714 |
apply (unfold succ_def)
|
|
715 |
apply (rule cons_lepoll_consD)
|
|
716 |
apply (rule_tac [2] mem_not_refl)
|
|
717 |
prefer 2 apply blast
|
|
718 |
apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
|
|
719 |
done
|
|
720 |
|
|
721 |
lemma Diff_sing_eqpoll: "[| a:A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
|
|
722 |
by (blast intro!: eqpollI
|
|
723 |
elim!: eqpollE
|
|
724 |
intro: Diff_sing_lepoll lepoll_Diff_sing)
|
|
725 |
|
|
726 |
lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a:A |] ==> A = {a}"
|
|
727 |
apply (frule Diff_sing_lepoll, assumption)
|
|
728 |
apply (drule lepoll_0_is_0)
|
|
729 |
apply (blast elim: equalityE)
|
|
730 |
done
|
|
731 |
|
|
732 |
lemma Un_lepoll_sum: "A Un B \<lesssim> A+B"
|
|
733 |
apply (unfold lepoll_def)
|
|
734 |
apply (rule_tac x = "lam x: A Un B. if x:A then Inl (x) else Inr (x) " in exI)
|
|
735 |
apply (rule_tac d = "%z. snd (z) " in lam_injective)
|
|
736 |
apply force
|
|
737 |
apply (simp add: Inl_def Inr_def)
|
|
738 |
done
|
|
739 |
|
|
740 |
lemma well_ord_Un:
|
|
741 |
"[| well_ord(X,R); well_ord(Y,S) |] ==> EX T. well_ord(X Un Y, T)"
|
|
742 |
by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]],
|
|
743 |
assumption)
|
|
744 |
|
|
745 |
(*Krzysztof Grabczewski*)
|
|
746 |
lemma disj_Un_eqpoll_sum: "A Int B = 0 ==> A Un B \<approx> A + B"
|
|
747 |
apply (unfold eqpoll_def)
|
|
748 |
apply (rule_tac x = "lam a:A Un B. if a:A then Inl (a) else Inr (a) " in exI)
|
|
749 |
apply (rule_tac d = "%z. case (%x. x, %x. x, z) " in lam_bijective)
|
|
750 |
apply auto
|
|
751 |
done
|
|
752 |
|
|
753 |
|
13244
|
754 |
subsection {*Finite and infinite sets*}
|
13221
|
755 |
|
13244
|
756 |
lemma Finite_0 [simp]: "Finite(0)"
|
13221
|
757 |
apply (unfold Finite_def)
|
|
758 |
apply (blast intro!: eqpoll_refl nat_0I)
|
|
759 |
done
|
|
760 |
|
|
761 |
lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n; n:nat |] ==> Finite(A)"
|
|
762 |
apply (unfold Finite_def)
|
|
763 |
apply (erule rev_mp)
|
|
764 |
apply (erule nat_induct)
|
|
765 |
apply (blast dest!: lepoll_0_is_0 intro!: eqpoll_refl nat_0I)
|
|
766 |
apply (blast dest!: lepoll_succ_disj)
|
|
767 |
done
|
|
768 |
|
|
769 |
lemma lesspoll_nat_is_Finite:
|
|
770 |
"A \<prec> nat ==> Finite(A)"
|
|
771 |
apply (unfold Finite_def)
|
|
772 |
apply (blast dest: ltD lesspoll_cardinal_lt
|
|
773 |
lesspoll_imp_eqpoll [THEN eqpoll_sym])
|
|
774 |
done
|
|
775 |
|
|
776 |
lemma lepoll_Finite:
|
|
777 |
"[| Y \<lesssim> X; Finite(X) |] ==> Finite(Y)"
|
|
778 |
apply (unfold Finite_def)
|
|
779 |
apply (blast elim!: eqpollE
|
|
780 |
intro: lepoll_trans [THEN lepoll_nat_imp_Finite
|
|
781 |
[unfolded Finite_def]])
|
|
782 |
done
|
|
783 |
|
|
784 |
lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite, standard]
|
|
785 |
|
|
786 |
lemmas Finite_Diff = Diff_subset [THEN subset_Finite, standard]
|
|
787 |
|
|
788 |
lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
|
|
789 |
apply (unfold Finite_def)
|
|
790 |
apply (rule_tac P = "y:x" in case_split_thm)
|
|
791 |
apply (simp add: cons_absorb)
|
|
792 |
apply (erule bexE)
|
|
793 |
apply (rule bexI)
|
|
794 |
apply (erule_tac [2] nat_succI)
|
|
795 |
apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
|
|
796 |
done
|
|
797 |
|
|
798 |
lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
|
|
799 |
apply (unfold succ_def)
|
|
800 |
apply (erule Finite_cons)
|
|
801 |
done
|
|
802 |
|
13269
|
803 |
lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
|
13244
|
804 |
by (blast intro: Finite_cons subset_Finite)
|
|
805 |
|
13269
|
806 |
lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
|
13244
|
807 |
by (simp add: succ_def)
|
|
808 |
|
13221
|
809 |
lemma nat_le_infinite_Ord:
|
|
810 |
"[| Ord(i); ~ Finite(i) |] ==> nat le i"
|
|
811 |
apply (unfold Finite_def)
|
|
812 |
apply (erule Ord_nat [THEN [2] Ord_linear2])
|
|
813 |
prefer 2 apply assumption
|
|
814 |
apply (blast intro!: eqpoll_refl elim!: ltE)
|
|
815 |
done
|
|
816 |
|
|
817 |
lemma Finite_imp_well_ord:
|
|
818 |
"Finite(A) ==> EX r. well_ord(A,r)"
|
|
819 |
apply (unfold Finite_def eqpoll_def)
|
|
820 |
apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
|
|
821 |
done
|
|
822 |
|
13244
|
823 |
lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
|
|
824 |
by (fast dest!: lepoll_0_is_0)
|
|
825 |
|
|
826 |
lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
|
|
827 |
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
|
|
828 |
|
|
829 |
lemma Finite_Fin_lemma [rule_format]:
|
|
830 |
"n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
|
|
831 |
apply (induct_tac n)
|
|
832 |
apply (rule allI)
|
|
833 |
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
|
|
834 |
apply (rule allI)
|
|
835 |
apply (rule impI)
|
|
836 |
apply (erule conjE)
|
|
837 |
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
|
|
838 |
apply (frule Diff_sing_eqpoll, assumption)
|
|
839 |
apply (erule allE)
|
|
840 |
apply (erule impE, fast)
|
|
841 |
apply (drule subsetD, assumption)
|
|
842 |
apply (drule Fin.consI, assumption)
|
|
843 |
apply (simp add: cons_Diff)
|
|
844 |
done
|
|
845 |
|
|
846 |
lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
|
|
847 |
by (unfold Finite_def, blast intro: Finite_Fin_lemma)
|
|
848 |
|
|
849 |
lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
|
|
850 |
apply (unfold Finite_def)
|
|
851 |
apply (blast intro: eqpoll_trans eqpoll_sym)
|
|
852 |
done
|
|
853 |
|
|
854 |
lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)"
|
|
855 |
apply (induct_tac n)
|
|
856 |
apply (simp add: eqpoll_0_iff, clarify)
|
|
857 |
apply (subgoal_tac "EX u. u:A")
|
|
858 |
apply (erule exE)
|
|
859 |
apply (rule Diff_sing_eqpoll [THEN revcut_rl])
|
|
860 |
prefer 2 apply assumption
|
|
861 |
apply assumption
|
|
862 |
apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
|
|
863 |
apply (rule Fin.consI, blast)
|
|
864 |
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
|
|
865 |
(*Now for the lemma assumed above*)
|
|
866 |
apply (unfold eqpoll_def)
|
|
867 |
apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
|
|
868 |
done
|
|
869 |
|
|
870 |
lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)"
|
|
871 |
apply (unfold Finite_def)
|
|
872 |
apply (blast intro: Fin_lemma)
|
|
873 |
done
|
|
874 |
|
|
875 |
lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)"
|
|
876 |
by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
|
|
877 |
|
|
878 |
lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)"
|
|
879 |
by (blast intro: Finite_into_Fin Fin_into_Finite)
|
|
880 |
|
|
881 |
lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"
|
|
882 |
by (blast intro!: Fin_into_Finite Fin_UnI
|
|
883 |
dest!: Finite_into_Fin
|
|
884 |
intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
|
|
885 |
Un_upper2 [THEN Fin_mono, THEN subsetD])
|
|
886 |
|
|
887 |
lemma Finite_Union: "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))"
|
|
888 |
apply (simp add: Finite_Fin_iff)
|
|
889 |
apply (rule Fin_UnionI)
|
|
890 |
apply (erule Fin_induct, simp)
|
|
891 |
apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
|
|
892 |
done
|
|
893 |
|
|
894 |
(* Induction principle for Finite(A), by Sidi Ehmety *)
|
13524
|
895 |
lemma Finite_induct [case_names 0 cons, induct set: Finite]:
|
13244
|
896 |
"[| Finite(A); P(0);
|
|
897 |
!! x B. [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
|
|
898 |
==> P(A)"
|
|
899 |
apply (erule Finite_into_Fin [THEN Fin_induct])
|
|
900 |
apply (blast intro: Fin_into_Finite)+
|
|
901 |
done
|
|
902 |
|
|
903 |
(*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
|
|
904 |
lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
|
|
905 |
apply (unfold Finite_def)
|
|
906 |
apply (case_tac "a:A")
|
|
907 |
apply (subgoal_tac [2] "A-{a}=A", auto)
|
|
908 |
apply (rule_tac x = "succ (n) " in bexI)
|
|
909 |
apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
|
|
910 |
apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
|
|
911 |
apply (auto dest: mem_irrefl)
|
|
912 |
done
|
|
913 |
|
|
914 |
(*Sidi Ehmety. And the contrapositive of this says
|
|
915 |
[| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
|
|
916 |
lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
|
|
917 |
apply (erule Finite_induct, auto)
|
|
918 |
apply (case_tac "x:A")
|
|
919 |
apply (subgoal_tac [2] "A-cons (x, B) = A - B")
|
|
920 |
apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
|
|
921 |
apply (rotate_tac -1, simp)
|
|
922 |
apply (drule Diff_sing_Finite, auto)
|
|
923 |
done
|
|
924 |
|
|
925 |
lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
|
|
926 |
by (erule Finite_induct, simp_all)
|
|
927 |
|
|
928 |
lemma Finite_RepFun_iff_lemma [rule_format]:
|
|
929 |
"[|Finite(x); !!x y. f(x)=f(y) ==> x=y|]
|
|
930 |
==> \<forall>A. x = RepFun(A,f) --> Finite(A)"
|
|
931 |
apply (erule Finite_induct)
|
|
932 |
apply clarify
|
|
933 |
apply (case_tac "A=0", simp)
|
|
934 |
apply (blast del: allE, clarify)
|
|
935 |
apply (subgoal_tac "\<exists>z\<in>A. x = f(z)")
|
|
936 |
prefer 2 apply (blast del: allE elim: equalityE, clarify)
|
|
937 |
apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
|
|
938 |
apply (blast intro: Diff_sing_Finite)
|
|
939 |
apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)")
|
|
940 |
apply (rule equalityI)
|
|
941 |
apply (blast intro: elim: equalityE)
|
|
942 |
apply (blast intro: elim: equalityCE)
|
|
943 |
done
|
|
944 |
|
|
945 |
text{*I don't know why, but if the premise is expressed using meta-connectives
|
|
946 |
then the simplifier cannot prove it automatically in conditional rewriting.*}
|
|
947 |
lemma Finite_RepFun_iff:
|
|
948 |
"(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
|
|
949 |
by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])
|
|
950 |
|
|
951 |
lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
|
|
952 |
apply (erule Finite_induct)
|
|
953 |
apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)
|
|
954 |
done
|
|
955 |
|
|
956 |
lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
|
|
957 |
apply (subgoal_tac "Finite({{x} . x \<in> A})")
|
|
958 |
apply (simp add: Finite_RepFun_iff )
|
|
959 |
apply (blast intro: subset_Finite)
|
|
960 |
done
|
|
961 |
|
|
962 |
lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
|
|
963 |
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
|
|
964 |
|
|
965 |
|
13221
|
966 |
|
|
967 |
(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
|
|
968 |
set is well-ordered. Proofs simplified by lcp. *)
|
|
969 |
|
|
970 |
lemma nat_wf_on_converse_Memrel: "n:nat ==> wf[n](converse(Memrel(n)))"
|
|
971 |
apply (erule nat_induct)
|
|
972 |
apply (blast intro: wf_onI)
|
|
973 |
apply (rule wf_onI)
|
|
974 |
apply (simp add: wf_on_def wf_def)
|
|
975 |
apply (rule_tac P = "x:Z" in case_split_thm)
|
|
976 |
txt{*x:Z case*}
|
|
977 |
apply (drule_tac x = x in bspec, assumption)
|
|
978 |
apply (blast elim: mem_irrefl mem_asym)
|
|
979 |
txt{*other case*}
|
|
980 |
apply (drule_tac x = "Z" in spec, blast)
|
|
981 |
done
|
|
982 |
|
|
983 |
lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
|
|
984 |
apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
|
|
985 |
apply (unfold well_ord_def)
|
|
986 |
apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel)
|
|
987 |
done
|
|
988 |
|
|
989 |
lemma well_ord_converse:
|
|
990 |
"[|well_ord(A,r);
|
|
991 |
well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) |]
|
|
992 |
==> well_ord(A,converse(r))"
|
|
993 |
apply (rule well_ord_Int_iff [THEN iffD1])
|
|
994 |
apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
|
|
995 |
apply (simp add: rvimage_converse converse_Int converse_prod
|
|
996 |
ordertype_ord_iso [THEN ord_iso_rvimage_eq])
|
|
997 |
done
|
|
998 |
|
|
999 |
lemma ordertype_eq_n:
|
|
1000 |
"[| well_ord(A,r); A \<approx> n; n:nat |] ==> ordertype(A,r)=n"
|
|
1001 |
apply (rule Ord_ordertype [THEN Ord_nat_eqpoll_iff, THEN iffD1], assumption+)
|
|
1002 |
apply (rule eqpoll_trans)
|
|
1003 |
prefer 2 apply assumption
|
|
1004 |
apply (unfold eqpoll_def)
|
|
1005 |
apply (blast intro!: ordermap_bij [THEN bij_converse_bij])
|
|
1006 |
done
|
|
1007 |
|
|
1008 |
lemma Finite_well_ord_converse:
|
|
1009 |
"[| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))"
|
|
1010 |
apply (unfold Finite_def)
|
|
1011 |
apply (rule well_ord_converse, assumption)
|
|
1012 |
apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
|
|
1013 |
done
|
|
1014 |
|
|
1015 |
lemma nat_into_Finite: "n:nat ==> Finite(n)"
|
|
1016 |
apply (unfold Finite_def)
|
|
1017 |
apply (fast intro!: eqpoll_refl)
|
|
1018 |
done
|
|
1019 |
|
|
1020 |
ML
|
|
1021 |
{*
|
|
1022 |
val Least_def = thm "Least_def";
|
|
1023 |
val eqpoll_def = thm "eqpoll_def";
|
|
1024 |
val lepoll_def = thm "lepoll_def";
|
|
1025 |
val lesspoll_def = thm "lesspoll_def";
|
|
1026 |
val cardinal_def = thm "cardinal_def";
|
|
1027 |
val Finite_def = thm "Finite_def";
|
|
1028 |
val Card_def = thm "Card_def";
|
|
1029 |
val eq_imp_not_mem = thm "eq_imp_not_mem";
|
|
1030 |
val decomp_bnd_mono = thm "decomp_bnd_mono";
|
|
1031 |
val Banach_last_equation = thm "Banach_last_equation";
|
|
1032 |
val decomposition = thm "decomposition";
|
|
1033 |
val schroeder_bernstein = thm "schroeder_bernstein";
|
|
1034 |
val bij_imp_eqpoll = thm "bij_imp_eqpoll";
|
|
1035 |
val eqpoll_refl = thm "eqpoll_refl";
|
|
1036 |
val eqpoll_sym = thm "eqpoll_sym";
|
|
1037 |
val eqpoll_trans = thm "eqpoll_trans";
|
|
1038 |
val subset_imp_lepoll = thm "subset_imp_lepoll";
|
|
1039 |
val lepoll_refl = thm "lepoll_refl";
|
|
1040 |
val le_imp_lepoll = thm "le_imp_lepoll";
|
|
1041 |
val eqpoll_imp_lepoll = thm "eqpoll_imp_lepoll";
|
|
1042 |
val lepoll_trans = thm "lepoll_trans";
|
|
1043 |
val eqpollI = thm "eqpollI";
|
|
1044 |
val eqpollE = thm "eqpollE";
|
|
1045 |
val eqpoll_iff = thm "eqpoll_iff";
|
|
1046 |
val lepoll_0_is_0 = thm "lepoll_0_is_0";
|
|
1047 |
val empty_lepollI = thm "empty_lepollI";
|
|
1048 |
val lepoll_0_iff = thm "lepoll_0_iff";
|
|
1049 |
val Un_lepoll_Un = thm "Un_lepoll_Un";
|
|
1050 |
val eqpoll_0_is_0 = thm "eqpoll_0_is_0";
|
|
1051 |
val eqpoll_0_iff = thm "eqpoll_0_iff";
|
|
1052 |
val eqpoll_disjoint_Un = thm "eqpoll_disjoint_Un";
|
|
1053 |
val lesspoll_not_refl = thm "lesspoll_not_refl";
|
|
1054 |
val lesspoll_irrefl = thm "lesspoll_irrefl";
|
|
1055 |
val lesspoll_imp_lepoll = thm "lesspoll_imp_lepoll";
|
|
1056 |
val lepoll_well_ord = thm "lepoll_well_ord";
|
|
1057 |
val lepoll_iff_leqpoll = thm "lepoll_iff_leqpoll";
|
|
1058 |
val inj_not_surj_succ = thm "inj_not_surj_succ";
|
|
1059 |
val lesspoll_trans = thm "lesspoll_trans";
|
|
1060 |
val lesspoll_trans1 = thm "lesspoll_trans1";
|
|
1061 |
val lesspoll_trans2 = thm "lesspoll_trans2";
|
|
1062 |
val Least_equality = thm "Least_equality";
|
|
1063 |
val LeastI = thm "LeastI";
|
|
1064 |
val Least_le = thm "Least_le";
|
|
1065 |
val less_LeastE = thm "less_LeastE";
|
|
1066 |
val LeastI2 = thm "LeastI2";
|
|
1067 |
val Least_0 = thm "Least_0";
|
|
1068 |
val Ord_Least = thm "Ord_Least";
|
|
1069 |
val Least_cong = thm "Least_cong";
|
|
1070 |
val cardinal_cong = thm "cardinal_cong";
|
|
1071 |
val well_ord_cardinal_eqpoll = thm "well_ord_cardinal_eqpoll";
|
|
1072 |
val Ord_cardinal_eqpoll = thm "Ord_cardinal_eqpoll";
|
|
1073 |
val well_ord_cardinal_eqE = thm "well_ord_cardinal_eqE";
|
|
1074 |
val well_ord_cardinal_eqpoll_iff = thm "well_ord_cardinal_eqpoll_iff";
|
|
1075 |
val Ord_cardinal_le = thm "Ord_cardinal_le";
|
|
1076 |
val Card_cardinal_eq = thm "Card_cardinal_eq";
|
|
1077 |
val CardI = thm "CardI";
|
|
1078 |
val Card_is_Ord = thm "Card_is_Ord";
|
|
1079 |
val Card_cardinal_le = thm "Card_cardinal_le";
|
|
1080 |
val Ord_cardinal = thm "Ord_cardinal";
|
|
1081 |
val Card_iff_initial = thm "Card_iff_initial";
|
|
1082 |
val lt_Card_imp_lesspoll = thm "lt_Card_imp_lesspoll";
|
|
1083 |
val Card_0 = thm "Card_0";
|
|
1084 |
val Card_Un = thm "Card_Un";
|
|
1085 |
val Card_cardinal = thm "Card_cardinal";
|
|
1086 |
val cardinal_mono = thm "cardinal_mono";
|
|
1087 |
val cardinal_lt_imp_lt = thm "cardinal_lt_imp_lt";
|
|
1088 |
val Card_lt_imp_lt = thm "Card_lt_imp_lt";
|
|
1089 |
val Card_lt_iff = thm "Card_lt_iff";
|
|
1090 |
val Card_le_iff = thm "Card_le_iff";
|
|
1091 |
val well_ord_lepoll_imp_Card_le = thm "well_ord_lepoll_imp_Card_le";
|
|
1092 |
val lepoll_cardinal_le = thm "lepoll_cardinal_le";
|
|
1093 |
val lepoll_Ord_imp_eqpoll = thm "lepoll_Ord_imp_eqpoll";
|
|
1094 |
val lesspoll_imp_eqpoll = thm "lesspoll_imp_eqpoll";
|
|
1095 |
val cons_lepoll_consD = thm "cons_lepoll_consD";
|
|
1096 |
val cons_eqpoll_consD = thm "cons_eqpoll_consD";
|
|
1097 |
val succ_lepoll_succD = thm "succ_lepoll_succD";
|
|
1098 |
val nat_lepoll_imp_le = thm "nat_lepoll_imp_le";
|
|
1099 |
val nat_eqpoll_iff = thm "nat_eqpoll_iff";
|
|
1100 |
val nat_into_Card = thm "nat_into_Card";
|
|
1101 |
val cardinal_0 = thm "cardinal_0";
|
|
1102 |
val cardinal_1 = thm "cardinal_1";
|
|
1103 |
val succ_lepoll_natE = thm "succ_lepoll_natE";
|
|
1104 |
val n_lesspoll_nat = thm "n_lesspoll_nat";
|
|
1105 |
val nat_lepoll_imp_ex_eqpoll_n = thm "nat_lepoll_imp_ex_eqpoll_n";
|
|
1106 |
val lepoll_imp_lesspoll_succ = thm "lepoll_imp_lesspoll_succ";
|
|
1107 |
val lesspoll_succ_imp_lepoll = thm "lesspoll_succ_imp_lepoll";
|
|
1108 |
val lesspoll_succ_iff = thm "lesspoll_succ_iff";
|
|
1109 |
val lepoll_succ_disj = thm "lepoll_succ_disj";
|
|
1110 |
val lesspoll_cardinal_lt = thm "lesspoll_cardinal_lt";
|
|
1111 |
val lt_not_lepoll = thm "lt_not_lepoll";
|
|
1112 |
val Ord_nat_eqpoll_iff = thm "Ord_nat_eqpoll_iff";
|
|
1113 |
val Card_nat = thm "Card_nat";
|
|
1114 |
val nat_le_cardinal = thm "nat_le_cardinal";
|
|
1115 |
val cons_lepoll_cong = thm "cons_lepoll_cong";
|
|
1116 |
val cons_eqpoll_cong = thm "cons_eqpoll_cong";
|
|
1117 |
val cons_lepoll_cons_iff = thm "cons_lepoll_cons_iff";
|
|
1118 |
val cons_eqpoll_cons_iff = thm "cons_eqpoll_cons_iff";
|
|
1119 |
val singleton_eqpoll_1 = thm "singleton_eqpoll_1";
|
|
1120 |
val cardinal_singleton = thm "cardinal_singleton";
|
|
1121 |
val not_0_is_lepoll_1 = thm "not_0_is_lepoll_1";
|
|
1122 |
val succ_eqpoll_cong = thm "succ_eqpoll_cong";
|
|
1123 |
val sum_eqpoll_cong = thm "sum_eqpoll_cong";
|
|
1124 |
val prod_eqpoll_cong = thm "prod_eqpoll_cong";
|
|
1125 |
val inj_disjoint_eqpoll = thm "inj_disjoint_eqpoll";
|
|
1126 |
val Diff_sing_lepoll = thm "Diff_sing_lepoll";
|
|
1127 |
val lepoll_Diff_sing = thm "lepoll_Diff_sing";
|
|
1128 |
val Diff_sing_eqpoll = thm "Diff_sing_eqpoll";
|
|
1129 |
val lepoll_1_is_sing = thm "lepoll_1_is_sing";
|
|
1130 |
val Un_lepoll_sum = thm "Un_lepoll_sum";
|
|
1131 |
val well_ord_Un = thm "well_ord_Un";
|
|
1132 |
val disj_Un_eqpoll_sum = thm "disj_Un_eqpoll_sum";
|
|
1133 |
val Finite_0 = thm "Finite_0";
|
|
1134 |
val lepoll_nat_imp_Finite = thm "lepoll_nat_imp_Finite";
|
|
1135 |
val lesspoll_nat_is_Finite = thm "lesspoll_nat_is_Finite";
|
|
1136 |
val lepoll_Finite = thm "lepoll_Finite";
|
|
1137 |
val subset_Finite = thm "subset_Finite";
|
|
1138 |
val Finite_Diff = thm "Finite_Diff";
|
|
1139 |
val Finite_cons = thm "Finite_cons";
|
|
1140 |
val Finite_succ = thm "Finite_succ";
|
|
1141 |
val nat_le_infinite_Ord = thm "nat_le_infinite_Ord";
|
|
1142 |
val Finite_imp_well_ord = thm "Finite_imp_well_ord";
|
|
1143 |
val nat_wf_on_converse_Memrel = thm "nat_wf_on_converse_Memrel";
|
|
1144 |
val nat_well_ord_converse_Memrel = thm "nat_well_ord_converse_Memrel";
|
|
1145 |
val well_ord_converse = thm "well_ord_converse";
|
|
1146 |
val ordertype_eq_n = thm "ordertype_eq_n";
|
|
1147 |
val Finite_well_ord_converse = thm "Finite_well_ord_converse";
|
|
1148 |
val nat_into_Finite = thm "nat_into_Finite";
|
|
1149 |
*}
|
9683
|
1150 |
|
435
|
1151 |
end
|