author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 47101  ded5cc757bc9 
child 58871  c399ae4b836f 
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) == 
46953  34 
\<Union>X\<in>Pow(K). {z. r \<in> 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 

46953  51 
lemma Card_Union [simp,intro,TC]: 
46841
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) 
46953  54 
show "Ord(\<Union>A)" using A 
46841
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 
46953  63 
hence jls: "j \<prec> c" 
64 
by (simp add: lt_Card_imp_lesspoll) 

46841
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" . 

46953  71 
hence False 
46841
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 

46953  76 
lemma Card_UN: "(!!x. x \<in> 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]: 

46953  80 
"(!!x. x \<in> 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)" 
46953  102 
by (auto intro: lam_bijective [where d = "case(Inr,Inl)"]) 
46841
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" 

46953  124 
by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 
46901  125 
also have "... \<approx> i + (j + k)" 
46953  126 
by (rule sum_assoc_eqpoll) 
46901  127 
also have "... \<approx> i + j + k" 
46953  128 
by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd j k eqpoll_sym) 
46901  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)" 
46953  151 
by (simp add: inj_def) 
46841
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: 
46952  157 
assumes K: "Card(K)" and L: "Ord(L)" shows "K \<le> (K \<oplus> L)" 
158 
proof (unfold cadd_def) 

159 
have "K \<le> K" 

46953  160 
by (rule Card_cardinal_le [OF K]) 
46952  161 
moreover have "K \<le> K + L" using K L 
162 
by (blast intro: well_ord_lepoll_imp_Card_le sum_lepoll_self 

46953  163 
well_ord_radd well_ord_Memrel Card_is_Ord) 
164 
ultimately show "K \<le> K + L" 

165 
by (blast intro: le_trans) 

46952  166 
qed 
13216  167 

14883  168 
subsubsection{*Monotonicity of addition*} 
13216  169 

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

180 
lemma cadd_le_mono: 

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

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

184 
apply (rule well_ord_lepoll_imp_Card_le) 

185 
apply (blast intro: well_ord_radd well_ord_Memrel) 

186 
apply (blast intro: sum_lepoll_mono subset_imp_lepoll) 

187 
done 

188 

14883  189 
subsubsection{*Addition of finite cardinals is "ordinary" addition*} 
13216  190 

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

192 
apply (unfold eqpoll_def) 

193 
apply (rule exI) 

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

199 

46953  200 
(*Pulling the succ(...) outside the ... requires m, n \<in> nat *) 
13216  201 
(*Unconditional version requires AC*) 
202 
lemma cadd_succ_lemma: 

46952  203 
assumes "Ord(m)" "Ord(n)" shows "succ(m) \<oplus> n = succ(m \<oplus> n)" 
204 
proof (unfold cadd_def) 

205 
have [intro]: "m + n \<approx> m + n" using assms 

206 
by (blast intro: eqpoll_sym well_ord_cardinal_eqpoll well_ord_radd well_ord_Memrel) 

13216  207 

46952  208 
have "succ(m) + n = succ(m + n)" 
46953  209 
by (rule sum_succ_eqpoll [THEN cardinal_cong]) 
210 
also have "... = succ(m + n)" 

46952  211 
by (blast intro: succ_eqpoll_cong cardinal_cong) 
212 
finally show "succ(m) + n = succ(m + n)" . 

213 
qed 

214 

215 
lemma nat_cadd_eq_add: 

46953  216 
assumes m: "m \<in> nat" and [simp]: "n \<in> nat" shows"m \<oplus> n = m #+ n" 
46952  217 
using m 
218 
proof (induct m) 

219 
case 0 thus ?case by (simp add: nat_into_Card cadd_0) 

220 
next 

221 
case (succ m) thus ?case by (simp add: cadd_succ_lemma nat_into_Card Card_cardinal_eq) 

222 
qed 

13216  223 

224 

13356  225 
subsection{*Cardinal multiplication*} 
13216  226 

14883  227 
subsubsection{*Cardinal multiplication is commutative*} 
13216  228 

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

230 
apply (unfold eqpoll_def) 

231 
apply (rule exI) 

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

13216  234 
done 
235 

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

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

239 
done 

240 

14883  241 
subsubsection{*Cardinal multiplication is associative*} 
13216  242 

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

244 
apply (unfold eqpoll_def) 

245 
apply (rule exI) 

246 
apply (rule prod_assoc_bij) 

247 
done 

248 

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

253 
proof (unfold cmult_def, rule cardinal_cong) 

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

46953  255 
by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult i j) 
46901  256 
also have "... \<approx> i * (j * k)" 
46953  257 
by (rule prod_assoc_eqpoll) 
46901  258 
also have "... \<approx> i * j * k" 
46953  259 
by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult j k eqpoll_sym) 
46901  260 
finally show "i * j * k \<approx> i * j * k" . 
261 
qed 

13216  262 

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

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

266 
apply (unfold eqpoll_def) 

267 
apply (rule exI) 

268 
apply (rule sum_prod_distrib_bij) 

269 
done 

270 

271 
lemma well_ord_cadd_cmult_distrib: 

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

274 
proof (unfold cadd_def cmult_def, rule cardinal_cong) 

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

46953  276 
by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 
46901  277 
also have "... \<approx> i * k + j * k" 
46953  278 
by (rule sum_prod_distrib_eqpoll) 
46901  279 
also have "... \<approx> i * k + j * k" 
46953  280 
by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll well_ord_rmult i j k eqpoll_sym) 
46901  281 
finally show "i + j * k \<approx> i * k + j * k" . 
282 
qed 

13216  283 

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

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

287 
apply (unfold eqpoll_def) 

288 
apply (rule exI) 

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

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

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

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

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

298 
apply (unfold eqpoll_def) 

299 
apply (rule exI) 

300 
apply (rule singleton_prod_bij [THEN bij_converse_bij]) 

301 
done 

302 

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

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

306 
done 

307 

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

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

311 
apply (unfold lepoll_def inj_def) 

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

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

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

319 
apply (rule_tac [2] well_ord_lepoll_imp_Card_le) 

320 
apply (rule_tac [3] prod_square_lepoll) 

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

13216  323 
done 
324 

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

46953  327 
lemma prod_lepoll_self: "b \<in> B ==> A \<lesssim> A*B" 
13216  328 
apply (unfold lepoll_def inj_def) 
46820  329 
apply (rule_tac x = "\<lambda>x\<in>A. <x,b>" in exI, simp) 
13216  330 
done 
331 

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

333 
lemma cmult_le_self: 

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

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

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

340 
done 

341 

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

344 
lemma prod_lepoll_mono: 

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

346 
apply (unfold lepoll_def) 

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

354 
lemma cmult_le_mono: 

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

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

358 
apply (rule well_ord_lepoll_imp_Card_le) 

359 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

360 
apply (blast intro: prod_lepoll_mono subset_imp_lepoll) 

361 
done 

362 

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

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

366 
apply (unfold eqpoll_def) 

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

370 
apply safe 

371 
apply (simp_all add: succI2 if_type mem_imp_not_eq) 

372 
done 

373 

374 
(*Unconditional version requires AC*) 

375 
lemma cmult_succ_lemma: 

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

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

379 
apply (rule cardinal_cong [symmetric]) 

380 
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) 

381 
apply (blast intro: well_ord_rmult well_ord_Memrel) 

382 
done 

383 

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

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

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

46953  392 
lemma sum_lepoll_prod: 
46901  393 
assumes C: "2 \<lesssim> C" shows "B+B \<lesssim> C*B" 
394 
proof  

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

46953  396 
by (simp add: sum_eq_2_times) 
46901  397 
also have "... \<lesssim> C*B" 
46953  398 
by (blast intro: prod_lepoll_mono lepoll_refl C) 
46901  399 
finally show "B+B \<lesssim> C*B" . 
400 
qed 

13216  401 

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

13221  403 
by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl) 
13216  404 

405 

13356  406 
subsection{*Infinite Cardinals are Limit Ordinals*} 
13216  407 

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

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

13216  412 
lemma nat_cons_lepoll: "nat \<lesssim> A ==> cons(u,A) \<lesssim> A" 
413 
apply (unfold lepoll_def) 

414 
apply (erule exE) 

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

417 
if z=u then f`0 

46953  418 
else if z \<in> range (f) then f`succ (converse (f) `z) else z" 
13216  419 
in exI) 
420 
apply (rule_tac d = 

46953  421 
"%y. if y \<in> range(f) then nat_case (u, %z. f`z, converse(f) `y) 
46820  422 
else y" 
13216  423 
in lam_injective) 
424 
apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun) 

425 
apply (simp add: inj_is_fun [THEN apply_rangeI] 

426 
inj_converse_fun [THEN apply_rangeI] 

427 
inj_converse_fun [THEN apply_funtype]) 

428 
done 

429 

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

431 
apply (erule nat_cons_lepoll [THEN eqpollI]) 

432 
apply (rule subset_consI [THEN subset_imp_lepoll]) 

433 
done 

434 

435 
(*Specialized version required below*) 

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

439 
done 

440 

441 
lemma InfCard_nat: "InfCard(nat)" 

442 
apply (unfold InfCard_def) 

443 
apply (blast intro: Card_nat le_refl Card_is_Ord) 

444 
done 

445 

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

447 
apply (unfold InfCard_def) 

448 
apply (erule conjunct1) 

449 
done 

450 

451 
lemma InfCard_Un: 

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

455 
done 

456 

457 
(*Kunen's Lemma 10.11*) 

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

459 
apply (unfold InfCard_def) 

460 
apply (erule conjE) 

461 
apply (frule Card_is_Ord) 

462 
apply (rule ltI [THEN non_succ_LimitI]) 

463 
apply (erule le_imp_subset [THEN subsetD]) 

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

465 
apply (unfold Card_def) 

466 
apply (drule trans) 

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

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

13221  469 
apply (rule le_eqI, assumption) 
13216  470 
apply (rule Ord_cardinal) 
471 
done 

472 

473 

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

475 

476 
(*A general fact about ordermap*) 

477 
lemma ordermap_eqpoll_pred: 

46953  478 
"[ well_ord(A,r); x \<in> A ] ==> ordermap(A,r)`x \<approx> Order.pred(A,x,r)" 
13216  479 
apply (unfold eqpoll_def) 
480 
apply (rule exI) 

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

486 

14883  487 
subsubsection{*Establishing the wellordering*} 
13216  488 

46953  489 
lemma well_ord_csquare: 
46901  490 
assumes K: "Ord(K)" shows "well_ord(K*K, csquare_rel(K))" 
491 
proof (unfold csquare_rel_def, rule well_ord_rvimage) 

492 
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 

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

494 
next 

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

496 
using K by (blast intro: well_ord_rmult well_ord_Memrel) 

497 
qed 

13216  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) 
46901  514 
apply (safe del: SigmaI dest!: csquareD) 
46820  515 
apply (unfold lt_def, auto) 
13216  516 
done 
517 

518 
lemma csquare_ltI: 

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

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

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

528 
lemma csquare_or_eqI: 

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

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

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

542 
lemma ordermap_z_lt: 

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

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

547 
prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ 

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

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

552 
done 

553 

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

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

46953  560 
show "well_ord(succ(z) \<times> succ(z), 
46901  561 
rmult(succ(z), Memrel(succ(z)), succ(z), Memrel(succ(z))))" 
46953  562 
by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult) 
46901  563 
next 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

564 
have zK: "z<K" using x y K z_def 
46901  565 
by (blast intro: Un_least_lt Limit_has_succ) 
46953  566 
hence oz: "Ord(z)" by (elim ltE) 
46901  567 
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

568 
using z_def 
46953  569 
by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y) 
46901  570 
also have "... \<approx> Order.pred(K \<times> K, \<langle>z,z\<rangle>, csquare_rel(K))" 
571 
proof (rule ordermap_eqpoll_pred) 

46953  572 
show "well_ord(K \<times> K, csquare_rel(K))" using K 
46901  573 
by (rule Limit_is_Ord [THEN well_ord_csquare]) 
574 
next 

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

576 
by (blast intro: ltD) 

577 
qed 

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

579 
by (rule pred_csquare_subset [THEN subset_imp_lepoll]) 

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

46953  581 
by (blast intro: prod_eqpoll_cong Ord_succ Ord_cardinal_eqpoll eqpoll_sym) 
46901  582 
finally show "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> succ(z) \<times> succ(z)" . 
583 
qed 

13216  584 

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

587 
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

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

589 
proof  
46953  590 
have CK: "Card(K)" using IK by (rule InfCard_is_Card) 
591 
hence OK: "Ord(K)" by (rule Card_is_Ord) 

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

592 
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

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

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

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

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

597 
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

598 
hence Oi: "Ord(i)" by (elim ltE) 
46953  599 
obtain x y where x: "x \<in> K" and y: "y \<in> K" 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

600 
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

601 
using i by (auto simp add: ordertype_unfold elim: ltE) 
46953  602 
hence xy: "Ord(x)" "Ord(y)" "x < K" "y < K" using OK 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

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

604 
hence ou: "Ord(x \<union> y)" 
46953  605 
by (simp add: Ord_Un) 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

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

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

608 
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

609 
by (auto simp add: ieq intro: InfCard_is_Limit [THEN ordermap_csquare_le]) 
46953  610 
moreover have "succ(succ(x \<union> y)) \<otimes> succ(succ(x \<union> y)) < K" 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

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

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

613 
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

614 
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

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

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

617 
by (simp add: InfCard_def le_imp_subset) 
46953  618 
finally show "succ(succ(x \<union> y)) \<otimes> succ(succ(x \<union> y)) < K" 
619 
by (simp add: ltI OK) 

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

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

621 
assume natxy: "nat \<le> x \<union> y" 
46953  622 
hence seq: "succ(succ(x \<union> y)) = x \<union> y" using xy 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

623 
by (simp add: le_imp_subset nat_succ_eqpoll [THEN cardinal_cong] le_succ_iff) 
46953  624 
also have "... < K" using xy 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

625 
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

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

627 
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

628 
by (simp add: seq InfCard_def Card_cardinal nat_le_cardinal) 
46953  629 
ultimately show ?thesis by (simp add: eq ltD) 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

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

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

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

634 
qed 
13216  635 

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

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

638 
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

639 
proof  
46953  640 
have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) 
46935  641 
show "InfCard(K) ==> K \<otimes> K = K" using OK 
642 
proof (induct rule: trans_induct) 

643 
case (step i) 

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

645 
proof (rule le_anti_sym) 

46953  646 
have "i \<times> i = ordertype(i \<times> i, csquare_rel(i))" 
647 
by (rule cardinal_cong, 

46935  648 
simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll]) 
46953  649 
hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" 
46935  650 
by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype]) 
651 
moreover 

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

46953  653 
by (simp add: ordertype_csquare_le) 
46935  654 
ultimately show "i \<otimes> i \<le> i" by (rule le_trans) 
655 
next 

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

46953  657 
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

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

660 
qed 
13216  661 

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

663 
lemma well_ord_InfCard_square_eq: 

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

664 
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

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

666 
have "A \<times> A \<approx> A \<times> A" 
46953  667 
by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_sym r) 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

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

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

670 
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

671 
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

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

673 
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

674 
by (simp add: cmult_def) 
46953  675 
qed 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

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

677 
qed 
13216  678 

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

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

13356  683 
done 
684 

47101  685 
lemma Inf_Card_is_InfCard: "[ Card(i); ~ Finite(i) ] ==> InfCard(i)" 
13356  686 
by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord]) 
687 

14883  688 
subsubsection{*Toward's Kunen's Corollary 10.13 (1)*} 
13216  689 

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

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

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

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

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

696 
apply (simp add: InfCard_csquare_eq) 

697 
done 

698 

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

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

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

704 
apply (rule Un_commute [THEN ssubst]) 

46820  705 
apply (simp_all add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq 
13221  706 
subset_Un_iff2 [THEN iffD1] le_imp_subset) 
13216  707 
done 
708 

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

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

13216  712 
done 
713 

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

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

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

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

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

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

721 
apply (simp add: InfCard_cdouble_eq) 

722 
done 

723 

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

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

728 
apply (rule Un_commute [THEN ssubst]) 

13221  729 
apply (simp_all add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) 
13216  730 
done 
731 

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

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

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

735 
*) 

736 

27517  737 
subsection{*For Every Cardinal Number There Exists A Greater One*} 
13356  738 

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

13216  740 

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

742 
apply (unfold jump_cardinal_def) 

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

744 
prefer 2 apply (blast intro!: Ord_ordertype) 

745 
apply (unfold Transset_def) 

746 
apply (safe del: subsetI) 

13221  747 
apply (simp add: ordertype_pred_unfold, safe) 
13216  748 
apply (rule UN_I) 
749 
apply (rule_tac [2] ReplaceI) 

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

751 
done 

752 

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

754 
lemma jump_cardinal_iff: 

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

755 
"i \<in> jump_cardinal(K) \<longleftrightarrow> 
46820  756 
(\<exists>r X. r \<subseteq> K*K & X \<subseteq> K & well_ord(X,r) & i = ordertype(X,r))" 
13216  757 
apply (unfold jump_cardinal_def) 
46820  758 
apply (blast del: subsetI) 
13216  759 
done 
760 

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

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

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

764 
apply (rule jump_cardinal_iff [THEN iffD2]) 

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

46820  766 
apply (rule_tac x=K in exI) 
13216  767 
apply (simp add: ordertype_Memrel well_ord_Memrel) 
768 
apply (simp add: Memrel_def subset_iff) 

769 
done 

770 

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

772 
whose ordertype is jump_cardinal(K). *) 

773 
lemma Card_jump_cardinal_lemma: 

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

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

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

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

780 
apply (intro exI conjI) 

13221  781 
apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+) 
13216  782 
apply (erule bij_is_inj [THEN well_ord_rvimage]) 
783 
apply (rule Ord_jump_cardinal [THEN well_ord_Memrel]) 

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

785 
ordertype_Memrel Ord_jump_cardinal) 

786 
done 

787 

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

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

790 
apply (rule Ord_jump_cardinal [THEN CardI]) 

791 
apply (unfold eqpoll_def) 

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

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

794 
done 

795 

13356  796 
subsection{*Basic Properties of Successor Cardinals*} 
13216  797 

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

799 
apply (unfold csucc_def) 

800 
apply (rule LeastI) 

801 
apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ 

802 
done 

803 

45602  804 
lemmas Card_csucc = csucc_basic [THEN conjunct1] 
13216  805 

45602  806 
lemmas lt_csucc = csucc_basic [THEN conjunct2] 
13216  807 

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

13221  809 
by (blast intro: Ord_0_le lt_csucc lt_trans1) 
13216  810 

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

814 
apply (blast intro: Card_is_Ord)+ 

815 
done 

816 

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

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

820 
apply (erule_tac [2] lt_trans1) 

821 
apply (simp_all add: lt_csucc Card_csucc Card_is_Ord) 

822 
apply (rule notI [THEN not_lt_imp_le]) 

13221  823 
apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl], assumption) 
13216  824 
apply (rule Ord_cardinal_le [THEN lt_trans1]) 
46820  825 
apply (simp_all add: Ord_cardinal Card_is_Ord) 
13216  826 
done 
827 

828 
lemma Card_lt_csucc_iff: 

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

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

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

46820  833 
by (simp add: InfCard_def Card_csucc Card_is_Ord 
13216  834 
lt_csucc [THEN leI, THEN [2] le_trans]) 
835 

836 

14883  837 
subsubsection{*Removing elements from a finite set decreases its cardinality*} 
13216  838 

14883  839 
lemma Finite_imp_cardinal_cons [simp]: 
46952  840 
assumes FA: "Finite(A)" and a: "a\<notin>A" shows "cons(a,A) = succ(A)" 
841 
proof  

842 
{ fix X 

843 
have "Finite(X) ==> a \<notin> X \<Longrightarrow> cons(a,X) \<lesssim> X \<Longrightarrow> False" 

844 
proof (induct X rule: Finite_induct) 

46953  845 
case 0 thus False by (simp add: lepoll_0_iff) 
46952  846 
next 
46953  847 
case (cons x Y) 
848 
hence "cons(x, cons(a, Y)) \<lesssim> cons(x, Y)" by (simp add: cons_commute) 

46952  849 
hence "cons(a, Y) \<lesssim> Y" using cons by (blast dest: cons_lepoll_consD) 
850 
thus False using cons by auto 

851 
qed 

46953  852 
} 
46952  853 
hence [simp]: "~ cons(a,A) \<lesssim> A" using a FA by auto 
854 
have [simp]: "A \<approx> A" using Finite_imp_well_ord [OF FA] 

855 
by (blast intro: well_ord_cardinal_eqpoll) 

46953  856 
have "(\<mu> i. i \<approx> cons(a, A)) = succ(A)" 
46952  857 
proof (rule Least_equality [OF _ _ notI]) 
46953  858 
show "succ(A) \<approx> cons(a, A)" 
859 
by (simp add: succ_def cons_eqpoll_cong mem_not_refl a) 

46952  860 
next 
861 
show "Ord(succ(A))" by simp 

862 
next 

863 
fix i 

864 
assume i: "i \<le> A" "i \<approx> cons(a, A)" 

865 
have "cons(a, A) \<approx> i" by (rule eqpoll_sym) (rule i) 

866 
also have "... \<lesssim> A" by (rule le_imp_lepoll) (rule i) 

867 
also have "... \<approx> A" by simp 

868 
finally have "cons(a, A) \<lesssim> A" . 

869 
thus False by simp 

870 
qed 

46953  871 
thus ?thesis by (simp add: cardinal_def) 
46952  872 
qed 
13216  873 

13221  874 
lemma Finite_imp_succ_cardinal_Diff: 
46953  875 
"[ Finite(A); a \<in> A ] ==> succ(A{a}) = A" 
13784  876 
apply (rule_tac b = A in cons_Diff [THEN subst], assumption) 
13221  877 
apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite]) 
878 
apply (simp add: cons_Diff) 

13216  879 
done 
880 

46953  881 
lemma Finite_imp_cardinal_Diff: "[ Finite(A); a \<in> A ] ==> A{a} < A" 
13216  882 
apply (rule succ_leE) 
13221  883 
apply (simp add: Finite_imp_succ_cardinal_Diff) 
13216  884 
done 
885 

46820  886 
lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> A \<in> nat" 
46952  887 
proof (induct rule: Finite_induct) 
888 
case 0 thus ?case by (simp add: cardinal_0) 

889 
next 

890 
case (cons x A) thus ?case by (simp add: Finite_imp_cardinal_cons) 

891 
qed 

13216  892 

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

14883  896 
apply (simp add: Finite_Int cons_absorb Un_cons Int_cons_left) 
897 
done 

898 

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

14883  901 
by (simp add: Finite_Un card_Un_Int) 
902 

46952  903 
lemma card_partition: 
904 
assumes FC: "Finite(C)" 

905 
shows 

906 
"Finite (\<Union> C) \<Longrightarrow> 

907 
(\<forall>c\<in>C. c = k) \<Longrightarrow> 

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

14883  909 
k #* C = \<Union> C" 
46952  910 
using FC 
911 
proof (induct rule: Finite_induct) 

912 
case 0 thus ?case by simp 

913 
next 

914 
case (cons x B) 

915 
hence "x \<inter> \<Union>B = 0" by auto 

916 
thus ?case using cons 

917 
by (auto simp add: card_Un_disjoint) 

918 
qed 

14883  919 

920 

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

13216  922 

45602  923 
lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel] 
13216  924 

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

926 
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

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

928 
have "m + n \<approx> m+n" using m n 
46953  929 
by (blast intro: nat_implies_well_ord well_ord_radd well_ord_cardinal_eqpoll eqpoll_sym) 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46901
diff
changeset

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

931 
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

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

933 
qed 
13216  934 

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

937 
case 0 thus ?case by auto 

938 
next 

939 
case (succ i) thus ?case by auto 

940 
next 

941 
case (limit l) thus ?case 

942 
by (blast dest: nat_le_Limit le_imp_subset) 

943 
qed 

13216  944 

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

437  948 
end 