author  paulson 
Tue, 06 Mar 2012 16:06:52 +0000  
changeset 46821  ff6b0c1087f2 
parent 46820  c656222c4dc1 
child 46841  49b91b716cbe 
permissions  rwrr 
1478  1 
(* Title: ZF/CardinalArith.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

437  3 
Copyright 1994 University of Cambridge 
13328  4 
*) 
13216  5 

13328  6 
header{*Cardinal Arithmetic Without the Axiom of Choice*} 
437  7 

16417  8 
theory CardinalArith imports Cardinal OrderArith ArithSimp Finite begin 
467  9 

24893  10 
definition 
11 
InfCard :: "i=>o" where 

46820  12 
"InfCard(i) == Card(i) & nat \<le> i" 
437  13 

24893  14 
definition 
15 
cmult :: "[i,i]=>i" (infixl "*" 70) where 

12667  16 
"i * j == i*j" 
46820  17 

24893  18 
definition 
19 
cadd :: "[i,i]=>i" (infixl "+" 65) where 

12667  20 
"i + j == i+j" 
437  21 

24893  22 
definition 
23 
csquare_rel :: "i=>i" where 

46820  24 
"csquare_rel(K) == 
25 
rvimage(K*K, 

26 
lam <x,y>:K*K. <x \<union> y, x, y>, 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27517
diff
changeset

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

24893  29 
definition 
30 
jump_cardinal :: "i=>i" where 

14883  31 
{*This def is more complex than Kunen's but it more easily proved to 
32 
be a cardinal*} 

46820  33 
"jump_cardinal(K) == 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

34 
\<Union>X\<in>Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" 
46820  35 

24893  36 
definition 
37 
csucc :: "i=>i" where 

14883  38 
{*needed because @{term "jump_cardinal(K)"} might not be the successor 
39 
of @{term K}*} 

12667  40 
"csucc(K) == LEAST L. Card(L) & K<L" 
484  41 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

42 
notation (xsymbols) 
24893  43 
cadd (infixl "\<oplus>" 65) and 
44 
cmult (infixl "\<otimes>" 70) 

45 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

46 
notation (HTML) 
24893  47 
cadd (infixl "\<oplus>" 65) and 
48 
cmult (infixl "\<otimes>" 70) 

12667  49 

50 

46820  51 
lemma Card_Union [simp,intro,TC]: "(\<forall>x\<in>A. Card(x)) ==> Card(\<Union>(A))" 
52 
apply (rule CardI) 

53 
apply (simp add: Card_is_Ord) 

12667  54 
apply (clarify dest!: ltD) 
46820  55 
apply (drule bspec, assumption) 
56 
apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 

12667  57 
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) 
46820  58 
apply (drule lesspoll_trans1, assumption) 
13216  59 
apply (subgoal_tac "B \<lesssim> \<Union>A") 
46820  60 
apply (drule lesspoll_trans1, assumption, blast) 
61 
apply (blast intro: subset_imp_lepoll) 

12667  62 
done 
63 

46820  64 
lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))" 
65 
by (blast intro: Card_Union) 

12667  66 

67 
lemma Card_OUN [simp,intro,TC]: 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

68 
"(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))" 
46820  69 
by (simp add: OUnion_def Card_0) 
9654
9754ba005b64
Xsymbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9548
diff
changeset

70 

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

73 
apply (rule conjI) 

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

75 
apply (rule notI) 

76 
apply (erule eqpollE) 

77 
apply (rule succ_lepoll_natE) 

46820  78 
apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 
79 
lepoll_trans, assumption) 

12776  80 
done 
81 

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

83 
apply (unfold lesspoll_def) 

84 
apply (simp add: Card_iff_initial) 

85 
apply (fast intro!: le_imp_lepoll ltI leI) 

86 
done 

87 

14883  88 
lemma lesspoll_lemma: "[ ~ A \<prec> B; C \<prec> B ] ==> A  C \<noteq> 0" 
12776  89 
apply (unfold lesspoll_def) 
90 
apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll] 

46820  91 
intro!: eqpollI elim: notE 
12776  92 
elim!: eqpollE lepoll_trans) 
93 
done 

94 

13216  95 

13356  96 
subsection{*Cardinal addition*} 
13216  97 

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

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

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

102 

14883  103 
subsubsection{*Cardinal addition is commutative*} 
13216  104 

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

106 
apply (unfold eqpoll_def) 

107 
apply (rule exI) 

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

109 
apply auto 

110 
done 

111 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

112 
lemma cadd_commute: "i \<oplus> j = j \<oplus> i" 
13216  113 
apply (unfold cadd_def) 
114 
apply (rule sum_commute_eqpoll [THEN cardinal_cong]) 

115 
done 

116 

14883  117 
subsubsection{*Cardinal addition is associative*} 
13216  118 

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

120 
apply (unfold eqpoll_def) 

121 
apply (rule exI) 

122 
apply (rule sum_assoc_bij) 

123 
done 

124 

125 
(*Unconditional version requires AC*) 

46820  126 
lemma well_ord_cadd_assoc: 
13216  127 
"[ well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) ] 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

128 
==> (i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)" 
13216  129 
apply (unfold cadd_def) 
130 
apply (rule cardinal_cong) 

131 
apply (rule eqpoll_trans) 

132 
apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 

46820  133 
apply (blast intro: well_ord_radd ) 
13216  134 
apply (rule sum_assoc_eqpoll [THEN eqpoll_trans]) 
135 
apply (rule eqpoll_sym) 

136 
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

46820  137 
apply (blast intro: well_ord_radd ) 
13216  138 
done 
139 

14883  140 
subsubsection{*0 is the identity for addition*} 
13216  141 

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

143 
apply (unfold eqpoll_def) 

144 
apply (rule exI) 

145 
apply (rule bij_0_sum) 

146 
done 

147 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

148 
lemma cadd_0 [simp]: "Card(K) ==> 0 \<oplus> K = K" 
13216  149 
apply (unfold cadd_def) 
150 
apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq) 

151 
done 

152 

14883  153 
subsubsection{*Addition by another cardinal*} 
13216  154 

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

156 
apply (unfold lepoll_def inj_def) 

46820  157 
apply (rule_tac x = "\<lambda>x\<in>A. Inl (x) " in exI) 
13221  158 
apply simp 
13216  159 
done 
160 

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

162 

46820  163 
lemma cadd_le_self: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

164 
"[ Card(K); Ord(L) ] ==> K \<le> (K \<oplus> L)" 
13216  165 
apply (unfold cadd_def) 
13221  166 
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le], 
167 
assumption) 

13216  168 
apply (rule_tac [2] sum_lepoll_self) 
169 
apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord) 

170 
done 

171 

14883  172 
subsubsection{*Monotonicity of addition*} 
13216  173 

46820  174 
lemma sum_lepoll_mono: 
13221  175 
"[ A \<lesssim> C; B \<lesssim> D ] ==> A + B \<lesssim> C + D" 
13216  176 
apply (unfold lepoll_def) 
13221  177 
apply (elim exE) 
46820  178 
apply (rule_tac x = "\<lambda>z\<in>A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI) 
13221  179 
apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) ` y))" 
13216  180 
in lam_injective) 
13221  181 
apply (typecheck add: inj_is_fun, auto) 
13216  182 
done 
183 

184 
lemma cadd_le_mono: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

185 
"[ K' \<le> K; L' \<le> L ] ==> (K' \<oplus> L') \<le> (K \<oplus> L)" 
13216  186 
apply (unfold cadd_def) 
187 
apply (safe dest!: le_subset_iff [THEN iffD1]) 

188 
apply (rule well_ord_lepoll_imp_Card_le) 

189 
apply (blast intro: well_ord_radd well_ord_Memrel) 

190 
apply (blast intro: sum_lepoll_mono subset_imp_lepoll) 

191 
done 

192 

14883  193 
subsubsection{*Addition of finite cardinals is "ordinary" addition*} 
13216  194 

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

196 
apply (unfold eqpoll_def) 

197 
apply (rule exI) 

46820  198 
apply (rule_tac c = "%z. if z=Inl (A) then A+B else z" 
13216  199 
and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective) 
13221  200 
apply simp_all 
13216  201 
apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+ 
202 
done 

203 

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

205 
(*Unconditional version requires AC*) 

206 
lemma cadd_succ_lemma: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

207 
"[ Ord(m); Ord(n) ] ==> succ(m) \<oplus> n = succ(m \<oplus> n)" 
13216  208 
apply (unfold cadd_def) 
209 
apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans]) 

210 
apply (rule succ_eqpoll_cong [THEN cardinal_cong]) 

211 
apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym]) 

212 
apply (blast intro: well_ord_radd well_ord_Memrel) 

213 
done 

214 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

215 
lemma nat_cadd_eq_add: "[ m: nat; n: nat ] ==> m \<oplus> n = m#+n" 
13244  216 
apply (induct_tac m) 
13216  217 
apply (simp add: nat_into_Card [THEN cadd_0]) 
218 
apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq]) 

219 
done 

220 

221 

13356  222 
subsection{*Cardinal multiplication*} 
13216  223 

14883  224 
subsubsection{*Cardinal multiplication is commutative*} 
13216  225 

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

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

228 
apply (unfold eqpoll_def) 

229 
apply (rule exI) 

46820  230 
apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective, 
231 
auto) 

13216  232 
done 
233 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

234 
lemma cmult_commute: "i \<otimes> j = j \<otimes> i" 
13216  235 
apply (unfold cmult_def) 
236 
apply (rule prod_commute_eqpoll [THEN cardinal_cong]) 

237 
done 

238 

14883  239 
subsubsection{*Cardinal multiplication is associative*} 
13216  240 

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

242 
apply (unfold eqpoll_def) 

243 
apply (rule exI) 

244 
apply (rule prod_assoc_bij) 

245 
done 

246 

247 
(*Unconditional version requires AC*) 

248 
lemma well_ord_cmult_assoc: 

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

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

250 
==> (i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" 
13216  251 
apply (unfold cmult_def) 
252 
apply (rule cardinal_cong) 

46820  253 
apply (rule eqpoll_trans) 
13216  254 
apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 
255 
apply (blast intro: well_ord_rmult) 

256 
apply (rule prod_assoc_eqpoll [THEN eqpoll_trans]) 

46820  257 
apply (rule eqpoll_sym) 
13216  258 
apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 
259 
apply (blast intro: well_ord_rmult) 

260 
done 

261 

14883  262 
subsubsection{*Cardinal multiplication distributes over addition*} 
13216  263 

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

265 
apply (unfold eqpoll_def) 

266 
apply (rule exI) 

267 
apply (rule sum_prod_distrib_bij) 

268 
done 

269 

270 
lemma well_ord_cadd_cmult_distrib: 

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

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

272 
==> (i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)" 
13216  273 
apply (unfold cadd_def cmult_def) 
274 
apply (rule cardinal_cong) 

46820  275 
apply (rule eqpoll_trans) 
13216  276 
apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) 
277 
apply (blast intro: well_ord_radd) 

278 
apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans]) 

46820  279 
apply (rule eqpoll_sym) 
280 
apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll 

13216  281 
well_ord_cardinal_eqpoll]) 
282 
apply (blast intro: well_ord_rmult)+ 

283 
done 

284 

14883  285 
subsubsection{*Multiplication by 0 yields 0*} 
13216  286 

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

288 
apply (unfold eqpoll_def) 

289 
apply (rule exI) 

13221  290 
apply (rule lam_bijective, safe) 
13216  291 
done 
292 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

293 
lemma cmult_0 [simp]: "0 \<otimes> i = 0" 
13221  294 
by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong]) 
13216  295 

14883  296 
subsubsection{*1 is the identity for multiplication*} 
13216  297 

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

299 
apply (unfold eqpoll_def) 

300 
apply (rule exI) 

301 
apply (rule singleton_prod_bij [THEN bij_converse_bij]) 

302 
done 

303 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

304 
lemma cmult_1 [simp]: "Card(K) ==> 1 \<otimes> K = K" 
13216  305 
apply (unfold cmult_def succ_def) 
306 
apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq) 

307 
done 

308 

13356  309 
subsection{*Some inequalities for multiplication*} 
13216  310 

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

312 
apply (unfold lepoll_def inj_def) 

46820  313 
apply (rule_tac x = "\<lambda>x\<in>A. <x,x>" in exI, simp) 
13216  314 
done 
315 

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

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

317 
lemma cmult_square_le: "Card(K) ==> K \<le> K \<otimes> K" 
13216  318 
apply (unfold cmult_def) 
319 
apply (rule le_trans) 

320 
apply (rule_tac [2] well_ord_lepoll_imp_Card_le) 

321 
apply (rule_tac [3] prod_square_lepoll) 

13221  322 
apply (simp add: le_refl Card_is_Ord Card_cardinal_eq) 
323 
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) 

13216  324 
done 
325 

14883  326 
subsubsection{*Multiplication by a nonzero cardinal*} 
13216  327 

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

329 
apply (unfold lepoll_def inj_def) 

46820  330 
apply (rule_tac x = "\<lambda>x\<in>A. <x,b>" in exI, simp) 
13216  331 
done 
332 

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

334 
lemma cmult_le_self: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

335 
"[ Card(K); Ord(L); 0<L ] ==> K \<le> (K \<otimes> L)" 
13216  336 
apply (unfold cmult_def) 
337 
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le]) 

13221  338 
apply assumption 
13216  339 
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) 
340 
apply (blast intro: prod_lepoll_self ltD) 

341 
done 

342 

14883  343 
subsubsection{*Monotonicity of multiplication*} 
13216  344 

345 
lemma prod_lepoll_mono: 

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

347 
apply (unfold lepoll_def) 

13221  348 
apply (elim exE) 
13216  349 
apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in exI) 
46820  350 
apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>" 
13216  351 
in lam_injective) 
13221  352 
apply (typecheck add: inj_is_fun, auto) 
13216  353 
done 
354 

355 
lemma cmult_le_mono: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

356 
"[ K' \<le> K; L' \<le> L ] ==> (K' \<otimes> L') \<le> (K \<otimes> L)" 
13216  357 
apply (unfold cmult_def) 
358 
apply (safe dest!: le_subset_iff [THEN iffD1]) 

359 
apply (rule well_ord_lepoll_imp_Card_le) 

360 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

361 
apply (blast intro: prod_lepoll_mono subset_imp_lepoll) 

362 
done 

363 

13356  364 
subsection{*Multiplication of finite cardinals is "ordinary" multiplication*} 
13216  365 

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

367 
apply (unfold eqpoll_def) 

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

371 
apply safe 

372 
apply (simp_all add: succI2 if_type mem_imp_not_eq) 

373 
done 

374 

375 
(*Unconditional version requires AC*) 

376 
lemma cmult_succ_lemma: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

377 
"[ Ord(m); Ord(n) ] ==> succ(m) \<otimes> n = n \<oplus> (m \<otimes> n)" 
13216  378 
apply (unfold cmult_def cadd_def) 
379 
apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans]) 

380 
apply (rule cardinal_cong [symmetric]) 

381 
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

382 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

383 
done 

384 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

385 
lemma nat_cmult_eq_mult: "[ m: nat; n: nat ] ==> m \<otimes> n = m#*n" 
13244  386 
apply (induct_tac m) 
13221  387 
apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add) 
13216  388 
done 
389 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

390 
lemma cmult_2: "Card(n) ==> 2 \<otimes> n = n \<oplus> n" 
13221  391 
by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0]) 
13216  392 

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

46820  394 
apply (rule lepoll_trans) 
395 
apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll]) 

396 
apply (erule prod_lepoll_mono) 

397 
apply (rule lepoll_refl) 

13216  398 
done 
399 

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

13221  401 
by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl) 
13216  402 

403 

13356  404 
subsection{*Infinite Cardinals are Limit Ordinals*} 
13216  405 

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

46820  407 
\<lambda>z\<in>cons(u,A). if z=u then 0 else if z \<in> nat then succ(z) else z 
13216  408 
and inverse %y. if y:nat then nat_case(u, %z. z, y) else y. \ 
409 
If f: inj(nat,A) then range(f) behaves like the natural numbers.*) 

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

411 
apply (unfold lepoll_def) 

412 
apply (erule exE) 

46820  413 
apply (rule_tac x = 
414 
"\<lambda>z\<in>cons (u,A). 

415 
if z=u then f`0 

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

13216  417 
in exI) 
418 
apply (rule_tac d = 

46820  419 
"%y. if y: range(f) then nat_case (u, %z. f`z, converse(f) `y) 
420 
else y" 

13216  421 
in lam_injective) 
422 
apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun) 

423 
apply (simp add: inj_is_fun [THEN apply_rangeI] 

424 
inj_converse_fun [THEN apply_rangeI] 

425 
inj_converse_fun [THEN apply_funtype]) 

426 
done 

427 

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

429 
apply (erule nat_cons_lepoll [THEN eqpollI]) 

430 
apply (rule subset_consI [THEN subset_imp_lepoll]) 

431 
done 

432 

433 
(*Specialized version required below*) 

46820  434 
lemma nat_succ_eqpoll: "nat \<subseteq> A ==> succ(A) \<approx> A" 
13216  435 
apply (unfold succ_def) 
436 
apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll]) 

437 
done 

438 

439 
lemma InfCard_nat: "InfCard(nat)" 

440 
apply (unfold InfCard_def) 

441 
apply (blast intro: Card_nat le_refl Card_is_Ord) 

442 
done 

443 

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

445 
apply (unfold InfCard_def) 

446 
apply (erule conjunct1) 

447 
done 

448 

449 
lemma InfCard_Un: 

46820  450 
"[ InfCard(K); Card(L) ] ==> InfCard(K \<union> L)" 
13216  451 
apply (unfold InfCard_def) 
452 
apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans] Card_is_Ord) 

453 
done 

454 

455 
(*Kunen's Lemma 10.11*) 

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

457 
apply (unfold InfCard_def) 

458 
apply (erule conjE) 

459 
apply (frule Card_is_Ord) 

460 
apply (rule ltI [THEN non_succ_LimitI]) 

461 
apply (erule le_imp_subset [THEN subsetD]) 

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

463 
apply (unfold Card_def) 

464 
apply (drule trans) 

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

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

13221  467 
apply (rule le_eqI, assumption) 
13216  468 
apply (rule Ord_cardinal) 
469 
done 

470 

471 

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

473 

474 
(*A general fact about ordermap*) 

475 
lemma ordermap_eqpoll_pred: 

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

13221  479 
apply (simp add: ordermap_eq_image well_ord_is_wf) 
46820  480 
apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, 
13221  481 
THEN bij_converse_bij]) 
13216  482 
apply (rule pred_subset) 
483 
done 

484 

14883  485 
subsubsection{*Establishing the wellordering*} 
13216  486 

487 
lemma csquare_lam_inj: 

46820  488 
"Ord(K) ==> (lam <x,y>:K*K. <x \<union> y, x, y>) \<in> inj(K*K, K*K*K)" 
13216  489 
apply (unfold inj_def) 
490 
apply (force intro: lam_type Un_least_lt [THEN ltD] ltI) 

491 
done 

492 

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

494 
apply (unfold csquare_rel_def) 

13221  495 
apply (rule csquare_lam_inj [THEN well_ord_rvimage], assumption) 
13216  496 
apply (blast intro: well_ord_rmult well_ord_Memrel) 
497 
done 

498 

14883  499 
subsubsection{*Characterising initial segments of the wellordering*} 
13216  500 

501 
lemma csquareD: 

46820  502 
"[ <<x,y>, <z,z>> \<in> csquare_rel(K); x<K; y<K; z<K ] ==> x \<le> z & y \<le> z" 
13216  503 
apply (unfold csquare_rel_def) 
504 
apply (erule rev_mp) 

505 
apply (elim ltE) 

13221  506 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  507 
apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le) 
13221  508 
apply (simp_all add: lt_def succI2) 
13216  509 
done 
510 

46820  511 
lemma pred_csquare_subset: 
512 
"z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) \<subseteq> succ(z)*succ(z)" 

13216  513 
apply (unfold Order.pred_def) 
514 
apply (safe del: SigmaI succCI) 

515 
apply (erule csquareD [THEN conjE]) 

46820  516 
apply (unfold lt_def, auto) 
13216  517 
done 
518 

519 
lemma csquare_ltI: 

46820  520 
"[ x<z; y<z; z<K ] ==> <<x,y>, <z,z>> \<in> csquare_rel(K)" 
13216  521 
apply (unfold csquare_rel_def) 
522 
apply (subgoal_tac "x<K & y<K") 

46820  523 
prefer 2 apply (blast intro: lt_trans) 
13216  524 
apply (elim ltE) 
13221  525 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  526 
done 
527 

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

529 
lemma csquare_or_eqI: 

46820  530 
"[ x \<le> z; y \<le> z; z<K ] ==> <<x,y>, <z,z>> \<in> csquare_rel(K)  x=z & y=z" 
13216  531 
apply (unfold csquare_rel_def) 
532 
apply (subgoal_tac "x<K & y<K") 

46820  533 
prefer 2 apply (blast intro: lt_trans1) 
13216  534 
apply (elim ltE) 
13221  535 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  536 
apply (elim succE) 
46820  537 
apply (simp_all add: subset_Un_iff [THEN iff_sym] 
13221  538 
subset_Un_iff2 [THEN iff_sym] OrdmemD) 
13216  539 
done 
540 

14883  541 
subsubsection{*The cardinality of initial segments*} 
13216  542 

543 
lemma ordermap_z_lt: 

46820  544 
"[ Limit(K); x<K; y<K; z=succ(x \<union> y) ] ==> 
13216  545 
ordermap(K*K, csquare_rel(K)) ` <x,y> < 
546 
ordermap(K*K, csquare_rel(K)) ` <z,z>" 

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

548 
prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ 

46820  549 
Limit_is_Ord [THEN well_ord_csquare], clarify) 
13216  550 
apply (rule csquare_ltI [THEN ordermap_mono, THEN ltI]) 
551 
apply (erule_tac [4] well_ord_is_wf) 

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

553 
done 

554 

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

556 
lemma ordermap_csquare_le: 

46820  557 
"[ Limit(K); x<K; y<K; z=succ(x \<union> y) ] 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

558 
==>  ordermap(K*K, csquare_rel(K)) ` <x,y>  \<le> succ(z) \<otimes> succ(z)" 
13216  559 
apply (unfold cmult_def) 
560 
apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le]) 

561 
apply (rule Ord_cardinal [THEN well_ord_Memrel])+ 

562 
apply (subgoal_tac "z<K") 

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

46820  564 
apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans], 
13221  565 
assumption+) 
13216  566 
apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) 
567 
apply (erule Limit_is_Ord [THEN well_ord_csquare]) 

568 
apply (blast intro: ltD) 

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

570 
assumption) 

571 
apply (elim ltE) 

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

573 
apply (erule Ord_succ [THEN Ord_cardinal_eqpoll])+ 

574 
done 

575 

46820  576 
(*Kunen: "... so the order type is @{text"\<le>"} K" *) 
13216  577 
lemma ordertype_csquare_le: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

578 
"[ InfCard(K); \<forall>y\<in>K. InfCard(y) \<longrightarrow> y \<otimes> y = y ] 
46820  579 
==> ordertype(K*K, csquare_rel(K)) \<le> K" 
13216  580 
apply (frule InfCard_is_Card [THEN Card_is_Ord]) 
13221  581 
apply (rule all_lt_imp_le, assumption) 
13216  582 
apply (erule well_ord_csquare [THEN Ord_ordertype]) 
583 
apply (rule Card_lt_imp_lt) 

584 
apply (erule_tac [3] InfCard_is_Card) 

585 
apply (erule_tac [2] ltE) 

586 
apply (simp add: ordertype_unfold) 

587 
apply (safe elim!: ltE) 

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

13221  589 
prefer 2 apply (blast intro: Ord_in_Ord, clarify) 
46820  590 
(*??WHAT A MESS!*) 
13216  591 
apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1], 
46820  592 
(assumption  rule refl  erule ltI)+) 
593 
apply (rule_tac i = "xa \<union> ya" and j = nat in Ord_linear2, 

13216  594 
simp_all add: Ord_Un Ord_nat) 
46820  595 
prefer 2 (*case @{term"nat \<le> (xa \<union> ya)"} *) 
596 
apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] 

13216  597 
le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un 
598 
ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD]) 

46820  599 
(*the finite case: @{term"xa \<union> ya < nat"} *) 
13784  600 
apply (rule_tac j = nat in lt_trans2) 
13216  601 
apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type 
602 
nat_into_Card [THEN Card_cardinal_eq] Ord_nat) 

603 
apply (simp add: InfCard_def) 

604 
done 

605 

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

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

607 
lemma InfCard_csquare_eq: "InfCard(K) ==> K \<otimes> K = K" 
13216  608 
apply (frule InfCard_is_Card [THEN Card_is_Ord]) 
609 
apply (erule rev_mp) 

46820  610 
apply (erule_tac i=K in trans_induct) 
13216  611 
apply (rule impI) 
612 
apply (rule le_anti_sym) 

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

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

46820  615 
apply (simp add: cmult_def Ord_cardinal_le 
13221  616 
well_ord_csquare [THEN Ord_ordertype] 
46820  617 
well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll, 
13221  618 
THEN cardinal_cong], assumption+) 
13216  619 
done 
620 

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

622 
lemma well_ord_InfCard_square_eq: 

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

624 
apply (rule prod_eqpoll_cong [THEN eqpoll_trans]) 

625 
apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+ 

626 
apply (rule well_ord_cardinal_eqE) 

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

13216  629 
done 
630 

13356  631 
lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K" 
46820  632 
apply (rule well_ord_InfCard_square_eq) 
633 
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) 

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

13356  635 
done 
636 

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

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

639 

14883  640 
subsubsection{*Toward's Kunen's Corollary 10.13 (1)*} 
13216  641 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

642 
lemma InfCard_le_cmult_eq: "[ InfCard(K); L \<le> K; 0<L ] ==> K \<otimes> L = K" 
13216  643 
apply (rule le_anti_sym) 
644 
prefer 2 

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

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

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

648 
apply (simp add: InfCard_csquare_eq) 

649 
done 

650 

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

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

652 
lemma InfCard_cmult_eq: "[ InfCard(K); InfCard(L) ] ==> K \<otimes> L = K \<union> L" 
13784  653 
apply (rule_tac i = K and j = L in Ord_linear_le) 
13216  654 
apply (typecheck add: InfCard_is_Card Card_is_Ord) 
655 
apply (rule cmult_commute [THEN ssubst]) 

656 
apply (rule Un_commute [THEN ssubst]) 

46820  657 
apply (simp_all add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq 
13221  658 
subset_Un_iff2 [THEN iffD1] le_imp_subset) 
13216  659 
done 
660 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

661 
lemma InfCard_cdouble_eq: "InfCard(K) ==> K \<oplus> K = K" 
13221  662 
apply (simp add: cmult_2 [symmetric] InfCard_is_Card cmult_commute) 
663 
apply (simp add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ) 

13216  664 
done 
665 

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

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

667 
lemma InfCard_le_cadd_eq: "[ InfCard(K); L \<le> K ] ==> K \<oplus> L = K" 
13216  668 
apply (rule le_anti_sym) 
669 
prefer 2 

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

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

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

673 
apply (simp add: InfCard_cdouble_eq) 

674 
done 

675 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

676 
lemma InfCard_cadd_eq: "[ InfCard(K); InfCard(L) ] ==> K \<oplus> L = K \<union> L" 
13784  677 
apply (rule_tac i = K and j = L in Ord_linear_le) 
13216  678 
apply (typecheck add: InfCard_is_Card Card_is_Ord) 
679 
apply (rule cadd_commute [THEN ssubst]) 

680 
apply (rule Un_commute [THEN ssubst]) 

13221  681 
apply (simp_all add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) 
13216  682 
done 
683 

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

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

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

687 
*) 

688 

27517  689 
subsection{*For Every Cardinal Number There Exists A Greater One*} 
13356  690 

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

13216  692 

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

694 
apply (unfold jump_cardinal_def) 

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

696 
prefer 2 apply (blast intro!: Ord_ordertype) 

697 
apply (unfold Transset_def) 

698 
apply (safe del: subsetI) 

13221  699 
apply (simp add: ordertype_pred_unfold, safe) 
13216  700 
apply (rule UN_I) 
701 
apply (rule_tac [2] ReplaceI) 

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

703 
done 

704 

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

706 
lemma jump_cardinal_iff: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

707 
"i \<in> jump_cardinal(K) \<longleftrightarrow> 
46820  708 
(\<exists>r X. r \<subseteq> K*K & X \<subseteq> K & well_ord(X,r) & i = ordertype(X,r))" 
13216  709 
apply (unfold jump_cardinal_def) 
46820  710 
apply (blast del: subsetI) 
13216  711 
done 
712 

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

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

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

716 
apply (rule jump_cardinal_iff [THEN iffD2]) 

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

46820  718 
apply (rule_tac x=K in exI) 
13216  719 
apply (simp add: ordertype_Memrel well_ord_Memrel) 
720 
apply (simp add: Memrel_def subset_iff) 

721 
done 

722 

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

724 
whose ordertype is jump_cardinal(K). *) 

725 
lemma Card_jump_cardinal_lemma: 

46820  726 
"[ well_ord(X,r); r \<subseteq> K * K; X \<subseteq> K; 
727 
f \<in> bij(ordertype(X,r), jump_cardinal(K)) ] 

728 
==> jump_cardinal(K) \<in> jump_cardinal(K)" 

729 
apply (subgoal_tac "f O ordermap (X,r) \<in> bij (X, jump_cardinal (K))") 

13216  730 
prefer 2 apply (blast intro: comp_bij ordermap_bij) 
731 
apply (rule jump_cardinal_iff [THEN iffD2]) 

732 
apply (intro exI conjI) 

13221  733 
apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+) 
13216  734 
apply (erule bij_is_inj [THEN well_ord_rvimage]) 
735 
apply (rule Ord_jump_cardinal [THEN well_ord_Memrel]) 

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

737 
ordertype_Memrel Ord_jump_cardinal) 

738 
done 

739 

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

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

742 
apply (rule Ord_jump_cardinal [THEN CardI]) 

743 
apply (unfold eqpoll_def) 

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

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

746 
done 

747 

13356  748 
subsection{*Basic Properties of Successor Cardinals*} 
13216  749 

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

751 
apply (unfold csucc_def) 

752 
apply (rule LeastI) 

753 
apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ 

754 
done 

755 

45602  756 
lemmas Card_csucc = csucc_basic [THEN conjunct1] 
13216  757 

45602  758 
lemmas lt_csucc = csucc_basic [THEN conjunct2] 
13216  759 

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

13221  761 
by (blast intro: Ord_0_le lt_csucc lt_trans1) 
13216  762 

46820  763 
lemma csucc_le: "[ Card(L); K<L ] ==> csucc(K) \<le> L" 
13216  764 
apply (unfold csucc_def) 
765 
apply (rule Least_le) 

766 
apply (blast intro: Card_is_Ord)+ 

767 
done 

768 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

769 
lemma lt_csucc_iff: "[ Ord(i); Card(K) ] ==> i < csucc(K) \<longleftrightarrow> i \<le> K" 
13216  770 
apply (rule iffI) 
771 
apply (rule_tac [2] Card_lt_imp_lt) 

772 
apply (erule_tac [2] lt_trans1) 

773 
apply (simp_all add: lt_csucc Card_csucc Card_is_Ord) 

774 
apply (rule notI [THEN not_lt_imp_le]) 

13221  775 
apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl], assumption) 
13216  776 
apply (rule Ord_cardinal_le [THEN lt_trans1]) 
46820  777 
apply (simp_all add: Ord_cardinal Card_is_Ord) 
13216  778 
done 
779 

780 
lemma Card_lt_csucc_iff: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

781 
"[ Card(K'); Card(K) ] ==> K' < csucc(K) \<longleftrightarrow> K' \<le> K" 
13221  782 
by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord) 
13216  783 

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

46820  785 
by (simp add: InfCard_def Card_csucc Card_is_Ord 
13216  786 
lt_csucc [THEN leI, THEN [2] le_trans]) 
787 

788 

14883  789 
subsubsection{*Removing elements from a finite set decreases its cardinality*} 
13216  790 

46820  791 
lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x\<notin>A \<longrightarrow> ~ cons(x,A) \<lesssim> A" 
13216  792 
apply (erule Fin_induct) 
13221  793 
apply (simp add: lepoll_0_iff) 
13216  794 
apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))") 
13221  795 
apply simp 
796 
apply (blast dest!: cons_lepoll_consD, blast) 

13216  797 
done 
798 

14883  799 
lemma Finite_imp_cardinal_cons [simp]: 
46820  800 
"[ Finite(A); a\<notin>A ] ==> cons(a,A) = succ(A)" 
13216  801 
apply (unfold cardinal_def) 
802 
apply (rule Least_equality) 

803 
apply (fold cardinal_def) 

13221  804 
apply (simp add: succ_def) 
13216  805 
apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll 
806 
elim!: mem_irrefl dest!: Finite_imp_well_ord) 

807 
apply (blast intro: Card_cardinal Card_is_Ord) 

808 
apply (rule notI) 

13221  809 
apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE], 
810 
assumption, assumption) 

13216  811 
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) 
812 
apply (erule le_imp_lepoll [THEN lepoll_trans]) 

813 
apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll] 

814 
dest!: Finite_imp_well_ord) 

815 
done 

816 

817 

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

13784  820 
apply (rule_tac b = A in cons_Diff [THEN subst], assumption) 
13221  821 
apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite]) 
822 
apply (simp add: cons_Diff) 

13216  823 
done 
824 

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

826 
apply (rule succ_leE) 

13221  827 
apply (simp add: Finite_imp_succ_cardinal_Diff) 
13216  828 
done 
829 

46820  830 
lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> A \<in> nat" 
14883  831 
apply (erule Finite_induct) 
832 
apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons) 

833 
done 

13216  834 

14883  835 
lemma card_Un_Int: 
46820  836 
"[Finite(A); Finite(B)] ==> A #+ B = A \<union> B #+ A \<inter> B" 
837 
apply (erule Finite_induct, simp) 

14883  838 
apply (simp add: Finite_Int cons_absorb Un_cons Int_cons_left) 
839 
done 

840 

46820  841 
lemma card_Un_disjoint: 
842 
"[Finite(A); Finite(B); A \<inter> B = 0] ==> A \<union> B = A #+ B" 

14883  843 
by (simp add: Finite_Un card_Un_Int) 
844 

845 
lemma card_partition [rule_format]: 

46820  846 
"Finite(C) ==> 
847 
Finite (\<Union> C) \<longrightarrow> 

848 
(\<forall>c\<in>C. c = k) \<longrightarrow> 

849 
(\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = 0) \<longrightarrow> 

14883  850 
k #* C = \<Union> C" 
851 
apply (erule Finite_induct, auto) 

46820  852 
apply (subgoal_tac " x \<inter> \<Union>B = 0") 
14883  853 
apply (auto simp add: card_Un_disjoint Finite_Union 
854 
subset_Finite [of _ "\<Union> (cons(x,F))"]) 

855 
done 

856 

857 

858 
subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*} 

13216  859 

45602  860 
lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel] 
13216  861 

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

863 
apply (rule eqpoll_trans) 

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

865 
apply (erule nat_implies_well_ord)+ 

13221  866 
apply (simp add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl) 
13216  867 
done 
868 

46820  869 
lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<longrightarrow> i \<in> nat  i=nat" 
13221  870 
apply (erule trans_induct3, auto) 
13216  871 
apply (blast dest!: nat_le_Limit [THEN le_imp_subset]) 
872 
done 

873 

46820  874 
lemma Ord_nat_subset_into_Card: "[ Ord(i); i \<subseteq> nat ] ==> Card(i)" 
13221  875 
by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) 
13216  876 

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

878 
apply (rule succ_inject) 

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

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

880 
apply (simp add: Finite_imp_succ_cardinal_Diff) 
13216  881 
apply (subgoal_tac "1 \<lesssim> A") 
13221  882 
prefer 2 apply (blast intro: not_0_is_lepoll_1) 
883 
apply (frule Finite_imp_well_ord, clarify) 

13216  884 
apply (drule well_ord_lepoll_imp_Card_le) 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

885 
apply (auto simp add: cardinal_1) 
13216  886 
apply (rule trans) 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

887 
apply (rule_tac [2] diff_succ) 
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

888 
apply (auto simp add: Finite_cardinal_in_nat) 
13216  889 
done 
890 

13221  891 
lemma cardinal_lt_imp_Diff_not_0 [rule_format]: 
46820  892 
"Finite(B) ==> \<forall>A. B<A \<longrightarrow> A  B \<noteq> 0" 
13221  893 
apply (erule Finite_induct, auto) 
894 
apply (case_tac "Finite (A)") 

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

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

897 
apply (auto simp add: Finite_0 Finite_cons) 

13216  898 
apply (subgoal_tac "B<A") 
13221  899 
prefer 2 apply (blast intro: lt_trans Ord_cardinal) 
13216  900 
apply (case_tac "x:A") 
13221  901 
apply (subgoal_tac [2] "A  cons (x, B) = A  B") 
902 
apply auto 

46820  903 
apply (subgoal_tac "A \<le> cons (x, B) ") 
13221  904 
prefer 2 
46820  905 
apply (blast dest: Finite_cons [THEN Finite_imp_well_ord] 
13216  906 
intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll) 
907 
apply (auto simp add: Finite_imp_cardinal_cons) 

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

909 
apply (blast intro: lt_trans) 

910 
done 

911 

437  912 
end 