author  paulson 
Sun, 14 Jul 2002 15:14:43 +0200  
changeset 13356  c9cfe1638bf2 
parent 13328  703de709a64b 
child 13615  449a70d88b38 
permissions  rwrr 
1478  1 
(* Title: ZF/CardinalArith.thy 
437  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
437  4 
Copyright 1994 University of Cambridge 
5 

13328  6 
*) 
13216  7 

13328  8 
header{*Cardinal Arithmetic Without the Axiom of Choice*} 
437  9 

12667  10 
theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite: 
467  11 

12667  12 
constdefs 
437  13 

12667  14 
InfCard :: "i=>o" 
15 
"InfCard(i) == Card(i) & nat le i" 

437  16 

12667  17 
cmult :: "[i,i]=>i" (infixl "*" 70) 
18 
"i * j == i*j" 

19 

20 
cadd :: "[i,i]=>i" (infixl "+" 65) 

21 
"i + j == i+j" 

437  22 

12667  23 
csquare_rel :: "i=>i" 
24 
"csquare_rel(K) == 

25 
rvimage(K*K, 

26 
lam <x,y>:K*K. <x Un y, x, y>, 

27 
rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" 

437  28 

484  29 
(*This def is more complex than Kunen's but it more easily proved to 
30 
be a cardinal*) 

12667  31 
jump_cardinal :: "i=>i" 
32 
"jump_cardinal(K) == 

1155  33 
UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" 
12667  34 

484  35 
(*needed because jump_cardinal(K) might not be the successor of K*) 
12667  36 
csucc :: "i=>i" 
37 
"csucc(K) == LEAST L. Card(L) & K<L" 

484  38 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9964
diff
changeset

39 
syntax (xsymbols) 
12667  40 
"op +" :: "[i,i] => i" (infixl "\<oplus>" 65) 
41 
"op *" :: "[i,i] => i" (infixl "\<otimes>" 70) 

42 

43 

44 
lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))" 

45 
apply (rule CardI) 

46 
apply (simp add: Card_is_Ord) 

47 
apply (clarify dest!: ltD) 

48 
apply (drule bspec, assumption) 

49 
apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 

50 
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) 

51 
apply (drule lesspoll_trans1, assumption) 

13216  52 
apply (subgoal_tac "B \<lesssim> \<Union>A") 
12667  53 
apply (drule lesspoll_trans1, assumption, blast) 
54 
apply (blast intro: subset_imp_lepoll) 

55 
done 

56 

57 
lemma Card_UN: 

58 
"(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" 

59 
by (blast intro: Card_Union) 

60 

61 
lemma Card_OUN [simp,intro,TC]: 

62 
"(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))" 

63 
by (simp add: OUnion_def Card_0) 

9654
9754ba005b64
Xsymbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9548
diff
changeset

64 

12776  65 
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat" 
66 
apply (unfold lesspoll_def) 

67 
apply (rule conjI) 

68 
apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat) 

69 
apply (rule notI) 

70 
apply (erule eqpollE) 

71 
apply (rule succ_lepoll_natE) 

72 
apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 

12820  73 
lepoll_trans, assumption) 
12776  74 
done 
75 

76 
lemma in_Card_imp_lesspoll: "[ Card(K); b \<in> K ] ==> b \<prec> K" 

77 
apply (unfold lesspoll_def) 

78 
apply (simp add: Card_iff_initial) 

79 
apply (fast intro!: le_imp_lepoll ltI leI) 

80 
done 

81 

82 
lemma lesspoll_lemma: 

83 
"[ ~ A \<prec> B; C \<prec> B ] ==> A  C \<noteq> 0" 

84 
apply (unfold lesspoll_def) 

85 
apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll] 

86 
intro!: eqpollI elim: notE 

87 
elim!: eqpollE lepoll_trans) 

88 
done 

89 

13216  90 

13356  91 
subsection{*Cardinal addition*} 
13216  92 

13328  93 
text{*Note: Could omit proving the algebraic laws for cardinal addition and 
94 
multiplication. On finite cardinals these operations coincide with 

95 
addition and multiplication of natural numbers; on infinite cardinals they 

96 
coincide with union (maximum). Either way we get most laws for free.*} 

97 

13216  98 
(** Cardinal addition is commutative **) 
99 

100 
lemma sum_commute_eqpoll: "A+B \<approx> B+A" 

101 
apply (unfold eqpoll_def) 

102 
apply (rule exI) 

103 
apply (rule_tac c = "case(Inr,Inl)" and d = "case(Inr,Inl)" in lam_bijective) 

104 
apply auto 

105 
done 

106 

107 
lemma cadd_commute: "i + j = j + i" 

108 
apply (unfold cadd_def) 

109 
apply (rule sum_commute_eqpoll [THEN cardinal_cong]) 

110 
done 

111 

112 
(** Cardinal addition is associative **) 

113 

114 
lemma sum_assoc_eqpoll: "(A+B)+C \<approx> A+(B+C)" 

115 
apply (unfold eqpoll_def) 

116 
apply (rule exI) 

117 
apply (rule sum_assoc_bij) 

118 
done 

119 

120 
(*Unconditional version requires AC*) 

121 
lemma well_ord_cadd_assoc: 

122 
"[ well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) ] 

123 
==> (i + j) + k = i + (j + k)" 

124 
apply (unfold cadd_def) 

125 
apply (rule cardinal_cong) 

126 
apply (rule eqpoll_trans) 

127 
apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 

13221  128 
apply (blast intro: well_ord_radd ) 
13216  129 
apply (rule sum_assoc_eqpoll [THEN eqpoll_trans]) 
130 
apply (rule eqpoll_sym) 

131 
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

13221  132 
apply (blast intro: well_ord_radd ) 
13216  133 
done 
134 

135 
(** 0 is the identity for addition **) 

136 

137 
lemma sum_0_eqpoll: "0+A \<approx> A" 

138 
apply (unfold eqpoll_def) 

139 
apply (rule exI) 

140 
apply (rule bij_0_sum) 

141 
done 

142 

143 
lemma cadd_0 [simp]: "Card(K) ==> 0 + K = K" 

144 
apply (unfold cadd_def) 

145 
apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq) 

146 
done 

147 

148 
(** Addition by another cardinal **) 

149 

150 
lemma sum_lepoll_self: "A \<lesssim> A+B" 

151 
apply (unfold lepoll_def inj_def) 

152 
apply (rule_tac x = "lam x:A. Inl (x) " in exI) 

13221  153 
apply simp 
13216  154 
done 
155 

156 
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*) 

157 

158 
lemma cadd_le_self: 

159 
"[ Card(K); Ord(L) ] ==> K le (K + L)" 

160 
apply (unfold cadd_def) 

13221  161 
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le], 
162 
assumption) 

13216  163 
apply (rule_tac [2] sum_lepoll_self) 
164 
apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord) 

165 
done 

166 

167 
(** Monotonicity of addition **) 

168 

169 
lemma sum_lepoll_mono: 

13221  170 
"[ A \<lesssim> C; B \<lesssim> D ] ==> A + B \<lesssim> C + D" 
13216  171 
apply (unfold lepoll_def) 
13221  172 
apply (elim exE) 
13216  173 
apply (rule_tac x = "lam z:A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI) 
13221  174 
apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) ` y))" 
13216  175 
in lam_injective) 
13221  176 
apply (typecheck add: inj_is_fun, auto) 
13216  177 
done 
178 

179 
lemma cadd_le_mono: 

180 
"[ K' le K; L' le L ] ==> (K' + L') le (K + L)" 

181 
apply (unfold cadd_def) 

182 
apply (safe dest!: le_subset_iff [THEN iffD1]) 

183 
apply (rule well_ord_lepoll_imp_Card_le) 

184 
apply (blast intro: well_ord_radd well_ord_Memrel) 

185 
apply (blast intro: sum_lepoll_mono subset_imp_lepoll) 

186 
done 

187 

188 
(** Addition of finite cardinals is "ordinary" addition **) 

189 

190 
lemma sum_succ_eqpoll: "succ(A)+B \<approx> succ(A+B)" 

191 
apply (unfold eqpoll_def) 

192 
apply (rule exI) 

193 
apply (rule_tac c = "%z. if z=Inl (A) then A+B else z" 

194 
and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective) 

13221  195 
apply simp_all 
13216  196 
apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+ 
197 
done 

198 

199 
(*Pulling the succ(...) outside the ... requires m, n: nat *) 

200 
(*Unconditional version requires AC*) 

201 
lemma cadd_succ_lemma: 

202 
"[ Ord(m); Ord(n) ] ==> succ(m) + n = succ(m + n)" 

203 
apply (unfold cadd_def) 

204 
apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans]) 

205 
apply (rule succ_eqpoll_cong [THEN cardinal_cong]) 

206 
apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym]) 

207 
apply (blast intro: well_ord_radd well_ord_Memrel) 

208 
done 

209 

210 
lemma nat_cadd_eq_add: "[ m: nat; n: nat ] ==> m + n = m#+n" 

13244  211 
apply (induct_tac m) 
13216  212 
apply (simp add: nat_into_Card [THEN cadd_0]) 
213 
apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq]) 

214 
done 

215 

216 

13356  217 
subsection{*Cardinal multiplication*} 
13216  218 

219 
(** Cardinal multiplication is commutative **) 

220 

221 
(*Easier to prove the two directions separately*) 

222 
lemma prod_commute_eqpoll: "A*B \<approx> B*A" 

223 
apply (unfold eqpoll_def) 

224 
apply (rule exI) 

13221  225 
apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective, 
226 
auto) 

13216  227 
done 
228 

229 
lemma cmult_commute: "i * j = j * i" 

230 
apply (unfold cmult_def) 

231 
apply (rule prod_commute_eqpoll [THEN cardinal_cong]) 

232 
done 

233 

234 
(** Cardinal multiplication is associative **) 

235 

236 
lemma prod_assoc_eqpoll: "(A*B)*C \<approx> A*(B*C)" 

237 
apply (unfold eqpoll_def) 

238 
apply (rule exI) 

239 
apply (rule prod_assoc_bij) 

240 
done 

241 

242 
(*Unconditional version requires AC*) 

243 
lemma well_ord_cmult_assoc: 

244 
"[ well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) ] 

245 
==> (i * j) * k = i * (j * k)" 

246 
apply (unfold cmult_def) 

247 
apply (rule cardinal_cong) 

13221  248 
apply (rule eqpoll_trans) 
13216  249 
apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 
250 
apply (blast intro: well_ord_rmult) 

251 
apply (rule prod_assoc_eqpoll [THEN eqpoll_trans]) 

13221  252 
apply (rule eqpoll_sym) 
13216  253 
apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 
254 
apply (blast intro: well_ord_rmult) 

255 
done 

256 

257 
(** Cardinal multiplication distributes over addition **) 

258 

259 
lemma sum_prod_distrib_eqpoll: "(A+B)*C \<approx> (A*C)+(B*C)" 

260 
apply (unfold eqpoll_def) 

261 
apply (rule exI) 

262 
apply (rule sum_prod_distrib_bij) 

263 
done 

264 

265 
lemma well_ord_cadd_cmult_distrib: 

266 
"[ well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) ] 

267 
==> (i + j) * k = (i * k) + (j * k)" 

268 
apply (unfold cadd_def cmult_def) 

269 
apply (rule cardinal_cong) 

13221  270 
apply (rule eqpoll_trans) 
13216  271 
apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 
272 
apply (blast intro: well_ord_radd) 

273 
apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans]) 

13221  274 
apply (rule eqpoll_sym) 
13216  275 
apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll 
276 
well_ord_cardinal_eqpoll]) 

277 
apply (blast intro: well_ord_rmult)+ 

278 
done 

279 

280 
(** Multiplication by 0 yields 0 **) 

281 

282 
lemma prod_0_eqpoll: "0*A \<approx> 0" 

283 
apply (unfold eqpoll_def) 

284 
apply (rule exI) 

13221  285 
apply (rule lam_bijective, safe) 
13216  286 
done 
287 

288 
lemma cmult_0 [simp]: "0 * i = 0" 

13221  289 
by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong]) 
13216  290 

291 
(** 1 is the identity for multiplication **) 

292 

293 
lemma prod_singleton_eqpoll: "{x}*A \<approx> A" 

294 
apply (unfold eqpoll_def) 

295 
apply (rule exI) 

296 
apply (rule singleton_prod_bij [THEN bij_converse_bij]) 

297 
done 

298 

299 
lemma cmult_1 [simp]: "Card(K) ==> 1 * K = K" 

300 
apply (unfold cmult_def succ_def) 

301 
apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq) 

302 
done 

303 

13356  304 
subsection{*Some inequalities for multiplication*} 
13216  305 

306 
lemma prod_square_lepoll: "A \<lesssim> A*A" 

307 
apply (unfold lepoll_def inj_def) 

13221  308 
apply (rule_tac x = "lam x:A. <x,x>" in exI, simp) 
13216  309 
done 
310 

311 
(*Could probably weaken the premise to well_ord(K,r), or remove using AC*) 

312 
lemma cmult_square_le: "Card(K) ==> K le K * K" 

313 
apply (unfold cmult_def) 

314 
apply (rule le_trans) 

315 
apply (rule_tac [2] well_ord_lepoll_imp_Card_le) 

316 
apply (rule_tac [3] prod_square_lepoll) 

13221  317 
apply (simp add: le_refl Card_is_Ord Card_cardinal_eq) 
318 
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) 

13216  319 
done 
320 

321 
(** Multiplication by a nonzero cardinal **) 

322 

323 
lemma prod_lepoll_self: "b: B ==> A \<lesssim> A*B" 

324 
apply (unfold lepoll_def inj_def) 

13221  325 
apply (rule_tac x = "lam x:A. <x,b>" in exI, simp) 
13216  326 
done 
327 

328 
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*) 

329 
lemma cmult_le_self: 

330 
"[ Card(K); Ord(L); 0<L ] ==> K le (K * L)" 

331 
apply (unfold cmult_def) 

332 
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le]) 

13221  333 
apply assumption 
13216  334 
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) 
335 
apply (blast intro: prod_lepoll_self ltD) 

336 
done 

337 

338 
(** Monotonicity of multiplication **) 

339 

340 
lemma prod_lepoll_mono: 

341 
"[ A \<lesssim> C; B \<lesssim> D ] ==> A * B \<lesssim> C * D" 

342 
apply (unfold lepoll_def) 

13221  343 
apply (elim exE) 
13216  344 
apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in exI) 
345 
apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>" 

346 
in lam_injective) 

13221  347 
apply (typecheck add: inj_is_fun, auto) 
13216  348 
done 
349 

350 
lemma cmult_le_mono: 

351 
"[ K' le K; L' le L ] ==> (K' * L') le (K * L)" 

352 
apply (unfold cmult_def) 

353 
apply (safe dest!: le_subset_iff [THEN iffD1]) 

354 
apply (rule well_ord_lepoll_imp_Card_le) 

355 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

356 
apply (blast intro: prod_lepoll_mono subset_imp_lepoll) 

357 
done 

358 

13356  359 
subsection{*Multiplication of finite cardinals is "ordinary" multiplication*} 
13216  360 

361 
lemma prod_succ_eqpoll: "succ(A)*B \<approx> B + A*B" 

362 
apply (unfold eqpoll_def) 

13221  363 
apply (rule exI) 
13216  364 
apply (rule_tac c = "%<x,y>. if x=A then Inl (y) else Inr (<x,y>)" 
365 
and d = "case (%y. <A,y>, %z. z)" in lam_bijective) 

366 
apply safe 

367 
apply (simp_all add: succI2 if_type mem_imp_not_eq) 

368 
done 

369 

370 
(*Unconditional version requires AC*) 

371 
lemma cmult_succ_lemma: 

372 
"[ Ord(m); Ord(n) ] ==> succ(m) * n = n + (m * n)" 

373 
apply (unfold cmult_def cadd_def) 

374 
apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans]) 

375 
apply (rule cardinal_cong [symmetric]) 

376 
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

377 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

378 
done 

379 

380 
lemma nat_cmult_eq_mult: "[ m: nat; n: nat ] ==> m * n = m#*n" 

13244  381 
apply (induct_tac m) 
13221  382 
apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add) 
13216  383 
done 
384 

385 
lemma cmult_2: "Card(n) ==> 2 * n = n + n" 

13221  386 
by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0]) 
13216  387 

388 
lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B" 

13221  389 
apply (rule lepoll_trans) 
13216  390 
apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll]) 
391 
apply (erule prod_lepoll_mono) 

13221  392 
apply (rule lepoll_refl) 
13216  393 
done 
394 

395 
lemma lepoll_imp_sum_lepoll_prod: "[ A \<lesssim> B; 2 \<lesssim> A ] ==> A+B \<lesssim> A*B" 

13221  396 
by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl) 
13216  397 

398 

13356  399 
subsection{*Infinite Cardinals are Limit Ordinals*} 
13216  400 

401 
(*This proof is modelled upon one assuming nat<=A, with injection 

402 
lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z 

403 
and inverse %y. if y:nat then nat_case(u, %z. z, y) else y. \ 

404 
If f: inj(nat,A) then range(f) behaves like the natural numbers.*) 

405 
lemma nat_cons_lepoll: "nat \<lesssim> A ==> cons(u,A) \<lesssim> A" 

406 
apply (unfold lepoll_def) 

407 
apply (erule exE) 

408 
apply (rule_tac x = 

409 
"lam z:cons (u,A). 

410 
if z=u then f`0 

411 
else if z: range (f) then f`succ (converse (f) `z) else z" 

412 
in exI) 

413 
apply (rule_tac d = 

414 
"%y. if y: range(f) then nat_case (u, %z. f`z, converse(f) `y) 

415 
else y" 

416 
in lam_injective) 

417 
apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun) 

418 
apply (simp add: inj_is_fun [THEN apply_rangeI] 

419 
inj_converse_fun [THEN apply_rangeI] 

420 
inj_converse_fun [THEN apply_funtype]) 

421 
done 

422 

423 
lemma nat_cons_eqpoll: "nat \<lesssim> A ==> cons(u,A) \<approx> A" 

424 
apply (erule nat_cons_lepoll [THEN eqpollI]) 

425 
apply (rule subset_consI [THEN subset_imp_lepoll]) 

426 
done 

427 

428 
(*Specialized version required below*) 

429 
lemma nat_succ_eqpoll: "nat <= A ==> succ(A) \<approx> A" 

430 
apply (unfold succ_def) 

431 
apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll]) 

432 
done 

433 

434 
lemma InfCard_nat: "InfCard(nat)" 

435 
apply (unfold InfCard_def) 

436 
apply (blast intro: Card_nat le_refl Card_is_Ord) 

437 
done 

438 

439 
lemma InfCard_is_Card: "InfCard(K) ==> Card(K)" 

440 
apply (unfold InfCard_def) 

441 
apply (erule conjunct1) 

442 
done 

443 

444 
lemma InfCard_Un: 

445 
"[ InfCard(K); Card(L) ] ==> InfCard(K Un L)" 

446 
apply (unfold InfCard_def) 

447 
apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans] Card_is_Ord) 

448 
done 

449 

450 
(*Kunen's Lemma 10.11*) 

451 
lemma InfCard_is_Limit: "InfCard(K) ==> Limit(K)" 

452 
apply (unfold InfCard_def) 

453 
apply (erule conjE) 

454 
apply (frule Card_is_Ord) 

455 
apply (rule ltI [THEN non_succ_LimitI]) 

456 
apply (erule le_imp_subset [THEN subsetD]) 

457 
apply (safe dest!: Limit_nat [THEN Limit_le_succD]) 

458 
apply (unfold Card_def) 

459 
apply (drule trans) 

460 
apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong]) 

461 
apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl]) 

13221  462 
apply (rule le_eqI, assumption) 
13216  463 
apply (rule Ord_cardinal) 
464 
done 

465 

466 

467 
(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***) 

468 

469 
(*A general fact about ordermap*) 

470 
lemma ordermap_eqpoll_pred: 

13269  471 
"[ well_ord(A,r); x:A ] ==> ordermap(A,r)`x \<approx> Order.pred(A,x,r)" 
13216  472 
apply (unfold eqpoll_def) 
473 
apply (rule exI) 

13221  474 
apply (simp add: ordermap_eq_image well_ord_is_wf) 
475 
apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, 

476 
THEN bij_converse_bij]) 

13216  477 
apply (rule pred_subset) 
478 
done 

479 

480 
(** Establishing the wellordering **) 

481 

482 
lemma csquare_lam_inj: 

483 
"Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)" 

484 
apply (unfold inj_def) 

485 
apply (force intro: lam_type Un_least_lt [THEN ltD] ltI) 

486 
done 

487 

488 
lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))" 

489 
apply (unfold csquare_rel_def) 

13221  490 
apply (rule csquare_lam_inj [THEN well_ord_rvimage], assumption) 
13216  491 
apply (blast intro: well_ord_rmult well_ord_Memrel) 
492 
done 

493 

494 
(** Characterising initial segments of the wellordering **) 

495 

496 
lemma csquareD: 

497 
"[ <<x,y>, <z,z>> : csquare_rel(K); x<K; y<K; z<K ] ==> x le z & y le z" 

498 
apply (unfold csquare_rel_def) 

499 
apply (erule rev_mp) 

500 
apply (elim ltE) 

13221  501 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  502 
apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le) 
13221  503 
apply (simp_all add: lt_def succI2) 
13216  504 
done 
505 

506 
lemma pred_csquare_subset: 

13269  507 
"z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)" 
13216  508 
apply (unfold Order.pred_def) 
509 
apply (safe del: SigmaI succCI) 

510 
apply (erule csquareD [THEN conjE]) 

13221  511 
apply (unfold lt_def, auto) 
13216  512 
done 
513 

514 
lemma csquare_ltI: 

515 
"[ x<z; y<z; z<K ] ==> <<x,y>, <z,z>> : csquare_rel(K)" 

516 
apply (unfold csquare_rel_def) 

517 
apply (subgoal_tac "x<K & y<K") 

518 
prefer 2 apply (blast intro: lt_trans) 

519 
apply (elim ltE) 

13221  520 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  521 
done 
522 

523 
(*Part of the traditional proof. UNUSED since it's harder to prove & apply *) 

524 
lemma csquare_or_eqI: 

525 
"[ x le z; y le z; z<K ] ==> <<x,y>, <z,z>> : csquare_rel(K)  x=z & y=z" 

526 
apply (unfold csquare_rel_def) 

527 
apply (subgoal_tac "x<K & y<K") 

528 
prefer 2 apply (blast intro: lt_trans1) 

529 
apply (elim ltE) 

13221  530 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  531 
apply (elim succE) 
13221  532 
apply (simp_all add: subset_Un_iff [THEN iff_sym] 
533 
subset_Un_iff2 [THEN iff_sym] OrdmemD) 

13216  534 
done 
535 

536 
(** The cardinality of initial segments **) 

537 

538 
lemma ordermap_z_lt: 

539 
"[ Limit(K); x<K; y<K; z=succ(x Un y) ] ==> 

540 
ordermap(K*K, csquare_rel(K)) ` <x,y> < 

541 
ordermap(K*K, csquare_rel(K)) ` <z,z>" 

542 
apply (subgoal_tac "z<K & well_ord (K*K, csquare_rel (K))") 

543 
prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ 

13221  544 
Limit_is_Ord [THEN well_ord_csquare], clarify) 
13216  545 
apply (rule csquare_ltI [THEN ordermap_mono, THEN ltI]) 
546 
apply (erule_tac [4] well_ord_is_wf) 

547 
apply (blast intro!: Un_upper1_le Un_upper2_le Ord_ordermap elim!: ltE)+ 

548 
done 

549 

550 
(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *) 

551 
lemma ordermap_csquare_le: 

13221  552 
"[ Limit(K); x<K; y<K; z=succ(x Un y) ] 
553 
==>  ordermap(K*K, csquare_rel(K)) ` <x,y>  le succ(z) * succ(z)" 

13216  554 
apply (unfold cmult_def) 
555 
apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le]) 

556 
apply (rule Ord_cardinal [THEN well_ord_Memrel])+ 

557 
apply (subgoal_tac "z<K") 

558 
prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ) 

13221  559 
apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans], 
560 
assumption+) 

13216  561 
apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) 
562 
apply (erule Limit_is_Ord [THEN well_ord_csquare]) 

563 
apply (blast intro: ltD) 

564 
apply (rule pred_csquare_subset [THEN subset_imp_lepoll, THEN lepoll_trans], 

565 
assumption) 

566 
apply (elim ltE) 

567 
apply (rule prod_eqpoll_cong [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]) 

568 
apply (erule Ord_succ [THEN Ord_cardinal_eqpoll])+ 

569 
done 

570 

571 
(*Kunen: "... so the order type <= K" *) 

572 
lemma ordertype_csquare_le: 

573 
"[ InfCard(K); ALL y:K. InfCard(y) > y * y = y ] 

574 
==> ordertype(K*K, csquare_rel(K)) le K" 

575 
apply (frule InfCard_is_Card [THEN Card_is_Ord]) 

13221  576 
apply (rule all_lt_imp_le, assumption) 
13216  577 
apply (erule well_ord_csquare [THEN Ord_ordertype]) 
578 
apply (rule Card_lt_imp_lt) 

579 
apply (erule_tac [3] InfCard_is_Card) 

580 
apply (erule_tac [2] ltE) 

581 
apply (simp add: ordertype_unfold) 

582 
apply (safe elim!: ltE) 

583 
apply (subgoal_tac "Ord (xa) & Ord (ya)") 

13221  584 
prefer 2 apply (blast intro: Ord_in_Ord, clarify) 
13216  585 
(*??WHAT A MESS!*) 
586 
apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1], 

587 
(assumption  rule refl  erule ltI)+) 

588 
apply (rule_tac i = "xa Un ya" and j = "nat" in Ord_linear2, 

589 
simp_all add: Ord_Un Ord_nat) 

590 
prefer 2 (*case nat le (xa Un ya) *) 

591 
apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] 

592 
le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un 

593 
ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD]) 

594 
(*the finite case: xa Un ya < nat *) 

595 
apply (rule_tac j = "nat" in lt_trans2) 

596 
apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type 

597 
nat_into_Card [THEN Card_cardinal_eq] Ord_nat) 

598 
apply (simp add: InfCard_def) 

599 
done 

600 

601 
(*Main result: Kunen's Theorem 10.12*) 

602 
lemma InfCard_csquare_eq: "InfCard(K) ==> K * K = K" 

603 
apply (frule InfCard_is_Card [THEN Card_is_Ord]) 

604 
apply (erule rev_mp) 

605 
apply (erule_tac i=K in trans_induct) 

606 
apply (rule impI) 

607 
apply (rule le_anti_sym) 

608 
apply (erule_tac [2] InfCard_is_Card [THEN cmult_square_le]) 

609 
apply (rule ordertype_csquare_le [THEN [2] le_trans]) 

13221  610 
apply (simp add: cmult_def Ord_cardinal_le 
611 
well_ord_csquare [THEN Ord_ordertype] 

612 
well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll, 

613 
THEN cardinal_cong], assumption+) 

13216  614 
done 
615 

616 
(*Corollary for arbitrary wellordered sets (all sets, assuming AC)*) 

617 
lemma well_ord_InfCard_square_eq: 

618 
"[ well_ord(A,r); InfCard(A) ] ==> A*A \<approx> A" 

619 
apply (rule prod_eqpoll_cong [THEN eqpoll_trans]) 

620 
apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+ 

621 
apply (rule well_ord_cardinal_eqE) 

13221  622 
apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel, assumption) 
623 
apply (simp add: cmult_def [symmetric] InfCard_csquare_eq) 

13216  624 
done 
625 

13356  626 
lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K" 
627 
apply (rule well_ord_InfCard_square_eq) 

628 
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) 

629 
apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) 

630 
done 

631 

632 
lemma Inf_Card_is_InfCard: "[ ~Finite(i); Card(i) ] ==> InfCard(i)" 

633 
by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord]) 

634 

13216  635 
(** Toward's Kunen's Corollary 10.13 (1) **) 
636 

637 
lemma InfCard_le_cmult_eq: "[ InfCard(K); L le K; 0<L ] ==> K * L = K" 

638 
apply (rule le_anti_sym) 

639 
prefer 2 

640 
apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card) 

641 
apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl]) 

642 
apply (rule cmult_le_mono [THEN le_trans], assumption+) 

643 
apply (simp add: InfCard_csquare_eq) 

644 
done 

645 

646 
(*Corollary 10.13 (1), for cardinal multiplication*) 

647 
lemma InfCard_cmult_eq: "[ InfCard(K); InfCard(L) ] ==> K * L = K Un L" 

648 
apply (rule_tac i = "K" and j = "L" in Ord_linear_le) 

649 
apply (typecheck add: InfCard_is_Card Card_is_Ord) 

650 
apply (rule cmult_commute [THEN ssubst]) 

651 
apply (rule Un_commute [THEN ssubst]) 

13221  652 
apply (simp_all add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq 
653 
subset_Un_iff2 [THEN iffD1] le_imp_subset) 

13216  654 
done 
655 

656 
lemma InfCard_cdouble_eq: "InfCard(K) ==> K + K = K" 

13221  657 
apply (simp add: cmult_2 [symmetric] InfCard_is_Card cmult_commute) 
658 
apply (simp add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ) 

13216  659 
done 
660 

661 
(*Corollary 10.13 (1), for cardinal addition*) 

662 
lemma InfCard_le_cadd_eq: "[ InfCard(K); L le K ] ==> K + L = K" 

663 
apply (rule le_anti_sym) 

664 
prefer 2 

665 
apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card) 

666 
apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl]) 

667 
apply (rule cadd_le_mono [THEN le_trans], assumption+) 

668 
apply (simp add: InfCard_cdouble_eq) 

669 
done 

670 

671 
lemma InfCard_cadd_eq: "[ InfCard(K); InfCard(L) ] ==> K + L = K Un L" 

672 
apply (rule_tac i = "K" and j = "L" in Ord_linear_le) 

673 
apply (typecheck add: InfCard_is_Card Card_is_Ord) 

674 
apply (rule cadd_commute [THEN ssubst]) 

675 
apply (rule Un_commute [THEN ssubst]) 

13221  676 
apply (simp_all add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) 
13216  677 
done 
678 

679 
(*The other part, Corollary 10.13 (2), refers to the cardinality of the set 

680 
of all ntuples of elements of K. A better version for the Isabelle theory 

681 
might be InfCard(K) ==> list(K) = K. 

682 
*) 

683 

13356  684 
subsection{*For Every Cardinal Number There Exists A Greater One} 
685 

686 
text{*This result is Kunen's Theorem 10.16, which would be trivial using AC*} 

13216  687 

688 
lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))" 

689 
apply (unfold jump_cardinal_def) 

690 
apply (rule Ord_is_Transset [THEN [2] OrdI]) 

691 
prefer 2 apply (blast intro!: Ord_ordertype) 

692 
apply (unfold Transset_def) 

693 
apply (safe del: subsetI) 

13221  694 
apply (simp add: ordertype_pred_unfold, safe) 
13216  695 
apply (rule UN_I) 
696 
apply (rule_tac [2] ReplaceI) 

697 
prefer 4 apply (blast intro: well_ord_subset elim!: predE)+ 

698 
done 

699 

700 
(*Allows selective unfolding. Less work than deriving intro/elim rules*) 

701 
lemma jump_cardinal_iff: 

702 
"i : jump_cardinal(K) <> 

703 
(EX r X. r <= K*K & X <= K & well_ord(X,r) & i = ordertype(X,r))" 

704 
apply (unfold jump_cardinal_def) 

705 
apply (blast del: subsetI) 

706 
done 

707 

708 
(*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*) 

709 
lemma K_lt_jump_cardinal: "Ord(K) ==> K < jump_cardinal(K)" 

710 
apply (rule Ord_jump_cardinal [THEN [2] ltI]) 

711 
apply (rule jump_cardinal_iff [THEN iffD2]) 

712 
apply (rule_tac x="Memrel(K)" in exI) 

713 
apply (rule_tac x=K in exI) 

714 
apply (simp add: ordertype_Memrel well_ord_Memrel) 

715 
apply (simp add: Memrel_def subset_iff) 

716 
done 

717 

718 
(*The proof by contradiction: the bijection f yields a wellordering of X 

719 
whose ordertype is jump_cardinal(K). *) 

720 
lemma Card_jump_cardinal_lemma: 

721 
"[ well_ord(X,r); r <= K * K; X <= K; 

722 
f : bij(ordertype(X,r), jump_cardinal(K)) ] 

723 
==> jump_cardinal(K) : jump_cardinal(K)" 

724 
apply (subgoal_tac "f O ordermap (X,r) : bij (X, jump_cardinal (K))") 

725 
prefer 2 apply (blast intro: comp_bij ordermap_bij) 

726 
apply (rule jump_cardinal_iff [THEN iffD2]) 

727 
apply (intro exI conjI) 

13221  728 
apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+) 
13216  729 
apply (erule bij_is_inj [THEN well_ord_rvimage]) 
730 
apply (rule Ord_jump_cardinal [THEN well_ord_Memrel]) 

731 
apply (simp add: well_ord_Memrel [THEN [2] bij_ordertype_vimage] 

732 
ordertype_Memrel Ord_jump_cardinal) 

733 
done 

734 

735 
(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*) 

736 
lemma Card_jump_cardinal: "Card(jump_cardinal(K))" 

737 
apply (rule Ord_jump_cardinal [THEN CardI]) 

738 
apply (unfold eqpoll_def) 

739 
apply (safe dest!: ltD jump_cardinal_iff [THEN iffD1]) 

740 
apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl]) 

741 
done 

742 

13356  743 
subsection{*Basic Properties of Successor Cardinals*} 
13216  744 

745 
lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)" 

746 
apply (unfold csucc_def) 

747 
apply (rule LeastI) 

748 
apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ 

749 
done 

750 

751 
lemmas Card_csucc = csucc_basic [THEN conjunct1, standard] 

752 

753 
lemmas lt_csucc = csucc_basic [THEN conjunct2, standard] 

754 

755 
lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)" 

13221  756 
by (blast intro: Ord_0_le lt_csucc lt_trans1) 
13216  757 

758 
lemma csucc_le: "[ Card(L); K<L ] ==> csucc(K) le L" 

759 
apply (unfold csucc_def) 

760 
apply (rule Least_le) 

761 
apply (blast intro: Card_is_Ord)+ 

762 
done 

763 

764 
lemma lt_csucc_iff: "[ Ord(i); Card(K) ] ==> i < csucc(K) <> i le K" 

765 
apply (rule iffI) 

766 
apply (rule_tac [2] Card_lt_imp_lt) 

767 
apply (erule_tac [2] lt_trans1) 

768 
apply (simp_all add: lt_csucc Card_csucc Card_is_Ord) 

769 
apply (rule notI [THEN not_lt_imp_le]) 

13221  770 
apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl], assumption) 
13216  771 
apply (rule Ord_cardinal_le [THEN lt_trans1]) 
772 
apply (simp_all add: Ord_cardinal Card_is_Ord) 

773 
done 

774 

775 
lemma Card_lt_csucc_iff: 

776 
"[ Card(K'); Card(K) ] ==> K' < csucc(K) <> K' le K" 

13221  777 
by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord) 
13216  778 

779 
lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))" 

780 
by (simp add: InfCard_def Card_csucc Card_is_Ord 

781 
lt_csucc [THEN leI, THEN [2] le_trans]) 

782 

783 

784 
(** Removing elements from a finite set decreases its cardinality **) 

785 

786 
lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x~:A > ~ cons(x,A) \<lesssim> A" 

787 
apply (erule Fin_induct) 

13221  788 
apply (simp add: lepoll_0_iff) 
13216  789 
apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))") 
13221  790 
apply simp 
791 
apply (blast dest!: cons_lepoll_consD, blast) 

13216  792 
done 
793 

13221  794 
lemma Finite_imp_cardinal_cons: 
795 
"[ Finite(A); a~:A ] ==> cons(a,A) = succ(A)" 

13216  796 
apply (unfold cardinal_def) 
797 
apply (rule Least_equality) 

798 
apply (fold cardinal_def) 

13221  799 
apply (simp add: succ_def) 
13216  800 
apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll 
801 
elim!: mem_irrefl dest!: Finite_imp_well_ord) 

802 
apply (blast intro: Card_cardinal Card_is_Ord) 

803 
apply (rule notI) 

13221  804 
apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE], 
805 
assumption, assumption) 

13216  806 
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) 
807 
apply (erule le_imp_lepoll [THEN lepoll_trans]) 

808 
apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll] 

809 
dest!: Finite_imp_well_ord) 

810 
done 

811 

812 

13221  813 
lemma Finite_imp_succ_cardinal_Diff: 
814 
"[ Finite(A); a:A ] ==> succ(A{a}) = A" 

815 
apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption) 

816 
apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite]) 

817 
apply (simp add: cons_Diff) 

13216  818 
done 
819 

820 
lemma Finite_imp_cardinal_Diff: "[ Finite(A); a:A ] ==> A{a} < A" 

821 
apply (rule succ_leE) 

13221  822 
apply (simp add: Finite_imp_succ_cardinal_Diff) 
13216  823 
done 
824 

825 

826 
(** Theorems by Krzysztof Grabczewski, proofs by lcp **) 

827 

828 
lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard] 

829 

830 
lemma nat_sum_eqpoll_sum: "[ m:nat; n:nat ] ==> m + n \<approx> m #+ n" 

831 
apply (rule eqpoll_trans) 

832 
apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym]) 

833 
apply (erule nat_implies_well_ord)+ 

13221  834 
apply (simp add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl) 
13216  835 
done 
836 

13221  837 
lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i <= nat > i : nat  i=nat" 
838 
apply (erule trans_induct3, auto) 

13216  839 
apply (blast dest!: nat_le_Limit [THEN le_imp_subset]) 
840 
done 

841 

842 
lemma Ord_nat_subset_into_Card: "[ Ord(i); i <= nat ] ==> Card(i)" 

13221  843 
by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) 
13216  844 

845 
lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> A : nat" 

846 
apply (erule Finite_induct) 

847 
apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons) 

848 
done 

849 

850 
lemma Finite_Diff_sing_eq_diff_1: "[ Finite(A); x:A ] ==> A{x} = A # 1" 

851 
apply (rule succ_inject) 

852 
apply (rule_tac b = "A" in trans) 

13221  853 
apply (simp add: Finite_imp_succ_cardinal_Diff) 
13216  854 
apply (subgoal_tac "1 \<lesssim> A") 
13221  855 
prefer 2 apply (blast intro: not_0_is_lepoll_1) 
856 
apply (frule Finite_imp_well_ord, clarify) 

13216  857 
apply (rotate_tac 1) 
858 
apply (drule well_ord_lepoll_imp_Card_le) 

859 
apply (auto simp add: cardinal_1) 

860 
apply (rule trans) 

861 
apply (rule_tac [2] diff_succ) 

862 
apply (auto simp add: Finite_cardinal_in_nat) 

863 
done 

864 

13221  865 
lemma cardinal_lt_imp_Diff_not_0 [rule_format]: 
866 
"Finite(B) ==> ALL A. B<A > A  B ~= 0" 

867 
apply (erule Finite_induct, auto) 

13216  868 
apply (simp_all add: Finite_imp_cardinal_cons) 
13221  869 
apply (case_tac "Finite (A)") 
870 
apply (subgoal_tac [2] "Finite (cons (x, B))") 

871 
apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite) 

872 
apply (auto simp add: Finite_0 Finite_cons) 

13216  873 
apply (subgoal_tac "B<A") 
13221  874 
prefer 2 apply (blast intro: lt_trans Ord_cardinal) 
13216  875 
apply (case_tac "x:A") 
13221  876 
apply (subgoal_tac [2] "A  cons (x, B) = A  B") 
877 
apply auto 

13216  878 
apply (subgoal_tac "A le cons (x, B) ") 
13221  879 
prefer 2 
13216  880 
apply (blast dest: Finite_cons [THEN Finite_imp_well_ord] 
881 
intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll) 

882 
apply (auto simp add: Finite_imp_cardinal_cons) 

883 
apply (auto dest!: Finite_cardinal_in_nat simp add: le_iff) 

884 
apply (blast intro: lt_trans) 

885 
done 

886 

887 

888 
ML{* 

889 
val InfCard_def = thm "InfCard_def" 

890 
val cmult_def = thm "cmult_def" 

891 
val cadd_def = thm "cadd_def" 

892 
val jump_cardinal_def = thm "jump_cardinal_def" 

893 
val csucc_def = thm "csucc_def" 

894 

895 
val sum_commute_eqpoll = thm "sum_commute_eqpoll"; 

896 
val cadd_commute = thm "cadd_commute"; 

897 
val sum_assoc_eqpoll = thm "sum_assoc_eqpoll"; 

898 
val well_ord_cadd_assoc = thm "well_ord_cadd_assoc"; 

899 
val sum_0_eqpoll = thm "sum_0_eqpoll"; 

900 
val cadd_0 = thm "cadd_0"; 

901 
val sum_lepoll_self = thm "sum_lepoll_self"; 

902 
val cadd_le_self = thm "cadd_le_self"; 

903 
val sum_lepoll_mono = thm "sum_lepoll_mono"; 

904 
val cadd_le_mono = thm "cadd_le_mono"; 

905 
val eq_imp_not_mem = thm "eq_imp_not_mem"; 

906 
val sum_succ_eqpoll = thm "sum_succ_eqpoll"; 

907 
val nat_cadd_eq_add = thm "nat_cadd_eq_add"; 

908 
val prod_commute_eqpoll = thm "prod_commute_eqpoll"; 

909 
val cmult_commute = thm "cmult_commute"; 

910 
val prod_assoc_eqpoll = thm "prod_assoc_eqpoll"; 

911 
val well_ord_cmult_assoc = thm "well_ord_cmult_assoc"; 

912 
val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll"; 

913 
val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib"; 

914 
val prod_0_eqpoll = thm "prod_0_eqpoll"; 

915 
val cmult_0 = thm "cmult_0"; 

916 
val prod_singleton_eqpoll = thm "prod_singleton_eqpoll"; 

917 
val cmult_1 = thm "cmult_1"; 

918 
val prod_lepoll_self = thm "prod_lepoll_self"; 

919 
val cmult_le_self = thm "cmult_le_self"; 

920 
val prod_lepoll_mono = thm "prod_lepoll_mono"; 

921 
val cmult_le_mono = thm "cmult_le_mono"; 

922 
val prod_succ_eqpoll = thm "prod_succ_eqpoll"; 

923 
val nat_cmult_eq_mult = thm "nat_cmult_eq_mult"; 

924 
val cmult_2 = thm "cmult_2"; 

925 
val sum_lepoll_prod = thm "sum_lepoll_prod"; 

926 
val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod"; 

927 
val nat_cons_lepoll = thm "nat_cons_lepoll"; 

928 
val nat_cons_eqpoll = thm "nat_cons_eqpoll"; 

929 
val nat_succ_eqpoll = thm "nat_succ_eqpoll"; 

930 
val InfCard_nat = thm "InfCard_nat"; 

931 
val InfCard_is_Card = thm "InfCard_is_Card"; 

932 
val InfCard_Un = thm "InfCard_Un"; 

933 
val InfCard_is_Limit = thm "InfCard_is_Limit"; 

934 
val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred"; 

935 
val ordermap_z_lt = thm "ordermap_z_lt"; 

936 
val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq"; 

937 
val InfCard_cmult_eq = thm "InfCard_cmult_eq"; 

938 
val InfCard_cdouble_eq = thm "InfCard_cdouble_eq"; 

939 
val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq"; 

940 
val InfCard_cadd_eq = thm "InfCard_cadd_eq"; 

941 
val Ord_jump_cardinal = thm "Ord_jump_cardinal"; 

942 
val jump_cardinal_iff = thm "jump_cardinal_iff"; 

943 
val K_lt_jump_cardinal = thm "K_lt_jump_cardinal"; 

944 
val Card_jump_cardinal = thm "Card_jump_cardinal"; 

945 
val csucc_basic = thm "csucc_basic"; 

946 
val Card_csucc = thm "Card_csucc"; 

947 
val lt_csucc = thm "lt_csucc"; 

948 
val Ord_0_lt_csucc = thm "Ord_0_lt_csucc"; 

949 
val csucc_le = thm "csucc_le"; 

950 
val lt_csucc_iff = thm "lt_csucc_iff"; 

951 
val Card_lt_csucc_iff = thm "Card_lt_csucc_iff"; 

952 
val InfCard_csucc = thm "InfCard_csucc"; 

953 
val Finite_into_Fin = thm "Finite_into_Fin"; 

954 
val Fin_into_Finite = thm "Fin_into_Finite"; 

955 
val Finite_Fin_iff = thm "Finite_Fin_iff"; 

956 
val Finite_Un = thm "Finite_Un"; 

957 
val Finite_Union = thm "Finite_Union"; 

958 
val Finite_induct = thm "Finite_induct"; 

959 
val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll"; 

960 
val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons"; 

961 
val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff"; 

962 
val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff"; 

963 
val nat_implies_well_ord = thm "nat_implies_well_ord"; 

964 
val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum"; 

965 
val Diff_sing_Finite = thm "Diff_sing_Finite"; 

966 
val Diff_Finite = thm "Diff_Finite"; 

967 
val Ord_subset_natD = thm "Ord_subset_natD"; 

968 
val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card"; 

969 
val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat"; 

970 
val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1"; 

971 
val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0"; 

972 
*} 

973 

437  974 
end 