author  paulson 
Wed, 14 Mar 2012 17:19:08 +0000  
changeset 46935  38ecb2dc3636 
parent 46907  eea3eb057fea 
child 46952  5e1bcfdcb175 
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 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

51 
lemma Card_Union [simp,intro,TC]: 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

52 
assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

53 
proof (rule CardI) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

54 
show "Ord(\<Union>A)" using A 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

55 
by (simp add: Card_is_Ord) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

56 
next 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

57 
fix j 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

58 
assume j: "j < \<Union>A" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

59 
hence "\<exists>c\<in>A. j < c & Card(c)" using A 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

60 
by (auto simp add: lt_def intro: Card_is_Ord) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

61 
then obtain c where c: "c\<in>A" "j < c" "Card(c)" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

62 
by blast 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

63 
hence jls: "j \<prec> c" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

64 
by (simp add: lt_Card_imp_lesspoll) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

65 
{ assume eqp: "j \<approx> \<Union>A" 
46901  66 
have "c \<lesssim> \<Union>A" using c 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

67 
by (blast intro: subset_imp_lepoll) 
46901  68 
also have "... \<approx> j" by (rule eqpoll_sym [OF eqp]) 
69 
also have "... \<prec> c" by (rule jls) 

70 
finally have "c \<prec> c" . 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

71 
hence False 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

72 
by auto 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

73 
} thus "\<not> j \<approx> \<Union>A" by blast 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

74 
qed 
12667  75 

46820  76 
lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))" 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

77 
by blast 
12667  78 

79 
lemma Card_OUN [simp,intro,TC]: 

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

80 
"(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))" 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

81 
by (auto simp add: OUnion_def Card_0) 
12776  82 

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

84 
apply (unfold lesspoll_def) 

85 
apply (simp add: Card_iff_initial) 

86 
apply (fast intro!: le_imp_lepoll ltI leI) 

87 
done 

88 

13216  89 

13356  90 
subsection{*Cardinal addition*} 
13216  91 

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

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

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

96 

14883  97 
subsubsection{*Cardinal addition is commutative*} 
13216  98 

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

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

100 
proof (unfold eqpoll_def, rule exI) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

101 
show "(\<lambda>z\<in>A+B. case(Inr,Inl,z)) \<in> bij(A+B, B+A)" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

102 
by (auto intro: lam_bijective [where d = "case(Inr,Inl)"]) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

103 
qed 
13216  104 

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

105 
lemma cadd_commute: "i \<oplus> j = j \<oplus> i" 
13216  106 
apply (unfold cadd_def) 
107 
apply (rule sum_commute_eqpoll [THEN cardinal_cong]) 

108 
done 

109 

14883  110 
subsubsection{*Cardinal addition is associative*} 
13216  111 

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

113 
apply (unfold eqpoll_def) 

114 
apply (rule exI) 

115 
apply (rule sum_assoc_bij) 

116 
done 

117 

46901  118 
text{*Unconditional version requires AC*} 
46820  119 
lemma well_ord_cadd_assoc: 
46901  120 
assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)" 
121 
shows "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)" 

122 
proof (unfold cadd_def, rule cardinal_cong) 

123 
have "i + j + k \<approx> (i + j) + k" 

124 
by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 

125 
also have "... \<approx> i + (j + k)" 

126 
by (rule sum_assoc_eqpoll) 

127 
also have "... \<approx> i + j + k" 

128 
by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd j k eqpoll_sym) 

129 
finally show "i + j + k \<approx> i + j + k" . 

130 
qed 

131 

13216  132 

14883  133 
subsubsection{*0 is the identity for addition*} 
13216  134 

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

136 
apply (unfold eqpoll_def) 

137 
apply (rule exI) 

138 
apply (rule bij_0_sum) 

139 
done 

140 

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

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

144 
done 

145 

14883  146 
subsubsection{*Addition by another cardinal*} 
13216  147 

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

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

149 
proof (unfold lepoll_def, rule exI) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

150 
show "(\<lambda>x\<in>A. Inl (x)) \<in> inj(A, A + B)" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

151 
by (simp add: inj_def) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

152 
qed 
13216  153 

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

155 

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

157 
"[ Card(K); Ord(L) ] ==> K \<le> (K \<oplus> L)" 
13216  158 
apply (unfold cadd_def) 
13221  159 
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le], 
160 
assumption) 

13216  161 
apply (rule_tac [2] sum_lepoll_self) 
162 
apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord) 

163 
done 

164 

14883  165 
subsubsection{*Monotonicity of addition*} 
13216  166 

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

177 
lemma cadd_le_mono: 

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

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

181 
apply (rule well_ord_lepoll_imp_Card_le) 

182 
apply (blast intro: well_ord_radd well_ord_Memrel) 

183 
apply (blast intro: sum_lepoll_mono subset_imp_lepoll) 

184 
done 

185 

14883  186 
subsubsection{*Addition of finite cardinals is "ordinary" addition*} 
13216  187 

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

189 
apply (unfold eqpoll_def) 

190 
apply (rule exI) 

46820  191 
apply (rule_tac c = "%z. if z=Inl (A) then A+B else z" 
13216  192 
and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective) 
13221  193 
apply simp_all 
13216  194 
apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+ 
195 
done 

196 

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

198 
(*Unconditional version requires AC*) 

199 
lemma cadd_succ_lemma: 

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

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

203 
apply (rule succ_eqpoll_cong [THEN cardinal_cong]) 

204 
apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym]) 

205 
apply (blast intro: well_ord_radd well_ord_Memrel) 

206 
done 

207 

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

208 
lemma nat_cadd_eq_add: "[ m: nat; n: nat ] ==> m \<oplus> n = m#+n" 
13244  209 
apply (induct_tac m) 
13216  210 
apply (simp add: nat_into_Card [THEN cadd_0]) 
211 
apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq]) 

212 
done 

213 

214 

13356  215 
subsection{*Cardinal multiplication*} 
13216  216 

14883  217 
subsubsection{*Cardinal multiplication is commutative*} 
13216  218 

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

220 
apply (unfold eqpoll_def) 

221 
apply (rule exI) 

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

13216  224 
done 
225 

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

226 
lemma cmult_commute: "i \<otimes> j = j \<otimes> i" 
13216  227 
apply (unfold cmult_def) 
228 
apply (rule prod_commute_eqpoll [THEN cardinal_cong]) 

229 
done 

230 

14883  231 
subsubsection{*Cardinal multiplication is associative*} 
13216  232 

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

234 
apply (unfold eqpoll_def) 

235 
apply (rule exI) 

236 
apply (rule prod_assoc_bij) 

237 
done 

238 

46901  239 
text{*Unconditional version requires AC*} 
13216  240 
lemma well_ord_cmult_assoc: 
46901  241 
assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)" 
242 
shows "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" 

243 
proof (unfold cmult_def, rule cardinal_cong) 

244 
have "i * j * k \<approx> (i * j) * k" 

245 
by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult i j) 

246 
also have "... \<approx> i * (j * k)" 

247 
by (rule prod_assoc_eqpoll) 

248 
also have "... \<approx> i * j * k" 

249 
by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult j k eqpoll_sym) 

250 
finally show "i * j * k \<approx> i * j * k" . 

251 
qed 

13216  252 

14883  253 
subsubsection{*Cardinal multiplication distributes over addition*} 
13216  254 

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

256 
apply (unfold eqpoll_def) 

257 
apply (rule exI) 

258 
apply (rule sum_prod_distrib_bij) 

259 
done 

260 

261 
lemma well_ord_cadd_cmult_distrib: 

46901  262 
assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)" 
263 
shows "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)" 

264 
proof (unfold cadd_def cmult_def, rule cardinal_cong) 

265 
have "i + j * k \<approx> (i + j) * k" 

266 
by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 

267 
also have "... \<approx> i * k + j * k" 

268 
by (rule sum_prod_distrib_eqpoll) 

269 
also have "... \<approx> i * k + j * k" 

270 
by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll well_ord_rmult i j k eqpoll_sym) 

271 
finally show "i + j * k \<approx> i * k + j * k" . 

272 
qed 

13216  273 

14883  274 
subsubsection{*Multiplication by 0 yields 0*} 
13216  275 

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

277 
apply (unfold eqpoll_def) 

278 
apply (rule exI) 

13221  279 
apply (rule lam_bijective, safe) 
13216  280 
done 
281 

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

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

14883  285 
subsubsection{*1 is the identity for multiplication*} 
13216  286 

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

288 
apply (unfold eqpoll_def) 

289 
apply (rule exI) 

290 
apply (rule singleton_prod_bij [THEN bij_converse_bij]) 

291 
done 

292 

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

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

296 
done 

297 

13356  298 
subsection{*Some inequalities for multiplication*} 
13216  299 

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

301 
apply (unfold lepoll_def inj_def) 

46820  302 
apply (rule_tac x = "\<lambda>x\<in>A. <x,x>" in exI, simp) 
13216  303 
done 
304 

305 
(*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

306 
lemma cmult_square_le: "Card(K) ==> K \<le> K \<otimes> K" 
13216  307 
apply (unfold cmult_def) 
308 
apply (rule le_trans) 

309 
apply (rule_tac [2] well_ord_lepoll_imp_Card_le) 

310 
apply (rule_tac [3] prod_square_lepoll) 

13221  311 
apply (simp add: le_refl Card_is_Ord Card_cardinal_eq) 
312 
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) 

13216  313 
done 
314 

14883  315 
subsubsection{*Multiplication by a nonzero cardinal*} 
13216  316 

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

318 
apply (unfold lepoll_def inj_def) 

46820  319 
apply (rule_tac x = "\<lambda>x\<in>A. <x,b>" in exI, simp) 
13216  320 
done 
321 

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

323 
lemma cmult_le_self: 

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

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

13221  327 
apply assumption 
13216  328 
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) 
329 
apply (blast intro: prod_lepoll_self ltD) 

330 
done 

331 

14883  332 
subsubsection{*Monotonicity of multiplication*} 
13216  333 

334 
lemma prod_lepoll_mono: 

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

336 
apply (unfold lepoll_def) 

13221  337 
apply (elim exE) 
13216  338 
apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in exI) 
46820  339 
apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>" 
13216  340 
in lam_injective) 
13221  341 
apply (typecheck add: inj_is_fun, auto) 
13216  342 
done 
343 

344 
lemma cmult_le_mono: 

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

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

348 
apply (rule well_ord_lepoll_imp_Card_le) 

349 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

350 
apply (blast intro: prod_lepoll_mono subset_imp_lepoll) 

351 
done 

352 

13356  353 
subsection{*Multiplication of finite cardinals is "ordinary" multiplication*} 
13216  354 

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

356 
apply (unfold eqpoll_def) 

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

360 
apply safe 

361 
apply (simp_all add: succI2 if_type mem_imp_not_eq) 

362 
done 

363 

364 
(*Unconditional version requires AC*) 

365 
lemma cmult_succ_lemma: 

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

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

369 
apply (rule cardinal_cong [symmetric]) 

370 
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

371 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

372 
done 

373 

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

374 
lemma nat_cmult_eq_mult: "[ m: nat; n: nat ] ==> m \<otimes> n = m#*n" 
13244  375 
apply (induct_tac m) 
13221  376 
apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add) 
13216  377 
done 
378 

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

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

46901  382 
lemma sum_lepoll_prod: 
383 
assumes C: "2 \<lesssim> C" shows "B+B \<lesssim> C*B" 

384 
proof  

385 
have "B+B \<lesssim> 2*B" 

386 
by (simp add: sum_eq_2_times) 

387 
also have "... \<lesssim> C*B" 

388 
by (blast intro: prod_lepoll_mono lepoll_refl C) 

389 
finally show "B+B \<lesssim> C*B" . 

390 
qed 

13216  391 

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

13221  393 
by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl) 
13216  394 

395 

13356  396 
subsection{*Infinite Cardinals are Limit Ordinals*} 
13216  397 

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

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

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

403 
apply (unfold lepoll_def) 

404 
apply (erule exE) 

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

407 
if z=u then f`0 

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

13216  409 
in exI) 
410 
apply (rule_tac d = 

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

13216  413 
in lam_injective) 
414 
apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun) 

415 
apply (simp add: inj_is_fun [THEN apply_rangeI] 

416 
inj_converse_fun [THEN apply_rangeI] 

417 
inj_converse_fun [THEN apply_funtype]) 

418 
done 

419 

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

421 
apply (erule nat_cons_lepoll [THEN eqpollI]) 

422 
apply (rule subset_consI [THEN subset_imp_lepoll]) 

423 
done 

424 

425 
(*Specialized version required below*) 

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

429 
done 

430 

431 
lemma InfCard_nat: "InfCard(nat)" 

432 
apply (unfold InfCard_def) 

433 
apply (blast intro: Card_nat le_refl Card_is_Ord) 

434 
done 

435 

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

437 
apply (unfold InfCard_def) 

438 
apply (erule conjunct1) 

439 
done 

440 

441 
lemma InfCard_Un: 

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

445 
done 

446 

447 
(*Kunen's Lemma 10.11*) 

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

449 
apply (unfold InfCard_def) 

450 
apply (erule conjE) 

451 
apply (frule Card_is_Ord) 

452 
apply (rule ltI [THEN non_succ_LimitI]) 

453 
apply (erule le_imp_subset [THEN subsetD]) 

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

455 
apply (unfold Card_def) 

456 
apply (drule trans) 

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

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

13221  459 
apply (rule le_eqI, assumption) 
13216  460 
apply (rule Ord_cardinal) 
461 
done 

462 

463 

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

465 

466 
(*A general fact about ordermap*) 

467 
lemma ordermap_eqpoll_pred: 

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

13221  471 
apply (simp add: ordermap_eq_image well_ord_is_wf) 
46820  472 
apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, 
13221  473 
THEN bij_converse_bij]) 
13216  474 
apply (rule pred_subset) 
475 
done 

476 

14883  477 
subsubsection{*Establishing the wellordering*} 
13216  478 

46901  479 
lemma well_ord_csquare: 
480 
assumes K: "Ord(K)" shows "well_ord(K*K, csquare_rel(K))" 

481 
proof (unfold csquare_rel_def, rule well_ord_rvimage) 

482 
show "(\<lambda>\<langle>x,y\<rangle>\<in>K \<times> K. \<langle>x \<union> y, x, y\<rangle>) \<in> inj(K \<times> K, K \<times> K \<times> K)" using K 

483 
by (force simp add: inj_def intro: lam_type Un_least_lt [THEN ltD] ltI) 

484 
next 

485 
show "well_ord(K \<times> K \<times> K, rmult(K, Memrel(K), K \<times> K, rmult(K, Memrel(K), K, Memrel(K))))" 

486 
using K by (blast intro: well_ord_rmult well_ord_Memrel) 

487 
qed 

13216  488 

14883  489 
subsubsection{*Characterising initial segments of the wellordering*} 
13216  490 

491 
lemma csquareD: 

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

495 
apply (elim ltE) 

13221  496 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  497 
apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le) 
13221  498 
apply (simp_all add: lt_def succI2) 
13216  499 
done 
500 

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

13216  503 
apply (unfold Order.pred_def) 
46901  504 
apply (safe del: SigmaI dest!: csquareD) 
46820  505 
apply (unfold lt_def, auto) 
13216  506 
done 
507 

508 
lemma csquare_ltI: 

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

46820  512 
prefer 2 apply (blast intro: lt_trans) 
13216  513 
apply (elim ltE) 
13221  514 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  515 
done 
516 

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

518 
lemma csquare_or_eqI: 

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

46820  522 
prefer 2 apply (blast intro: lt_trans1) 
13216  523 
apply (elim ltE) 
13221  524 
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) 
13216  525 
apply (elim succE) 
46820  526 
apply (simp_all add: subset_Un_iff [THEN iff_sym] 
13221  527 
subset_Un_iff2 [THEN iff_sym] OrdmemD) 
13216  528 
done 
529 

14883  530 
subsubsection{*The cardinality of initial segments*} 
13216  531 

532 
lemma ordermap_z_lt: 

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

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

537 
prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ 

46820  538 
Limit_is_Ord [THEN well_ord_csquare], clarify) 
13216  539 
apply (rule csquare_ltI [THEN ordermap_mono, THEN ltI]) 
540 
apply (erule_tac [4] well_ord_is_wf) 

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

542 
done 

543 

46901  544 
text{*Kunen: "each @{term"\<langle>x,y\<rangle> \<in> K \<times> K"} has no more than @{term"z \<times> z"} predecessors..." (page 29) *} 
13216  545 
lemma ordermap_csquare_le: 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

546 
assumes K: "Limit(K)" and x: "x<K" and y: " y<K" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

547 
defines "z \<equiv> succ(x \<union> y)" 
46901  548 
shows "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<le> succ(z) \<otimes> succ(z)" 
549 
proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le) 

550 
show "well_ord(succ(z) \<times> succ(z), 

551 
rmult(succ(z), Memrel(succ(z)), succ(z), Memrel(succ(z))))" 

552 
by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult) 

553 
next 

46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

554 
have zK: "z<K" using x y K z_def 
46901  555 
by (blast intro: Un_least_lt Limit_has_succ) 
556 
hence oz: "Ord(z)" by (elim ltE) 

557 
have "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> ordermap(K \<times> K, csquare_rel(K)) ` \<langle>z,z\<rangle>" 

46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

558 
using z_def 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

559 
by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y) 
46901  560 
also have "... \<approx> Order.pred(K \<times> K, \<langle>z,z\<rangle>, csquare_rel(K))" 
561 
proof (rule ordermap_eqpoll_pred) 

562 
show "well_ord(K \<times> K, csquare_rel(K))" using K 

563 
by (rule Limit_is_Ord [THEN well_ord_csquare]) 

564 
next 

565 
show "\<langle>z, z\<rangle> \<in> K \<times> K" using zK 

566 
by (blast intro: ltD) 

567 
qed 

568 
also have "... \<lesssim> succ(z) \<times> succ(z)" using zK 

569 
by (rule pred_csquare_subset [THEN subset_imp_lepoll]) 

570 
also have "... \<approx> succ(z) \<times> succ(z)" using oz 

571 
by (blast intro: prod_eqpoll_cong Ord_succ Ord_cardinal_eqpoll eqpoll_sym) 

572 
finally show "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> succ(z) \<times> succ(z)" . 

573 
qed 

13216  574 

46901  575 
text{*Kunen: "... so the order type is @{text"\<le>"} K" *} 
13216  576 
lemma ordertype_csquare_le: 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

577 
assumes IK: "InfCard(K)" and eq: "\<And>y. y\<in>K \<Longrightarrow> InfCard(y) \<Longrightarrow> y \<otimes> y = y" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

578 
shows "ordertype(K*K, csquare_rel(K)) \<le> K" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

579 
proof  
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

580 
have CK: "Card(K)" using IK by (rule InfCard_is_Card) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

581 
hence OK: "Ord(K)" by (rule Card_is_Ord) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

582 
moreover have "Ord(ordertype(K \<times> K, csquare_rel(K)))" using OK 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

583 
by (rule well_ord_csquare [THEN Ord_ordertype]) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

584 
ultimately show ?thesis 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

585 
proof (rule all_lt_imp_le) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

586 
fix i 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

587 
assume i: "i < ordertype(K \<times> K, csquare_rel(K))" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

588 
hence Oi: "Ord(i)" by (elim ltE) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

589 
obtain x y where x: "x \<in> K" and y: "y \<in> K" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

590 
and ieq: "i = ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

591 
using i by (auto simp add: ordertype_unfold elim: ltE) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

592 
hence xy: "Ord(x)" "Ord(y)" "x < K" "y < K" using OK 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

593 
by (blast intro: Ord_in_Ord ltI)+ 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

594 
hence ou: "Ord(x \<union> y)" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

595 
by (simp add: Ord_Un) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

596 
show "i < K" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

597 
proof (rule Card_lt_imp_lt [OF _ Oi CK]) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

598 
have "i \<le> succ(succ(x \<union> y)) \<otimes> succ(succ(x \<union> y))" using IK xy 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

599 
by (auto simp add: ieq intro: InfCard_is_Limit [THEN ordermap_csquare_le]) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

600 
moreover have "succ(succ(x \<union> y)) \<otimes> succ(succ(x \<union> y)) < K" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

601 
proof (cases rule: Ord_linear2 [OF ou Ord_nat]) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

602 
assume "x \<union> y < nat" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

603 
hence "succ(succ(x \<union> y)) \<otimes> succ(succ(x \<union> y)) \<in> nat" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

604 
by (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

605 
nat_into_Card [THEN Card_cardinal_eq] Ord_nat) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

606 
also have "... \<subseteq> K" using IK 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

607 
by (simp add: InfCard_def le_imp_subset) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

608 
finally show "succ(succ(x \<union> y)) \<otimes> succ(succ(x \<union> y)) < K" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

609 
by (simp add: ltI OK) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

610 
next 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

611 
assume natxy: "nat \<le> x \<union> y" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

612 
hence seq: "succ(succ(x \<union> y)) = x \<union> y" using xy 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

613 
by (simp add: le_imp_subset nat_succ_eqpoll [THEN cardinal_cong] le_succ_iff) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

614 
also have "... < K" using xy 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

615 
by (simp add: Un_least_lt Ord_cardinal_le [THEN lt_trans1]) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

616 
finally have "succ(succ(x \<union> y)) < K" . 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

617 
moreover have "InfCard(succ(succ(x \<union> y)))" using xy natxy 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

618 
by (simp add: seq InfCard_def Card_cardinal nat_le_cardinal) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

619 
ultimately show ?thesis by (simp add: eq ltD) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

620 
qed 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

621 
ultimately show "i < K" by (blast intro: lt_trans1) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

622 
qed 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

623 
qed 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

624 
qed 
13216  625 

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

46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

627 
lemma InfCard_csquare_eq: 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

628 
assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

629 
proof  
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

630 
have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) 
46935  631 
show "InfCard(K) ==> K \<otimes> K = K" using OK 
632 
proof (induct rule: trans_induct) 

633 
case (step i) 

634 
show "i \<otimes> i = i" 

635 
proof (rule le_anti_sym) 

636 
have "i \<times> i = ordertype(i \<times> i, csquare_rel(i))" 

637 
by (rule cardinal_cong, 

638 
simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll]) 

639 
hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" 

640 
by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype]) 

641 
moreover 

642 
have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using step 

643 
by (simp add: ordertype_csquare_le) 

644 
ultimately show "i \<otimes> i \<le> i" by (rule le_trans) 

645 
next 

646 
show "i \<le> i \<otimes> i" using step 

647 
by (blast intro: cmult_square_le InfCard_is_Card) 

46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

648 
qed 
46935  649 
qed 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

650 
qed 
13216  651 

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

653 
lemma well_ord_InfCard_square_eq: 

46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

654 
assumes r: "well_ord(A,r)" and I: "InfCard(A)" shows "A \<times> A \<approx> A" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

655 
proof  
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

656 
have "A \<times> A \<approx> A \<times> A" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

657 
by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_sym r) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

658 
also have "... \<approx> A" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

659 
proof (rule well_ord_cardinal_eqE [OF _ r]) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

660 
show "well_ord(A \<times> A, rmult(A, Memrel(A), A, Memrel(A)))" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

661 
by (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel r) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

662 
next 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

663 
show "A \<times> A = A" using InfCard_csquare_eq I 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

664 
by (simp add: cmult_def) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

665 
qed 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

666 
finally show ?thesis . 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

667 
qed 
13216  668 

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

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

13356  673 
done 
674 

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

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

677 

14883  678 
subsubsection{*Toward's Kunen's Corollary 10.13 (1)*} 
13216  679 

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

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

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

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

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

686 
apply (simp add: InfCard_csquare_eq) 

687 
done 

688 

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

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

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

694 
apply (rule Un_commute [THEN ssubst]) 

46820  695 
apply (simp_all add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq 
13221  696 
subset_Un_iff2 [THEN iffD1] le_imp_subset) 
13216  697 
done 
698 

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

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

13216  702 
done 
703 

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

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

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

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

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

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

711 
apply (simp add: InfCard_cdouble_eq) 

712 
done 

713 

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

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

718 
apply (rule Un_commute [THEN ssubst]) 

13221  719 
apply (simp_all add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) 
13216  720 
done 
721 

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

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

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

725 
*) 

726 

27517  727 
subsection{*For Every Cardinal Number There Exists A Greater One*} 
13356  728 

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

13216  730 

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

732 
apply (unfold jump_cardinal_def) 

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

734 
prefer 2 apply (blast intro!: Ord_ordertype) 

735 
apply (unfold Transset_def) 

736 
apply (safe del: subsetI) 

13221  737 
apply (simp add: ordertype_pred_unfold, safe) 
13216  738 
apply (rule UN_I) 
739 
apply (rule_tac [2] ReplaceI) 

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

741 
done 

742 

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

744 
lemma jump_cardinal_iff: 

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

745 
"i \<in> jump_cardinal(K) \<longleftrightarrow> 
46820  746 
(\<exists>r X. r \<subseteq> K*K & X \<subseteq> K & well_ord(X,r) & i = ordertype(X,r))" 
13216  747 
apply (unfold jump_cardinal_def) 
46820  748 
apply (blast del: subsetI) 
13216  749 
done 
750 

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

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

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

754 
apply (rule jump_cardinal_iff [THEN iffD2]) 

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

46820  756 
apply (rule_tac x=K in exI) 
13216  757 
apply (simp add: ordertype_Memrel well_ord_Memrel) 
758 
apply (simp add: Memrel_def subset_iff) 

759 
done 

760 

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

762 
whose ordertype is jump_cardinal(K). *) 

763 
lemma Card_jump_cardinal_lemma: 

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

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

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

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

770 
apply (intro exI conjI) 

13221  771 
apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+) 
13216  772 
apply (erule bij_is_inj [THEN well_ord_rvimage]) 
773 
apply (rule Ord_jump_cardinal [THEN well_ord_Memrel]) 

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

775 
ordertype_Memrel Ord_jump_cardinal) 

776 
done 

777 

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

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

780 
apply (rule Ord_jump_cardinal [THEN CardI]) 

781 
apply (unfold eqpoll_def) 

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

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

784 
done 

785 

13356  786 
subsection{*Basic Properties of Successor Cardinals*} 
13216  787 

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

789 
apply (unfold csucc_def) 

790 
apply (rule LeastI) 

791 
apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ 

792 
done 

793 

45602  794 
lemmas Card_csucc = csucc_basic [THEN conjunct1] 
13216  795 

45602  796 
lemmas lt_csucc = csucc_basic [THEN conjunct2] 
13216  797 

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

13221  799 
by (blast intro: Ord_0_le lt_csucc lt_trans1) 
13216  800 

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

804 
apply (blast intro: Card_is_Ord)+ 

805 
done 

806 

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

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

810 
apply (erule_tac [2] lt_trans1) 

811 
apply (simp_all add: lt_csucc Card_csucc Card_is_Ord) 

812 
apply (rule notI [THEN not_lt_imp_le]) 

13221  813 
apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl], assumption) 
13216  814 
apply (rule Ord_cardinal_le [THEN lt_trans1]) 
46820  815 
apply (simp_all add: Ord_cardinal Card_is_Ord) 
13216  816 
done 
817 

818 
lemma Card_lt_csucc_iff: 

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

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

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

46820  823 
by (simp add: InfCard_def Card_csucc Card_is_Ord 
13216  824 
lt_csucc [THEN leI, THEN [2] le_trans]) 
825 

826 

14883  827 
subsubsection{*Removing elements from a finite set decreases its cardinality*} 
13216  828 

46820  829 
lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x\<notin>A \<longrightarrow> ~ cons(x,A) \<lesssim> A" 
13216  830 
apply (erule Fin_induct) 
13221  831 
apply (simp add: lepoll_0_iff) 
13216  832 
apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))") 
13221  833 
apply simp 
834 
apply (blast dest!: cons_lepoll_consD, blast) 

13216  835 
done 
836 

14883  837 
lemma Finite_imp_cardinal_cons [simp]: 
46820  838 
"[ Finite(A); a\<notin>A ] ==> cons(a,A) = succ(A)" 
13216  839 
apply (unfold cardinal_def) 
840 
apply (rule Least_equality) 

841 
apply (fold cardinal_def) 

13221  842 
apply (simp add: succ_def) 
13216  843 
apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll 
844 
elim!: mem_irrefl dest!: Finite_imp_well_ord) 

845 
apply (blast intro: Card_cardinal Card_is_Ord) 

846 
apply (rule notI) 

13221  847 
apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE], 
848 
assumption, assumption) 

13216  849 
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) 
850 
apply (erule le_imp_lepoll [THEN lepoll_trans]) 

851 
apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll] 

852 
dest!: Finite_imp_well_ord) 

853 
done 

854 

855 

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

13784  858 
apply (rule_tac b = A in cons_Diff [THEN subst], assumption) 
13221  859 
apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite]) 
860 
apply (simp add: cons_Diff) 

13216  861 
done 
862 

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

864 
apply (rule succ_leE) 

13221  865 
apply (simp add: Finite_imp_succ_cardinal_Diff) 
13216  866 
done 
867 

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

871 
done 

13216  872 

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

14883  876 
apply (simp add: Finite_Int cons_absorb Un_cons Int_cons_left) 
877 
done 

878 

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

14883  881 
by (simp add: Finite_Un card_Un_Int) 
882 

883 
lemma card_partition [rule_format]: 

46820  884 
"Finite(C) ==> 
885 
Finite (\<Union> C) \<longrightarrow> 

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

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

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

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

893 
done 

894 

895 

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

13216  897 

45602  898 
lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel] 
13216  899 

46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

900 
lemma nat_sum_eqpoll_sum: 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

901 
assumes m: "m \<in> nat" and n: "n \<in> nat" shows "m + n \<approx> m #+ n" 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

902 
proof  
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

903 
have "m + n \<approx> m+n" using m n 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

904 
by (blast intro: nat_implies_well_ord well_ord_radd well_ord_cardinal_eqpoll eqpoll_sym) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

905 
also have "... = m #+ n" using m n 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

906 
by (simp add: nat_cadd_eq_add [symmetric] cadd_def) 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

907 
finally show ?thesis . 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

908 
qed 
13216  909 

46935  910 
lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<Longrightarrow> i \<in> nat  i=nat" 
911 
proof (induct i rule: trans_induct3) 

912 
case 0 thus ?case by auto 

913 
next 

914 
case (succ i) thus ?case by auto 

915 
next 

916 
case (limit l) thus ?case 

917 
by (blast dest: nat_le_Limit le_imp_subset) 

918 
qed 

13216  919 

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

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

924 
apply (rule succ_inject) 

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

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

926 
apply (simp add: Finite_imp_succ_cardinal_Diff) 
13216  927 
apply (subgoal_tac "1 \<lesssim> A") 
13221  928 
prefer 2 apply (blast intro: not_0_is_lepoll_1) 
929 
apply (frule Finite_imp_well_ord, clarify) 

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

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

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

934 
apply (auto simp add: Finite_cardinal_in_nat) 
13216  935 
done 
936 

13221  937 
lemma cardinal_lt_imp_Diff_not_0 [rule_format]: 
46820  938 
"Finite(B) ==> \<forall>A. B<A \<longrightarrow> A  B \<noteq> 0" 
13221  939 
apply (erule Finite_induct, auto) 
940 
apply (case_tac "Finite (A)") 

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

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

943 
apply (auto simp add: Finite_0 Finite_cons) 

13216  944 
apply (subgoal_tac "B<A") 
13221  945 
prefer 2 apply (blast intro: lt_trans Ord_cardinal) 
13216  946 
apply (case_tac "x:A") 
13221  947 
apply (subgoal_tac [2] "A  cons (x, B) = A  B") 
948 
apply auto 

46820  949 
apply (subgoal_tac "A \<le> cons (x, B) ") 
13221  950 
prefer 2 
46820  951 
apply (blast dest: Finite_cons [THEN Finite_imp_well_ord] 
13216  952 
intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll) 
953 
apply (auto simp add: Finite_imp_cardinal_cons) 

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

955 
apply (blast intro: lt_trans) 

956 
done 

957 

437  958 
end 