author  paulson 
Sun, 16 Jun 2002 11:58:54 +0200  
changeset 13216  6104bd4088a2 
parent 13161  a40db0418145 
child 13221  e29378f347e4 
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 

13216  6 
Cardinal arithmetic  WITHOUT the Axiom of Choice 
7 

8 
Note: Could omit proving the algebraic laws for cardinal addition and 

9 
multiplication. On finite cardinals these operations coincide with 

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

11 
coincide with union (maximum). Either way we get most laws for free. 

437  12 
*) 
13 

12667  14 
theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite: 
467  15 

12667  16 
constdefs 
437  17 

12667  18 
InfCard :: "i=>o" 
19 
"InfCard(i) == Card(i) & nat le i" 

437  20 

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

23 

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

25 
"i + j == i+j" 

437  26 

12667  27 
csquare_rel :: "i=>i" 
28 
"csquare_rel(K) == 

29 
rvimage(K*K, 

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

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

437  32 

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

12667  35 
jump_cardinal :: "i=>i" 
36 
"jump_cardinal(K) == 

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

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

484  42 

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

43 
syntax (xsymbols) 
12667  44 
"op +" :: "[i,i] => i" (infixl "\<oplus>" 65) 
45 
"op *" :: "[i,i] => i" (infixl "\<otimes>" 70) 

46 

47 

13118  48 
(*** The following really belong early in the development ***) 
49 

50 
lemma relation_converse_converse [simp]: 

51 
"relation(r) ==> converse(converse(r)) = r" 

52 
by (simp add: relation_def, blast) 

53 

54 
lemma relation_restrict [simp]: "relation(restrict(r,A))" 

55 
by (simp add: restrict_def relation_def, blast) 

56 

57 
(*** The following really belong in Order ***) 

58 

59 
lemma subset_ord_iso_Memrel: 

13161  60 
"[ f: ord_iso(A,Memrel(B),C,r); A<=B ] ==> f: ord_iso(A,Memrel(A),C,r)" 
13118  61 
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel]) 
62 
apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption) 

63 
apply (simp add: right_comp_id) 

64 
done 

65 

66 
lemma restrict_ord_iso: 

13161  67 
"[ f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \<in> A; j < i; 
68 
trans[A](r) ] 

69 
==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)" 

13118  70 
apply (frule ltD) 
71 
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 

72 
apply (frule ord_iso_restrict_pred, assumption) 

73 
apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel) 

74 
apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI]) 

75 
done 

76 

77 
lemma restrict_ord_iso2: 

13161  78 
"[ f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A; 
79 
j < i; trans[A](r) ] 

80 
==> converse(restrict(converse(f), j)) 

13118  81 
\<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))" 
82 
by (blast intro: restrict_ord_iso ord_iso_sym ltI) 

83 

12667  84 
(*** The following really belong in OrderType ***) 
85 

13161  86 
lemma oadd_eq_0_iff: "[ Ord(i); Ord(j) ] ==> (i ++ j) = 0 <> i=0 & j=0" 
12667  87 
apply (erule trans_induct3 [of j]) 
88 
apply (simp_all add: oadd_Limit) 

12820  89 
apply (simp add: Union_empty_iff Limit_def lt_def, blast) 
12667  90 
done 
91 

13161  92 
lemma oadd_eq_lt_iff: "[ Ord(i); Ord(j) ] ==> 0 < (i ++ j) <> 0<i  0<j" 
12667  93 
by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff) 
94 

95 
lemma oadd_lt_self: "[ Ord(i); 0<j ] ==> i < i++j" 

96 
apply (rule lt_trans2) 

97 
apply (erule le_refl) 

98 
apply (simp only: lt_Ord2 oadd_1 [of i, symmetric]) 

99 
apply (blast intro: succ_leI oadd_le_mono) 

100 
done 

101 

13161  102 
lemma oadd_LimitI: "[ Ord(i); Limit(j) ] ==> Limit(i ++ j)" 
12667  103 
apply (simp add: oadd_Limit) 
104 
apply (frule Limit_has_1 [THEN ltD]) 

105 
apply (rule increasing_LimitI) 

106 
apply (rule Ord_0_lt) 

107 
apply (blast intro: Ord_in_Ord [OF Limit_is_Ord]) 

108 
apply (force simp add: Union_empty_iff oadd_eq_0_iff 

12820  109 
Limit_is_Ord [of j, THEN Ord_in_Ord], auto) 
12667  110 
apply (rule_tac x="succ(x)" in bexI) 
111 
apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord]) 

112 
apply (simp add: Limit_def lt_def) 

113 
done 

114 

115 
(*** The following really belong in Cardinal ***) 

116 

117 
lemma lesspoll_not_refl: "~ (i lesspoll i)" 

118 
by (simp add: lesspoll_def) 

119 

120 
lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P" 

121 
by (simp add: lesspoll_def) 

122 

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

124 
apply (rule CardI) 

125 
apply (simp add: Card_is_Ord) 

126 
apply (clarify dest!: ltD) 

127 
apply (drule bspec, assumption) 

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

129 
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) 

130 
apply (drule lesspoll_trans1, assumption) 

13216  131 
apply (subgoal_tac "B \<lesssim> \<Union>A") 
12667  132 
apply (drule lesspoll_trans1, assumption, blast) 
133 
apply (blast intro: subset_imp_lepoll) 

134 
done 

135 

136 
lemma Card_UN: 

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

138 
by (blast intro: Card_Union) 

139 

140 
lemma Card_OUN [simp,intro,TC]: 

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

142 
by (simp add: OUnion_def Card_0) 

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

143 

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

146 
apply (rule conjI) 

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

148 
apply (rule notI) 

149 
apply (erule eqpollE) 

150 
apply (rule succ_lepoll_natE) 

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

12820  152 
lepoll_trans, assumption) 
12776  153 
done 
154 

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

156 
apply (unfold lesspoll_def) 

157 
apply (simp add: Card_iff_initial) 

158 
apply (fast intro!: le_imp_lepoll ltI leI) 

159 
done 

160 

161 
lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0" 

162 
by (fast dest!: lepoll_0_is_0) 

163 

164 
lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0" 

165 
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0]) 

166 

167 
lemma Finite_Fin_lemma [rule_format]: 

168 
"n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) > A \<in> Fin(X)" 

169 
apply (induct_tac "n") 

170 
apply (rule allI) 

171 
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0]) 

172 
apply (rule allI) 

173 
apply (rule impI) 

174 
apply (erule conjE) 

12820  175 
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption) 
176 
apply (frule Diff_sing_eqpoll, assumption) 

12776  177 
apply (erule allE) 
178 
apply (erule impE, fast) 

12820  179 
apply (drule subsetD, assumption) 
180 
apply (drule Fin.consI, assumption) 

12776  181 
apply (simp add: cons_Diff) 
182 
done 

183 

184 
lemma Finite_Fin: "[ Finite(A); A \<subseteq> X ] ==> A \<in> Fin(X)" 

185 
by (unfold Finite_def, blast intro: Finite_Fin_lemma) 

186 

187 
lemma lesspoll_lemma: 

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

189 
apply (unfold lesspoll_def) 

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

191 
intro!: eqpollI elim: notE 

192 
elim!: eqpollE lepoll_trans) 

193 
done 

194 

195 
lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <> Finite(B)" 

196 
apply (unfold Finite_def) 

197 
apply (blast intro: eqpoll_trans eqpoll_sym) 

198 
done 

199 

13216  200 

201 
(*** Cardinal addition ***) 

202 

203 
(** Cardinal addition is commutative **) 

204 

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

206 
apply (unfold eqpoll_def) 

207 
apply (rule exI) 

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

209 
apply auto 

210 
done 

211 

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

213 
apply (unfold cadd_def) 

214 
apply (rule sum_commute_eqpoll [THEN cardinal_cong]) 

215 
done 

216 

217 
(** Cardinal addition is associative **) 

218 

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

220 
apply (unfold eqpoll_def) 

221 
apply (rule exI) 

222 
apply (rule sum_assoc_bij) 

223 
done 

224 

225 
(*Unconditional version requires AC*) 

226 
lemma well_ord_cadd_assoc: 

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

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

229 
apply (unfold cadd_def) 

230 
apply (rule cardinal_cong) 

231 
apply (rule eqpoll_trans) 

232 
apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 

233 
apply (blast intro: well_ord_radd elim:) 

234 
apply (rule sum_assoc_eqpoll [THEN eqpoll_trans]) 

235 
apply (rule eqpoll_sym) 

236 
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

237 
apply (blast intro: well_ord_radd elim:) 

238 
done 

239 

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

241 

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

243 
apply (unfold eqpoll_def) 

244 
apply (rule exI) 

245 
apply (rule bij_0_sum) 

246 
done 

247 

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

249 
apply (unfold cadd_def) 

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

251 
done 

252 

253 
(** Addition by another cardinal **) 

254 

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

256 
apply (unfold lepoll_def inj_def) 

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

258 
apply (simp (no_asm_simp)) 

259 
done 

260 

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

262 

263 
lemma cadd_le_self: 

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

265 
apply (unfold cadd_def) 

266 
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le]) 

267 
apply assumption; 

268 
apply (rule_tac [2] sum_lepoll_self) 

269 
apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord) 

270 
done 

271 

272 
(** Monotonicity of addition **) 

273 

274 
lemma sum_lepoll_mono: 

275 
"[ A \<lesssim> C; B \<lesssim> D ] ==> A + B \<lesssim> C + D" 

276 
apply (unfold lepoll_def) 

277 
apply (elim exE); 

278 
apply (rule_tac x = "lam z:A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI) 

279 
apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) `y))" 

280 
in lam_injective) 

281 
apply (typecheck add: inj_is_fun) 

282 
apply auto 

283 
done 

284 

285 
lemma cadd_le_mono: 

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

287 
apply (unfold cadd_def) 

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

289 
apply (rule well_ord_lepoll_imp_Card_le) 

290 
apply (blast intro: well_ord_radd well_ord_Memrel) 

291 
apply (blast intro: sum_lepoll_mono subset_imp_lepoll) 

292 
done 

293 

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

295 

296 
(*????????????????upair.ML*) 

297 
lemma eq_imp_not_mem: "a=A ==> a ~: A" 

298 
apply (blast intro: elim: mem_irrefl); 

299 
done 

300 

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

302 
apply (unfold eqpoll_def) 

303 
apply (rule exI) 

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

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

306 
apply (simp_all) 

307 
apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+ 

308 
done 

309 

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

311 
(*Unconditional version requires AC*) 

312 
lemma cadd_succ_lemma: 

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

314 
apply (unfold cadd_def) 

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

316 
apply (rule succ_eqpoll_cong [THEN cardinal_cong]) 

317 
apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym]) 

318 
apply (blast intro: well_ord_radd well_ord_Memrel) 

319 
done 

320 

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

322 
apply (induct_tac "m") 

323 
apply (simp add: nat_into_Card [THEN cadd_0]) 

324 
apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq]) 

325 
done 

326 

327 

328 
(*** Cardinal multiplication ***) 

329 

330 
(** Cardinal multiplication is commutative **) 

331 

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

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

334 
apply (unfold eqpoll_def) 

335 
apply (rule exI) 

336 
apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective) 

337 
apply (auto ); 

338 
done 

339 

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

341 
apply (unfold cmult_def) 

342 
apply (rule prod_commute_eqpoll [THEN cardinal_cong]) 

343 
done 

344 

345 
(** Cardinal multiplication is associative **) 

346 

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

348 
apply (unfold eqpoll_def) 

349 
apply (rule exI) 

350 
apply (rule prod_assoc_bij) 

351 
done 

352 

353 
(*Unconditional version requires AC*) 

354 
lemma well_ord_cmult_assoc: 

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

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

357 
apply (unfold cmult_def) 

358 
apply (rule cardinal_cong) 

359 
apply (rule eqpoll_trans); 

360 
apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 

361 
apply (blast intro: well_ord_rmult) 

362 
apply (rule prod_assoc_eqpoll [THEN eqpoll_trans]) 

363 
apply (rule eqpoll_sym); 

364 
apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

365 
apply (blast intro: well_ord_rmult) 

366 
done 

367 

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

369 

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

371 
apply (unfold eqpoll_def) 

372 
apply (rule exI) 

373 
apply (rule sum_prod_distrib_bij) 

374 
done 

375 

376 
lemma well_ord_cadd_cmult_distrib: 

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

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

379 
apply (unfold cadd_def cmult_def) 

380 
apply (rule cardinal_cong) 

381 
apply (rule eqpoll_trans); 

382 
apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 

383 
apply (blast intro: well_ord_radd) 

384 
apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans]) 

385 
apply (rule eqpoll_sym); 

386 
apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll 

387 
well_ord_cardinal_eqpoll]) 

388 
apply (blast intro: well_ord_rmult)+ 

389 
done 

390 

391 
(** Multiplication by 0 yields 0 **) 

392 

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

394 
apply (unfold eqpoll_def) 

395 
apply (rule exI) 

396 
apply (rule lam_bijective) 

397 
apply safe 

398 
done 

399 

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

401 
apply (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong]) 

402 
done 

403 

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

405 

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

407 
apply (unfold eqpoll_def) 

408 
apply (rule exI) 

409 
apply (rule singleton_prod_bij [THEN bij_converse_bij]) 

410 
done 

411 

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

413 
apply (unfold cmult_def succ_def) 

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

415 
done 

416 

417 
(*** Some inequalities for multiplication ***) 

418 

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

420 
apply (unfold lepoll_def inj_def) 

421 
apply (rule_tac x = "lam x:A. <x,x>" in exI) 

422 
apply (simp (no_asm)) 

423 
done 

424 

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

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

427 
apply (unfold cmult_def) 

428 
apply (rule le_trans) 

429 
apply (rule_tac [2] well_ord_lepoll_imp_Card_le) 

430 
apply (rule_tac [3] prod_square_lepoll) 

431 
apply (simp (no_asm_simp) add: le_refl Card_is_Ord Card_cardinal_eq) 

432 
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord); 

433 
done 

434 

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

436 

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

438 
apply (unfold lepoll_def inj_def) 

439 
apply (rule_tac x = "lam x:A. <x,b>" in exI) 

440 
apply (simp (no_asm_simp)) 

441 
done 

442 

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

444 
lemma cmult_le_self: 

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

446 
apply (unfold cmult_def) 

447 
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le]) 

448 
apply assumption; 

449 
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) 

450 
apply (blast intro: prod_lepoll_self ltD) 

451 
done 

452 

453 
(** Monotonicity of multiplication **) 

454 

455 
lemma prod_lepoll_mono: 

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

457 
apply (unfold lepoll_def) 

458 
apply (elim exE); 

459 
apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in exI) 

460 
apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>" 

461 
in lam_injective) 

462 
apply (typecheck add: inj_is_fun) 

463 
apply auto 

464 
done 

465 

466 
lemma cmult_le_mono: 

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

468 
apply (unfold cmult_def) 

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

470 
apply (rule well_ord_lepoll_imp_Card_le) 

471 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

472 
apply (blast intro: prod_lepoll_mono subset_imp_lepoll) 

473 
done 

474 

475 
(*** Multiplication of finite cardinals is "ordinary" multiplication ***) 

476 

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

478 
apply (unfold eqpoll_def) 

479 
apply (rule exI); 

480 
apply (rule_tac c = "%<x,y>. if x=A then Inl (y) else Inr (<x,y>)" 

481 
and d = "case (%y. <A,y>, %z. z)" in lam_bijective) 

482 
apply safe 

483 
apply (simp_all add: succI2 if_type mem_imp_not_eq) 

484 
done 

485 

486 
(*Unconditional version requires AC*) 

487 
lemma cmult_succ_lemma: 

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

489 
apply (unfold cmult_def cadd_def) 

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

491 
apply (rule cardinal_cong [symmetric]) 

492 
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

493 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

494 
done 

495 

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

497 
apply (induct_tac "m") 

498 
apply (simp (no_asm_simp)) 

499 
apply (simp (no_asm_simp) add: cmult_succ_lemma nat_cadd_eq_add) 

500 
done 

501 

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

503 
apply (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0]) 

504 
done 

505 

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

507 
apply (rule lepoll_trans); 

508 
apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll]) 

509 
apply (erule prod_lepoll_mono) 

510 
apply (rule lepoll_refl); 

511 
done 

512 

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

514 
apply (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl) 

515 
done 

516 

517 

518 
(*** Infinite Cardinals are Limit Ordinals ***) 

519 

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

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

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

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

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

525 
apply (unfold lepoll_def) 

526 
apply (erule exE) 

527 
apply (rule_tac x = 

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

529 
if z=u then f`0 

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

531 
in exI) 

532 
apply (rule_tac d = 

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

534 
else y" 

535 
in lam_injective) 

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

537 
apply (simp add: inj_is_fun [THEN apply_rangeI] 

538 
inj_converse_fun [THEN apply_rangeI] 

539 
inj_converse_fun [THEN apply_funtype]) 

540 
done 

541 

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

543 
apply (erule nat_cons_lepoll [THEN eqpollI]) 

544 
apply (rule subset_consI [THEN subset_imp_lepoll]) 

545 
done 

546 

547 
(*Specialized version required below*) 

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

549 
apply (unfold succ_def) 

550 
apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll]) 

551 
done 

552 

553 
lemma InfCard_nat: "InfCard(nat)" 

554 
apply (unfold InfCard_def) 

555 
apply (blast intro: Card_nat le_refl Card_is_Ord) 

556 
done 

557 

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

559 
apply (unfold InfCard_def) 

560 
apply (erule conjunct1) 

561 
done 

562 

563 
lemma InfCard_Un: 

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

565 
apply (unfold InfCard_def) 

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

567 
done 

568 

569 
(*Kunen's Lemma 10.11*) 

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

571 
apply (unfold InfCard_def) 

572 
apply (erule conjE) 

573 
apply (frule Card_is_Ord) 

574 
apply (rule ltI [THEN non_succ_LimitI]) 

575 
apply (erule le_imp_subset [THEN subsetD]) 

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

577 
apply (unfold Card_def) 

578 
apply (drule trans) 

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

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

581 
apply (rule le_eqI) 

582 
apply assumption; 

583 
apply (rule Ord_cardinal) 

584 
done 

585 

586 

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

588 

589 
(*A general fact about ordermap*) 

590 
lemma ordermap_eqpoll_pred: 

591 
"[ well_ord(A,r); x:A ] ==> ordermap(A,r)`x \<approx> pred(A,x,r)" 

592 
apply (unfold eqpoll_def) 

593 
apply (rule exI) 

594 
apply (simp (no_asm_simp) add: ordermap_eq_image well_ord_is_wf) 

595 
apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, THEN bij_converse_bij]) 

596 
apply (rule pred_subset) 

597 
done 

598 

599 
(** Establishing the wellordering **) 

600 

601 
lemma csquare_lam_inj: 

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

603 
apply (unfold inj_def) 

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

605 
done 

606 

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

608 
apply (unfold csquare_rel_def) 

609 
apply (rule csquare_lam_inj [THEN well_ord_rvimage]) 

610 
apply assumption; 

611 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

612 
done 

613 

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

615 

616 
lemma csquareD: 

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

618 
apply (unfold csquare_rel_def) 

619 
apply (erule rev_mp) 

620 
apply (elim ltE) 

621 
apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 

622 
apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le) 

623 
apply (simp_all (no_asm_simp) add: lt_def succI2) 

624 
done 

625 

626 
lemma pred_csquare_subset: 

627 
"z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)" 

628 
apply (unfold Order.pred_def) 

629 
apply (safe del: SigmaI succCI) 

630 
apply (erule csquareD [THEN conjE]) 

631 
apply (unfold lt_def) 

632 
apply (auto ); 

633 
done 

634 

635 
lemma csquare_ltI: 

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

637 
apply (unfold csquare_rel_def) 

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

639 
prefer 2 apply (blast intro: lt_trans) 

640 
apply (elim ltE) 

641 
apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 

642 
done 

643 

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

645 
lemma csquare_or_eqI: 

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

647 
apply (unfold csquare_rel_def) 

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

649 
prefer 2 apply (blast intro: lt_trans1) 

650 
apply (elim ltE) 

651 
apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 

652 
apply (elim succE) 

653 
apply (simp_all (no_asm_simp) add: subset_Un_iff [THEN iff_sym] subset_Un_iff2 [THEN iff_sym] OrdmemD) 

654 
done 

655 

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

657 

658 
lemma ordermap_z_lt: 

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

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

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

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

663 
prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ 

664 
Limit_is_Ord [THEN well_ord_csquare]) 

665 
apply (clarify ); 

666 
apply (rule csquare_ltI [THEN ordermap_mono, THEN ltI]) 

667 
apply (erule_tac [4] well_ord_is_wf) 

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

669 
done 

670 

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

672 
lemma ordermap_csquare_le: 

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

674 
 ordermap(K*K, csquare_rel(K)) ` <x,y>  le succ(z) * succ(z)" 

675 
apply (unfold cmult_def) 

676 
apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le]) 

677 
apply (rule Ord_cardinal [THEN well_ord_Memrel])+ 

678 
apply (subgoal_tac "z<K") 

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

680 
apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans]) 

681 
apply assumption + 

682 
apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) 

683 
apply (erule Limit_is_Ord [THEN well_ord_csquare]) 

684 
apply (blast intro: ltD) 

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

686 
assumption) 

687 
apply (elim ltE) 

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

689 
apply (erule Ord_succ [THEN Ord_cardinal_eqpoll])+ 

690 
done 

691 

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

693 
lemma ordertype_csquare_le: 

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

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

696 
apply (frule InfCard_is_Card [THEN Card_is_Ord]) 

697 
apply (rule all_lt_imp_le) 

698 
apply assumption 

699 
apply (erule well_ord_csquare [THEN Ord_ordertype]) 

700 
apply (rule Card_lt_imp_lt) 

701 
apply (erule_tac [3] InfCard_is_Card) 

702 
apply (erule_tac [2] ltE) 

703 
apply (simp add: ordertype_unfold) 

704 
apply (safe elim!: ltE) 

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

706 
prefer 2 apply (blast intro: Ord_in_Ord) 

707 
apply (clarify ); 

708 
(*??WHAT A MESS!*) 

709 
apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1], 

710 
(assumption  rule refl  erule ltI)+) 

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

712 
simp_all add: Ord_Un Ord_nat) 

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

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

715 
le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un 

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

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

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

719 
apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type 

720 
nat_into_Card [THEN Card_cardinal_eq] Ord_nat) 

721 
apply (simp add: InfCard_def) 

722 
done 

723 

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

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

726 
apply (frule InfCard_is_Card [THEN Card_is_Ord]) 

727 
apply (erule rev_mp) 

728 
apply (erule_tac i=K in trans_induct) 

729 
apply (rule impI) 

730 
apply (rule le_anti_sym) 

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

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

733 
prefer 2 apply (assumption) 

734 
prefer 2 apply (assumption) 

735 
apply (simp (no_asm_simp) add: cmult_def Ord_cardinal_le well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll, THEN cardinal_cong] well_ord_csquare [THEN Ord_ordertype]) 

736 
done 

737 

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

739 
lemma well_ord_InfCard_square_eq: 

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

741 
apply (rule prod_eqpoll_cong [THEN eqpoll_trans]) 

742 
apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+ 

743 
apply (rule well_ord_cardinal_eqE) 

744 
apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel) 

745 
apply assumption; 

746 
apply (simp (no_asm_simp) add: cmult_def [symmetric] InfCard_csquare_eq) 

747 
done 

748 

749 
(** Toward's Kunen's Corollary 10.13 (1) **) 

750 

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

752 
apply (rule le_anti_sym) 

753 
prefer 2 

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

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

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

757 
apply (simp add: InfCard_csquare_eq) 

758 
done 

759 

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

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

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

763 
apply (typecheck add: InfCard_is_Card Card_is_Ord) 

764 
apply (rule cmult_commute [THEN ssubst]) 

765 
apply (rule Un_commute [THEN ssubst]) 

766 
apply (simp_all (no_asm_simp) add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) 

767 
done 

768 

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

770 
apply (simp (no_asm_simp) add: cmult_2 [symmetric] InfCard_is_Card cmult_commute) 

771 
apply (simp (no_asm_simp) add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ) 

772 
done 

773 

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

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

776 
apply (rule le_anti_sym) 

777 
prefer 2 

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

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

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

781 
apply (simp add: InfCard_cdouble_eq) 

782 
done 

783 

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

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

786 
apply (typecheck add: InfCard_is_Card Card_is_Ord) 

787 
apply (rule cadd_commute [THEN ssubst]) 

788 
apply (rule Un_commute [THEN ssubst]) 

789 
apply (simp_all (no_asm_simp) add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) 

790 
done 

791 

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

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

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

795 
*) 

796 

797 
(*** For every cardinal number there exists a greater one 

798 
[Kunen's Theorem 10.16, which would be trivial using AC] ***) 

799 

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

801 
apply (unfold jump_cardinal_def) 

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

803 
prefer 2 apply (blast intro!: Ord_ordertype) 

804 
apply (unfold Transset_def) 

805 
apply (safe del: subsetI) 

806 
apply (simp add: ordertype_pred_unfold) 

807 
apply safe 

808 
apply (rule UN_I) 

809 
apply (rule_tac [2] ReplaceI) 

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

811 
done 

812 

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

814 
lemma jump_cardinal_iff: 

815 
"i : jump_cardinal(K) <> 

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

817 
apply (unfold jump_cardinal_def) 

818 
apply (blast del: subsetI) 

819 
done 

820 

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

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

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

824 
apply (rule jump_cardinal_iff [THEN iffD2]) 

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

826 
apply (rule_tac x=K in exI) 

827 
apply (simp add: ordertype_Memrel well_ord_Memrel) 

828 
apply (simp add: Memrel_def subset_iff) 

829 
done 

830 

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

832 
whose ordertype is jump_cardinal(K). *) 

833 
lemma Card_jump_cardinal_lemma: 

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

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

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

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

838 
prefer 2 apply (blast intro: comp_bij ordermap_bij) 

839 
apply (rule jump_cardinal_iff [THEN iffD2]) 

840 
apply (intro exI conjI) 

841 
apply (rule subset_trans [OF rvimage_type Sigma_mono]) 

842 
apply assumption+ 

843 
apply (erule bij_is_inj [THEN well_ord_rvimage]) 

844 
apply (rule Ord_jump_cardinal [THEN well_ord_Memrel]) 

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

846 
ordertype_Memrel Ord_jump_cardinal) 

847 
done 

848 

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

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

851 
apply (rule Ord_jump_cardinal [THEN CardI]) 

852 
apply (unfold eqpoll_def) 

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

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

855 
done 

856 

857 
(*** Basic properties of successor cardinals ***) 

858 

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

860 
apply (unfold csucc_def) 

861 
apply (rule LeastI) 

862 
apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ 

863 
done 

864 

865 
lemmas Card_csucc = csucc_basic [THEN conjunct1, standard] 

866 

867 
lemmas lt_csucc = csucc_basic [THEN conjunct2, standard] 

868 

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

870 
apply (blast intro: Ord_0_le lt_csucc lt_trans1) 

871 
done 

872 

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

874 
apply (unfold csucc_def) 

875 
apply (rule Least_le) 

876 
apply (blast intro: Card_is_Ord)+ 

877 
done 

878 

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

880 
apply (rule iffI) 

881 
apply (rule_tac [2] Card_lt_imp_lt) 

882 
apply (erule_tac [2] lt_trans1) 

883 
apply (simp_all add: lt_csucc Card_csucc Card_is_Ord) 

884 
apply (rule notI [THEN not_lt_imp_le]) 

885 
apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl]) 

886 
apply assumption 

887 
apply (rule Ord_cardinal_le [THEN lt_trans1]) 

888 
apply (simp_all add: Ord_cardinal Card_is_Ord) 

889 
done 

890 

891 
lemma Card_lt_csucc_iff: 

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

893 
by (simp (no_asm_simp) add: lt_csucc_iff Card_cardinal_eq Card_is_Ord) 

894 

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

896 
by (simp add: InfCard_def Card_csucc Card_is_Ord 

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

898 

899 

900 
(*** Finite sets ***) 

901 

902 
lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n > A : Fin(A)" 

903 
apply (induct_tac "n") 

904 
apply (simp (no_asm) add: eqpoll_0_iff) 

905 
apply clarify 

906 
apply (subgoal_tac "EX u. u:A") 

907 
apply (erule exE) 

908 
apply (rule Diff_sing_eqpoll [THEN revcut_rl]) 

909 
prefer 2 apply (assumption) 

910 
apply assumption 

911 
apply (rule_tac b = "A" in cons_Diff [THEN subst]) 

912 
apply assumption 

913 
apply (rule Fin.consI) 

914 
apply blast 

915 
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD]) 

916 
(*Now for the lemma assumed above*) 

917 
apply (unfold eqpoll_def) 

918 
apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type]) 

919 
done 

920 

921 
lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)" 

922 
apply (unfold Finite_def) 

923 
apply (blast intro: Fin_lemma) 

924 
done 

925 

926 
lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)" 

927 
apply (fast intro!: Finite_0 Finite_cons elim: Fin_induct) 

928 
done 

929 

930 
lemma Finite_Fin_iff: "Finite(A) <> A : Fin(A)" 

931 
apply (blast intro: Finite_into_Fin Fin_into_Finite) 

932 
done 

933 

934 
lemma Finite_Un: "[ Finite(A); Finite(B) ] ==> Finite(A Un B)" 

935 
by (blast intro!: Fin_into_Finite Fin_UnI 

936 
dest!: Finite_into_Fin 

937 
intro: Un_upper1 [THEN Fin_mono, THEN subsetD] 

938 
Un_upper2 [THEN Fin_mono, THEN subsetD]) 

939 

940 
lemma Finite_Union: "[ ALL y:X. Finite(y); Finite(X) ] ==> Finite(Union(X))" 

941 
apply (simp add: Finite_Fin_iff) 

942 
apply (rule Fin_UnionI) 

943 
apply (erule Fin_induct) 

944 
apply (simp (no_asm)) 

945 
apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD]) 

946 
done 

947 

948 
(* Induction principle for Finite(A), by Sidi Ehmety *) 

949 
lemma Finite_induct: 

950 
"[ Finite(A); P(0); 

951 
!! x B. [ Finite(B); x ~: B; P(B) ] ==> P(cons(x, B)) ] 

952 
==> P(A)" 

953 
apply (erule Finite_into_Fin [THEN Fin_induct]) 

954 
apply (blast intro: Fin_into_Finite)+ 

955 
done 

956 

957 

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

959 

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

961 
apply (erule Fin_induct) 

962 
apply (simp (no_asm) add: lepoll_0_iff) 

963 
apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))") 

964 
apply (simp (no_asm_simp)) 

965 
apply (blast dest!: cons_lepoll_consD) 

966 
apply blast 

967 
done 

968 

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

970 
apply (unfold cardinal_def) 

971 
apply (rule Least_equality) 

972 
apply (fold cardinal_def) 

973 
apply (simp (no_asm) add: succ_def) 

974 
apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll 

975 
elim!: mem_irrefl dest!: Finite_imp_well_ord) 

976 
apply (blast intro: Card_cardinal Card_is_Ord) 

977 
apply (rule notI) 

978 
apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE]) 

979 
apply assumption 

980 
apply assumption 

981 
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) 

982 
apply (erule le_imp_lepoll [THEN lepoll_trans]) 

983 
apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll] 

984 
dest!: Finite_imp_well_ord) 

985 
done 

986 

987 

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

989 
apply (rule_tac b = "A" in cons_Diff [THEN subst]) 

990 
apply assumption 

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

992 
apply (simp (no_asm_simp) add: cons_Diff) 

993 
done 

994 

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

996 
apply (rule succ_leE) 

997 
apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff) 

998 
done 

999 

1000 

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

1002 

1003 
lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard] 

1004 

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

1006 
apply (rule eqpoll_trans) 

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

1008 
apply (erule nat_implies_well_ord)+ 

1009 
apply (simp (no_asm_simp) add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl) 

1010 
done 

1011 

1012 

1013 
(*** Theorems by Sidi Ehmety ***) 

1014 

1015 
(*The contrapositive says ~Finite(A) ==> ~Finite(A{a}) *) 

1016 
lemma Diff_sing_Finite: "Finite(A  {a}) ==> Finite(A)" 

1017 
apply (unfold Finite_def) 

1018 
apply (case_tac "a:A") 

1019 
apply (subgoal_tac [2] "A{a}=A") 

1020 
apply auto 

1021 
apply (rule_tac x = "succ (n) " in bexI) 

1022 
apply (subgoal_tac "cons (a, A  {a}) = A & cons (n, n) = succ (n) ") 

1023 
apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong) 

1024 
apply (auto dest: mem_irrefl) 

1025 
done 

1026 

1027 
(*And the contrapositive of this says 

1028 
[ ~Finite(A); Finite(B) ] ==> ~Finite(AB) *) 

1029 
lemma Diff_Finite [rule_format (no_asm)]: "Finite(B) ==> Finite(AB) > Finite(A)" 

1030 
apply (erule Finite_induct) 

1031 
apply auto 

1032 
apply (case_tac "x:A") 

1033 
apply (subgoal_tac [2] "Acons (x, B) = A  B") 

1034 
apply (subgoal_tac "A  cons (x, B) = (A  B)  {x}") 

1035 
apply (rotate_tac 1) 

1036 
apply simp 

1037 
apply (drule Diff_sing_Finite) 

1038 
apply auto 

1039 
done 

1040 

1041 
lemma Ord_subset_natD [rule_format (no_asm)]: "Ord(i) ==> i <= nat > i : nat  i=nat" 

1042 
apply (erule trans_induct3) 

1043 
apply auto 

1044 
apply (blast dest!: nat_le_Limit [THEN le_imp_subset]) 

1045 
done 

1046 

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

1048 
apply (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) 

1049 
done 

1050 

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

1052 
apply (erule Finite_induct) 

1053 
apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons) 

1054 
done 

1055 

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

1057 
apply (rule succ_inject) 

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

1059 
apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff) 

1060 
apply (subgoal_tac "1 \<lesssim> A") 

1061 
prefer 2 apply (blast intro: not_0_is_lepoll_1) 

1062 
apply (frule Finite_imp_well_ord) 

1063 
apply clarify 

1064 
apply (rotate_tac 1) 

1065 
apply (drule well_ord_lepoll_imp_Card_le) 

1066 
apply (auto simp add: cardinal_1) 

1067 
apply (rule trans) 

1068 
apply (rule_tac [2] diff_succ) 

1069 
apply (auto simp add: Finite_cardinal_in_nat) 

1070 
done 

1071 

1072 
lemma cardinal_lt_imp_Diff_not_0 [rule_format (no_asm)]: "Finite(B) ==> ALL A. B<A > A  B ~= 0" 

1073 
apply (erule Finite_induct) 

1074 
apply auto 

1075 
apply (simp_all add: Finite_imp_cardinal_cons) 

1076 
apply (case_tac "Finite (A) ") 

1077 
apply (subgoal_tac [2] "Finite (cons (x, B))") 

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

1079 
apply (auto simp add: Finite_0 Finite_cons) 

1080 
apply (subgoal_tac "B<A") 

1081 
prefer 2 apply (blast intro: lt_trans Ord_cardinal) 

1082 
apply (case_tac "x:A") 

1083 
apply (subgoal_tac [2] "A  cons (x, B) = A  B") 

1084 
apply auto 

1085 
apply (subgoal_tac "A le cons (x, B) ") 

1086 
prefer 2 

1087 
apply (blast dest: Finite_cons [THEN Finite_imp_well_ord] 

1088 
intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll) 

1089 
apply (auto simp add: Finite_imp_cardinal_cons) 

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

1091 
apply (blast intro: lt_trans) 

1092 
done 

1093 

1094 

1095 
ML{* 

1096 
val InfCard_def = thm "InfCard_def" 

1097 
val cmult_def = thm "cmult_def" 

1098 
val cadd_def = thm "cadd_def" 

1099 
val jump_cardinal_def = thm "jump_cardinal_def" 

1100 
val csucc_def = thm "csucc_def" 

1101 

1102 
val sum_commute_eqpoll = thm "sum_commute_eqpoll"; 

1103 
val cadd_commute = thm "cadd_commute"; 

1104 
val sum_assoc_eqpoll = thm "sum_assoc_eqpoll"; 

1105 
val well_ord_cadd_assoc = thm "well_ord_cadd_assoc"; 

1106 
val sum_0_eqpoll = thm "sum_0_eqpoll"; 

1107 
val cadd_0 = thm "cadd_0"; 

1108 
val sum_lepoll_self = thm "sum_lepoll_self"; 

1109 
val cadd_le_self = thm "cadd_le_self"; 

1110 
val sum_lepoll_mono = thm "sum_lepoll_mono"; 

1111 
val cadd_le_mono = thm "cadd_le_mono"; 

1112 
val eq_imp_not_mem = thm "eq_imp_not_mem"; 

1113 
val sum_succ_eqpoll = thm "sum_succ_eqpoll"; 

1114 
val nat_cadd_eq_add = thm "nat_cadd_eq_add"; 

1115 
val prod_commute_eqpoll = thm "prod_commute_eqpoll"; 

1116 
val cmult_commute = thm "cmult_commute"; 

1117 
val prod_assoc_eqpoll = thm "prod_assoc_eqpoll"; 

1118 
val well_ord_cmult_assoc = thm "well_ord_cmult_assoc"; 

1119 
val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll"; 

1120 
val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib"; 

1121 
val prod_0_eqpoll = thm "prod_0_eqpoll"; 

1122 
val cmult_0 = thm "cmult_0"; 

1123 
val prod_singleton_eqpoll = thm "prod_singleton_eqpoll"; 

1124 
val cmult_1 = thm "cmult_1"; 

1125 
val prod_lepoll_self = thm "prod_lepoll_self"; 

1126 
val cmult_le_self = thm "cmult_le_self"; 

1127 
val prod_lepoll_mono = thm "prod_lepoll_mono"; 

1128 
val cmult_le_mono = thm "cmult_le_mono"; 

1129 
val prod_succ_eqpoll = thm "prod_succ_eqpoll"; 

1130 
val nat_cmult_eq_mult = thm "nat_cmult_eq_mult"; 

1131 
val cmult_2 = thm "cmult_2"; 

1132 
val sum_lepoll_prod = thm "sum_lepoll_prod"; 

1133 
val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod"; 

1134 
val nat_cons_lepoll = thm "nat_cons_lepoll"; 

1135 
val nat_cons_eqpoll = thm "nat_cons_eqpoll"; 

1136 
val nat_succ_eqpoll = thm "nat_succ_eqpoll"; 

1137 
val InfCard_nat = thm "InfCard_nat"; 

1138 
val InfCard_is_Card = thm "InfCard_is_Card"; 

1139 
val InfCard_Un = thm "InfCard_Un"; 

1140 
val InfCard_is_Limit = thm "InfCard_is_Limit"; 

1141 
val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred"; 

1142 
val ordermap_z_lt = thm "ordermap_z_lt"; 

1143 
val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq"; 

1144 
val InfCard_cmult_eq = thm "InfCard_cmult_eq"; 

1145 
val InfCard_cdouble_eq = thm "InfCard_cdouble_eq"; 

1146 
val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq"; 

1147 
val InfCard_cadd_eq = thm "InfCard_cadd_eq"; 

1148 
val Ord_jump_cardinal = thm "Ord_jump_cardinal"; 

1149 
val jump_cardinal_iff = thm "jump_cardinal_iff"; 

1150 
val K_lt_jump_cardinal = thm "K_lt_jump_cardinal"; 

1151 
val Card_jump_cardinal = thm "Card_jump_cardinal"; 

1152 
val csucc_basic = thm "csucc_basic"; 

1153 
val Card_csucc = thm "Card_csucc"; 

1154 
val lt_csucc = thm "lt_csucc"; 

1155 
val Ord_0_lt_csucc = thm "Ord_0_lt_csucc"; 

1156 
val csucc_le = thm "csucc_le"; 

1157 
val lt_csucc_iff = thm "lt_csucc_iff"; 

1158 
val Card_lt_csucc_iff = thm "Card_lt_csucc_iff"; 

1159 
val InfCard_csucc = thm "InfCard_csucc"; 

1160 
val Finite_into_Fin = thm "Finite_into_Fin"; 

1161 
val Fin_into_Finite = thm "Fin_into_Finite"; 

1162 
val Finite_Fin_iff = thm "Finite_Fin_iff"; 

1163 
val Finite_Un = thm "Finite_Un"; 

1164 
val Finite_Union = thm "Finite_Union"; 

1165 
val Finite_induct = thm "Finite_induct"; 

1166 
val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll"; 

1167 
val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons"; 

1168 
val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff"; 

1169 
val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff"; 

1170 
val nat_implies_well_ord = thm "nat_implies_well_ord"; 

1171 
val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum"; 

1172 
val Diff_sing_Finite = thm "Diff_sing_Finite"; 

1173 
val Diff_Finite = thm "Diff_Finite"; 

1174 
val Ord_subset_natD = thm "Ord_subset_natD"; 

1175 
val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card"; 

1176 
val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat"; 

1177 
val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1"; 

1178 
val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0"; 

1179 
*} 

1180 

437  1181 
end 