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/Cardinal.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

435  3 
Copyright 1994 University of Cambridge 
13328  4 
*) 
13221  5 

13328  6 
header{*Cardinal Numbers Without the Axiom of Choice*} 
435  7 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset

8 
theory Cardinal imports OrderType Finite Nat_ZF Sum begin 
13221  9 

24893  10 
definition 
435  11 
(*least ordinal operator*) 
24893  12 
Least :: "(i=>o) => i" (binder "LEAST " 10) where 
46820  13 
"Least(P) == THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> ~P(j))" 
435  14 

24893  15 
definition 
16 
eqpoll :: "[i,i] => o" (infixl "eqpoll" 50) where 

46953  17 
"A eqpoll B == \<exists>f. f \<in> bij(A,B)" 
435  18 

24893  19 
definition 
20 
lepoll :: "[i,i] => o" (infixl "lepoll" 50) where 

46953  21 
"A lepoll B == \<exists>f. f \<in> inj(A,B)" 
435  22 

24893  23 
definition 
24 
lesspoll :: "[i,i] => o" (infixl "lesspoll" 50) where 

13221  25 
"A lesspoll B == A lepoll B & ~(A eqpoll B)" 
832  26 

24893  27 
definition 
28 
cardinal :: "i=>i" ("_") where 

46847  29 
"A == (LEAST i. i eqpoll A)" 
435  30 

24893  31 
definition 
32 
Finite :: "i=>o" where 

46820  33 
"Finite(A) == \<exists>n\<in>nat. A eqpoll n" 
435  34 

24893  35 
definition 
36 
Card :: "i=>o" where 

13221  37 
"Card(i) == (i = i)" 
435  38 

21524  39 
notation (xsymbols) 
40 
eqpoll (infixl "\<approx>" 50) and 

41 
lepoll (infixl "\<lesssim>" 50) and 

42 
lesspoll (infixl "\<prec>" 50) and 

43 
Least (binder "\<mu>" 10) 

13221  44 

46847  45 
notation (HTML) 
21524  46 
eqpoll (infixl "\<approx>" 50) and 
47 
Least (binder "\<mu>" 10) 

48 

14565  49 

13357  50 
subsection{*The SchroederBernstein Theorem*} 
51 
text{*See Davey and Priestly, page 106*} 

13221  52 

53 
(** Lemma: Banach's Decomposition Theorem **) 

54 

55 
lemma decomp_bnd_mono: "bnd_mono(X, %W. X  g``(Y  f``W))" 

56 
by (rule bnd_monoI, blast+) 

57 

58 
lemma Banach_last_equation: 

46953  59 
"g \<in> Y>X 
46820  60 
==> g``(Y  f`` lfp(X, %W. X  g``(Y  f``W))) = 
61 
X  lfp(X, %W. X  g``(Y  f``W))" 

62 
apply (rule_tac P = "%u. ?v = Xu" 

13221  63 
in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst]) 
64 
apply (simp add: double_complement fun_is_rel [THEN image_subset]) 

65 
done 

66 

67 
lemma decomposition: 

46953  68 
"[ f \<in> X>Y; g \<in> Y>X ] ==> 
46820  69 
\<exists>XA XB YA YB. (XA \<inter> XB = 0) & (XA \<union> XB = X) & 
70 
(YA \<inter> YB = 0) & (YA \<union> YB = Y) & 

13221  71 
f``XA=YA & g``YB=XB" 
72 
apply (intro exI conjI) 

73 
apply (rule_tac [6] Banach_last_equation) 

74 
apply (rule_tac [5] refl) 

46820  75 
apply (assumption  
13221  76 
rule Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+ 
77 
done 

78 

79 
lemma schroeder_bernstein: 

46953  80 
"[ f \<in> inj(X,Y); g \<in> inj(Y,X) ] ==> \<exists>h. h \<in> bij(X,Y)" 
46820  81 
apply (insert decomposition [of f X Y g]) 
13221  82 
apply (simp add: inj_is_fun) 
83 
apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij) 

46820  84 
(* The instantiation of exI to @{term"restrict(f,XA) \<union> converse(restrict(g,YB))"} 
13221  85 
is forced by the context!! *) 
86 
done 

87 

88 

89 
(** Equipollence is an equivalence relation **) 

90 

46953  91 
lemma bij_imp_eqpoll: "f \<in> bij(A,B) ==> A \<approx> B" 
13221  92 
apply (unfold eqpoll_def) 
93 
apply (erule exI) 

94 
done 

95 

96 
(*A eqpoll A*) 

45602  97 
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp] 
13221  98 

99 
lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X" 

100 
apply (unfold eqpoll_def) 

101 
apply (blast intro: bij_converse_bij) 

102 
done 

103 

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

104 
lemma eqpoll_trans [trans]: 
13221  105 
"[ X \<approx> Y; Y \<approx> Z ] ==> X \<approx> Z" 
106 
apply (unfold eqpoll_def) 

107 
apply (blast intro: comp_bij) 

108 
done 

109 

110 
(** Lepollence is a partial ordering **) 

111 

112 
lemma subset_imp_lepoll: "X<=Y ==> X \<lesssim> Y" 

113 
apply (unfold lepoll_def) 

114 
apply (rule exI) 

115 
apply (erule id_subset_inj) 

116 
done 

117 

45602  118 
lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp] 
13221  119 

45602  120 
lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll] 
13221  121 

122 
lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y" 

123 
by (unfold eqpoll_def bij_def lepoll_def, blast) 

124 

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

125 
lemma lepoll_trans [trans]: "[ X \<lesssim> Y; Y \<lesssim> Z ] ==> X \<lesssim> Z" 
13221  126 
apply (unfold lepoll_def) 
127 
apply (blast intro: comp_inj) 

128 
done 

129 

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

130 
lemma eq_lepoll_trans [trans]: "[ X \<approx> Y; Y \<lesssim> Z ] ==> X \<lesssim> Z" 
46953  131 
by (blast intro: eqpoll_imp_lepoll lepoll_trans) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

132 

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

133 
lemma lepoll_eq_trans [trans]: "[ X \<lesssim> Y; Y \<approx> Z ] ==> X \<lesssim> Z" 
46953  134 
by (blast intro: eqpoll_imp_lepoll lepoll_trans) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

135 

13221  136 
(*Asymmetry law*) 
137 
lemma eqpollI: "[ X \<lesssim> Y; Y \<lesssim> X ] ==> X \<approx> Y" 

138 
apply (unfold lepoll_def eqpoll_def) 

139 
apply (elim exE) 

140 
apply (rule schroeder_bernstein, assumption+) 

141 
done 

142 

143 
lemma eqpollE: 

144 
"[ X \<approx> Y; [ X \<lesssim> Y; Y \<lesssim> X ] ==> P ] ==> P" 

46820  145 
by (blast intro: eqpoll_imp_lepoll eqpoll_sym) 
13221  146 

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

147 
lemma eqpoll_iff: "X \<approx> Y \<longleftrightarrow> X \<lesssim> Y & Y \<lesssim> X" 
13221  148 
by (blast intro: eqpollI elim!: eqpollE) 
149 

150 
lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0" 

151 
apply (unfold lepoll_def inj_def) 

152 
apply (blast dest: apply_type) 

153 
done 

154 

46820  155 
(*@{term"0 \<lesssim> Y"}*) 
45602  156 
lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll] 
13221  157 

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

158 
lemma lepoll_0_iff: "A \<lesssim> 0 \<longleftrightarrow> A=0" 
13221  159 
by (blast intro: lepoll_0_is_0 lepoll_refl) 
160 

46820  161 
lemma Un_lepoll_Un: 
162 
"[ A \<lesssim> B; C \<lesssim> D; B \<inter> D = 0 ] ==> A \<union> C \<lesssim> B \<union> D" 

13221  163 
apply (unfold lepoll_def) 
164 
apply (blast intro: inj_disjoint_Un) 

165 
done 

166 

167 
(*A eqpoll 0 ==> A=0*) 

45602  168 
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0] 
13221  169 

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

170 
lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0" 
13221  171 
by (blast intro: eqpoll_0_is_0 eqpoll_refl) 
172 

46820  173 
lemma eqpoll_disjoint_Un: 
174 
"[ A \<approx> B; C \<approx> D; A \<inter> C = 0; B \<inter> D = 0 ] 

175 
==> A \<union> C \<approx> B \<union> D" 

13221  176 
apply (unfold eqpoll_def) 
177 
apply (blast intro: bij_disjoint_Un) 

178 
done 

179 

180 

13356  181 
subsection{*lesspoll: contributions by Krzysztof Grabczewski *} 
13221  182 

183 
lemma lesspoll_not_refl: "~ (i \<prec> i)" 

46820  184 
by (simp add: lesspoll_def) 
13221  185 

186 
lemma lesspoll_irrefl [elim!]: "i \<prec> i ==> P" 

46820  187 
by (simp add: lesspoll_def) 
13221  188 

189 
lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B" 

190 
by (unfold lesspoll_def, blast) 

191 

46820  192 
lemma lepoll_well_ord: "[ A \<lesssim> B; well_ord(B,r) ] ==> \<exists>s. well_ord(A,s)" 
13221  193 
apply (unfold lepoll_def) 
194 
apply (blast intro: well_ord_rvimage) 

195 
done 

196 

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

197 
lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B  A \<approx> B" 
13221  198 
apply (unfold lesspoll_def) 
199 
apply (blast intro!: eqpollI elim!: eqpollE) 

200 
done 

201 

46820  202 
lemma inj_not_surj_succ: 
47042  203 
assumes fi: "f \<in> inj(A, succ(m))" and fns: "f \<notin> surj(A, succ(m))" 
204 
shows "\<exists>f. f \<in> inj(A,m)" 

205 
proof  

206 
from fi [THEN inj_is_fun] fns 

207 
obtain y where y: "y \<in> succ(m)" "\<And>x. x\<in>A \<Longrightarrow> f ` x \<noteq> y" 

208 
by (auto simp add: surj_def) 

209 
show ?thesis 

210 
proof 

211 
show "(\<lambda>z\<in>A. if f`z = m then y else f`z) \<in> inj(A, m)" using y fi 

212 
by (simp add: inj_def) 

213 
(auto intro!: if_type [THEN lam_type] intro: Pi_type dest: apply_funtype) 

214 
qed 

215 
qed 

13221  216 

217 
(** Variations on transitivity **) 

218 

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

219 
lemma lesspoll_trans [trans]: 
13221  220 
"[ X \<prec> Y; Y \<prec> Z ] ==> X \<prec> Z" 
221 
apply (unfold lesspoll_def) 

222 
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans) 

223 
done 

224 

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

225 
lemma lesspoll_trans1 [trans]: 
13221  226 
"[ X \<lesssim> Y; Y \<prec> Z ] ==> X \<prec> Z" 
227 
apply (unfold lesspoll_def) 

228 
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans) 

229 
done 

230 

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

231 
lemma lesspoll_trans2 [trans]: 
13221  232 
"[ X \<prec> Y; Y \<lesssim> Z ] ==> X \<prec> Z" 
233 
apply (unfold lesspoll_def) 

234 
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans) 

235 
done 

236 

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

237 
lemma eq_lesspoll_trans [trans]: 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

238 
"[ X \<approx> Y; Y \<prec> Z ] ==> X \<prec> Z" 
46953  239 
by (blast intro: eqpoll_imp_lepoll lesspoll_trans1) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

240 

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

241 
lemma lesspoll_eq_trans [trans]: 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

242 
"[ X \<prec> Y; Y \<approx> Z ] ==> X \<prec> Z" 
46953  243 
by (blast intro: eqpoll_imp_lepoll lesspoll_trans2) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

244 

13221  245 

246 
(** LEAST  the least number operator [from HOL/Univ.ML] **) 

247 

46820  248 
lemma Least_equality: 
46847  249 
"[ P(i); Ord(i); !!x. x<i ==> ~P(x) ] ==> (\<mu> x. P(x)) = i" 
46820  250 
apply (unfold Least_def) 
13221  251 
apply (rule the_equality, blast) 
252 
apply (elim conjE) 

253 
apply (erule Ord_linear_lt, assumption, blast+) 

254 
done 

255 

47016  256 
lemma LeastI: 
257 
assumes P: "P(i)" and i: "Ord(i)" shows "P(\<mu> x. P(x))" 

258 
proof  

259 
{ from i have "P(i) \<Longrightarrow> P(\<mu> x. P(x))" 

260 
proof (induct i rule: trans_induct) 

261 
case (step i) 

262 
show ?case 

263 
proof (cases "P(\<mu> a. P(a))") 

264 
case True thus ?thesis . 

265 
next 

266 
case False 

267 
hence "\<And>x. x \<in> i \<Longrightarrow> ~P(x)" using step 

268 
by blast 

47018  269 
hence "(\<mu> a. P(a)) = i" using step 
270 
by (blast intro: Least_equality ltD) 

271 
thus ?thesis using step.prems 

47016  272 
by simp 
273 
qed 

274 
qed 

275 
} 

276 
thus ?thesis using P . 

277 
qed 

13221  278 

47018  279 
text{*The proof is almost identical to the one above!*} 
280 
lemma Least_le: 

281 
assumes P: "P(i)" and i: "Ord(i)" shows "(\<mu> x. P(x)) \<le> i" 

282 
proof  

283 
{ from i have "P(i) \<Longrightarrow> (\<mu> x. P(x)) \<le> i" 

284 
proof (induct i rule: trans_induct) 

285 
case (step i) 

286 
show ?case 

287 
proof (cases "(\<mu> a. P(a)) \<le> i") 

288 
case True thus ?thesis . 

289 
next 

290 
case False 

291 
hence "\<And>x. x \<in> i \<Longrightarrow> ~ (\<mu> a. P(a)) \<le> i" using step 

292 
by blast 

293 
hence "(\<mu> a. P(a)) = i" using step 

294 
by (blast elim: ltE intro: ltI Least_equality lt_trans1) 

295 
thus ?thesis using step 

296 
by simp 

297 
qed 

298 
qed 

299 
} 

300 
thus ?thesis using P . 

301 
qed 

13221  302 

303 
(*LEAST really is the smallest*) 

46847  304 
lemma less_LeastE: "[ P(i); i < (\<mu> x. P(x)) ] ==> Q" 
13221  305 
apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+) 
46820  306 
apply (simp add: lt_Ord) 
13221  307 
done 
308 

309 
(*Easier to apply than LeastI: conclusion has only one occurrence of P*) 

310 
lemma LeastI2: 

46847  311 
"[ P(i); Ord(i); !!j. P(j) ==> Q(j) ] ==> Q(\<mu> j. P(j))" 
46820  312 
by (blast intro: LeastI ) 
13221  313 

314 
(*If there is no such P then LEAST is vacuously 0*) 

46820  315 
lemma Least_0: 
46847  316 
"[ ~ (\<exists>i. Ord(i) & P(i)) ] ==> (\<mu> x. P(x)) = 0" 
13221  317 
apply (unfold Least_def) 
318 
apply (rule the_0, blast) 

319 
done 

320 

46847  321 
lemma Ord_Least [intro,simp,TC]: "Ord(\<mu> x. P(x))" 
47042  322 
proof (cases "\<exists>i. Ord(i) & P(i)") 
323 
case True 

324 
then obtain i where "P(i)" "Ord(i)" by auto 

325 
hence " (\<mu> x. P(x)) \<le> i" by (rule Least_le) 

326 
thus ?thesis 

327 
by (elim ltE) 

328 
next 

329 
case False 

330 
hence "(\<mu> x. P(x)) = 0" by (rule Least_0) 

331 
thus ?thesis 

332 
by auto 

333 
qed 

13221  334 

335 

47042  336 
subsection{*Basic Properties of Cardinals*} 
13221  337 

338 
(*Not needed for simplification, but helpful below*) 

46847  339 
lemma Least_cong: "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (\<mu> x. P(x)) = (\<mu> x. Q(x))" 
13221  340 
by simp 
341 

46820  342 
(*Need AC to get @{term"X \<lesssim> Y ==> X \<le> Y"}; see well_ord_lepoll_imp_Card_le 
13221  343 
Converse also requires AC, but see well_ord_cardinal_eqE*) 
344 
lemma cardinal_cong: "X \<approx> Y ==> X = Y" 

345 
apply (unfold eqpoll_def cardinal_def) 

346 
apply (rule Least_cong) 

347 
apply (blast intro: comp_bij bij_converse_bij) 

348 
done 

349 

350 
(*Under AC, the premise becomes trivial; one consequence is A = A*) 

46820  351 
lemma well_ord_cardinal_eqpoll: 
47018  352 
assumes r: "well_ord(A,r)" shows "A \<approx> A" 
353 
proof (unfold cardinal_def) 

354 
show "(\<mu> i. i \<approx> A) \<approx> A" 

355 
by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) 

356 
qed 

13221  357 

46820  358 
(* @{term"Ord(A) ==> A \<approx> A"} *) 
13221  359 
lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll] 
360 

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

361 
lemma Ord_cardinal_idem: "Ord(A) \<Longrightarrow> A = A" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

362 
by (rule Ord_cardinal_eqpoll [THEN cardinal_cong]) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

363 

13221  364 
lemma well_ord_cardinal_eqE: 
46953  365 
assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "X = Y" 
46847  366 
shows "X \<approx> Y" 
367 
proof  

46953  368 
have "X \<approx> X" by (blast intro: well_ord_cardinal_eqpoll [OF woX] eqpoll_sym) 
46847  369 
also have "... = Y" by (rule eq) 
46953  370 
also have "... \<approx> Y" by (rule well_ord_cardinal_eqpoll [OF woY]) 
46847  371 
finally show ?thesis . 
372 
qed 

13221  373 

374 
lemma well_ord_cardinal_eqpoll_iff: 

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

375 
"[ well_ord(X,r); well_ord(Y,s) ] ==> X = Y \<longleftrightarrow> X \<approx> Y" 
13221  376 
by (blast intro: cardinal_cong well_ord_cardinal_eqE) 
377 

378 

379 
(** Observations from Kunen, page 28 **) 

380 

46820  381 
lemma Ord_cardinal_le: "Ord(i) ==> i \<le> i" 
13221  382 
apply (unfold cardinal_def) 
383 
apply (erule eqpoll_refl [THEN Least_le]) 

384 
done 

385 

386 
lemma Card_cardinal_eq: "Card(K) ==> K = K" 

387 
apply (unfold Card_def) 

388 
apply (erule sym) 

389 
done 

390 

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

391 
(* Could replace the @{term"~(j \<approx> i)"} by @{term"~(i \<preceq> j)"}. *) 
13221  392 
lemma CardI: "[ Ord(i); !!j. j<i ==> ~(j \<approx> i) ] ==> Card(i)" 
46820  393 
apply (unfold Card_def cardinal_def) 
13221  394 
apply (subst Least_equality) 
47018  395 
apply (blast intro: eqpoll_refl)+ 
13221  396 
done 
397 

398 
lemma Card_is_Ord: "Card(i) ==> Ord(i)" 

399 
apply (unfold Card_def cardinal_def) 

400 
apply (erule ssubst) 

401 
apply (rule Ord_Least) 

402 
done 

403 

46820  404 
lemma Card_cardinal_le: "Card(K) ==> K \<le> K" 
13221  405 
apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq) 
406 
done 

407 

408 
lemma Ord_cardinal [simp,intro!]: "Ord(A)" 

409 
apply (unfold cardinal_def) 

410 
apply (rule Ord_Least) 

411 
done 

412 

47018  413 
text{*The cardinals are the initial ordinals.*} 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

414 
lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)" 
47018  415 
proof  
416 
{ fix j 

417 
assume K: "Card(K)" "j \<approx> K" 

418 
assume "j < K" 

419 
also have "... = (\<mu> i. i \<approx> K)" using K 

420 
by (simp add: Card_def cardinal_def) 

421 
finally have "j < (\<mu> i. i \<approx> K)" . 

422 
hence "False" using K 

423 
by (best dest: less_LeastE) 

424 
} 

425 
then show ?thesis 

47042  426 
by (blast intro: CardI Card_is_Ord) 
47018  427 
qed 
13221  428 

429 
lemma lt_Card_imp_lesspoll: "[ Card(a); i<a ] ==> i \<prec> a" 

430 
apply (unfold lesspoll_def) 

431 
apply (drule Card_iff_initial [THEN iffD1]) 

432 
apply (blast intro!: leI [THEN le_imp_lepoll]) 

433 
done 

434 

435 
lemma Card_0: "Card(0)" 

436 
apply (rule Ord_0 [THEN CardI]) 

437 
apply (blast elim!: ltE) 

438 
done 

439 

46820  440 
lemma Card_Un: "[ Card(K); Card(L) ] ==> Card(K \<union> L)" 
13221  441 
apply (rule Ord_linear_le [of K L]) 
442 
apply (simp_all add: subset_Un_iff [THEN iffD1] Card_is_Ord le_imp_subset 

443 
subset_Un_iff2 [THEN iffD1]) 

444 
done 

445 

446 
(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*) 

447 

47101  448 
lemma Card_cardinal [iff]: "Card(A)" 
46847  449 
proof (unfold cardinal_def) 
450 
show "Card(\<mu> i. i \<approx> A)" 

451 
proof (cases "\<exists>i. Ord (i) & i \<approx> A") 

452 
case False thus ?thesis {*degenerate case*} 

453 
by (simp add: Least_0 Card_0) 

454 
next 

455 
case True {*real case: @{term A} is isomorphic to some ordinal*} 

456 
then obtain i where i: "Ord(i)" "i \<approx> A" by blast 

46953  457 
show ?thesis 
46847  458 
proof (rule CardI [OF Ord_Least], rule notI) 
459 
fix j 

46953  460 
assume j: "j < (\<mu> i. i \<approx> A)" 
46847  461 
assume "j \<approx> (\<mu> i. i \<approx> A)" 
462 
also have "... \<approx> A" using i by (auto intro: LeastI) 

463 
finally have "j \<approx> A" . 

46953  464 
thus False 
46847  465 
by (rule less_LeastE [OF _ j]) 
466 
qed 

467 
qed 

468 
qed 

13221  469 

470 
(*Kunen's Lemma 10.5*) 

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

472 
assumes i:"i \<le> j" and j: "j \<le> i" shows "j = i" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

473 
proof (rule eqpollI [THEN cardinal_cong]) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

474 
show "j \<lesssim> i" by (rule le_imp_lepoll [OF j]) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

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

476 
have Oi: "Ord(i)" using j by (rule le_Ord2) 
46953  477 
hence "i \<approx> i" 
478 
by (blast intro: Ord_cardinal_eqpoll eqpoll_sym) 

479 
also have "... \<lesssim> j" 

480 
by (blast intro: le_imp_lepoll i) 

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

481 
finally show "i \<lesssim> j" . 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

482 
qed 
13221  483 

46953  484 
lemma cardinal_mono: 
46877  485 
assumes ij: "i \<le> j" shows "i \<le> j" 
47016  486 
using Ord_cardinal [of i] Ord_cardinal [of j] 
487 
proof (cases rule: Ord_linear_le) 

488 
case le thus ?thesis . 

46877  489 
next 
47016  490 
case ge 
46877  491 
have i: "Ord(i)" using ij 
46953  492 
by (simp add: lt_Ord) 
493 
have ci: "i \<le> j" 

494 
by (blast intro: Ord_cardinal_le ij le_trans i) 

495 
have "i = i" 

496 
by (auto simp add: Ord_cardinal_idem i) 

46877  497 
also have "... = j" 
47016  498 
by (rule cardinal_eq_lemma [OF ge ci]) 
46877  499 
finally have "i = j" . 
500 
thus ?thesis by simp 

501 
qed 

13221  502 

47016  503 
text{*Since we have @{term"succ(nat) \<le> nat"}, the converse of @{text cardinal_mono} fails!*} 
13221  504 
lemma cardinal_lt_imp_lt: "[ i < j; Ord(i); Ord(j) ] ==> i < j" 
505 
apply (rule Ord_linear2 [of i j], assumption+) 

506 
apply (erule lt_trans2 [THEN lt_irrefl]) 

507 
apply (erule cardinal_mono) 

508 
done 

509 

510 
lemma Card_lt_imp_lt: "[ i < K; Ord(i); Card(K) ] ==> i < K" 

46877  511 
by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq) 
13221  512 

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

513 
lemma Card_lt_iff: "[ Ord(i); Card(K) ] ==> (i < K) \<longleftrightarrow> (i < K)" 
13221  514 
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1]) 
515 

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

516 
lemma Card_le_iff: "[ Ord(i); Card(K) ] ==> (K \<le> i) \<longleftrightarrow> (K \<le> i)" 
13269  517 
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym]) 
13221  518 

519 
(*Can use AC or finiteness to discharge first premise*) 

520 
lemma well_ord_lepoll_imp_Card_le: 

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

521 
assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

522 
shows "A \<le> B" 
47016  523 
using Ord_cardinal [of A] Ord_cardinal [of B] 
524 
proof (cases rule: Ord_linear_le) 

525 
case le thus ?thesis . 

526 
next 

527 
case ge 

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

528 
from lepoll_well_ord [OF AB wB] 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

529 
obtain s where s: "well_ord(A, s)" by blast 
46953  530 
have "B \<approx> B" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll) 
47016  531 
also have "... \<lesssim> A" by (rule le_imp_lepoll [OF ge]) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

532 
also have "... \<approx> A" by (rule well_ord_cardinal_eqpoll [OF s]) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

533 
finally have "B \<lesssim> A" . 
46953  534 
hence "A \<approx> B" by (blast intro: eqpollI AB) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

535 
hence "A = B" by (rule cardinal_cong) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

536 
thus ?thesis by simp 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

537 
qed 
13221  538 

46820  539 
lemma lepoll_cardinal_le: "[ A \<lesssim> i; Ord(i) ] ==> A \<le> i" 
13221  540 
apply (rule le_trans) 
541 
apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption) 

542 
apply (erule Ord_cardinal_le) 

543 
done 

544 

545 
lemma lepoll_Ord_imp_eqpoll: "[ A \<lesssim> i; Ord(i) ] ==> A \<approx> A" 

546 
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord) 

547 

14046  548 
lemma lesspoll_imp_eqpoll: "[ A \<prec> i; Ord(i) ] ==> A \<approx> A" 
13221  549 
apply (unfold lesspoll_def) 
550 
apply (blast intro: lepoll_Ord_imp_eqpoll) 

551 
done 

552 

46820  553 
lemma cardinal_subset_Ord: "[A<=i; Ord(i)] ==> A \<subseteq> i" 
14046  554 
apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le]) 
555 
apply (auto simp add: lt_def) 

556 
apply (blast intro: Ord_trans) 

557 
done 

13221  558 

13356  559 
subsection{*The finite cardinals *} 
13221  560 

46820  561 
lemma cons_lepoll_consD: 
562 
"[ cons(u,A) \<lesssim> cons(v,B); u\<notin>A; v\<notin>B ] ==> A \<lesssim> B" 

13221  563 
apply (unfold lepoll_def inj_def, safe) 
46820  564 
apply (rule_tac x = "\<lambda>x\<in>A. if f`x=v then f`u else f`x" in exI) 
13221  565 
apply (rule CollectI) 
566 
(*Proving it's in the function space A>B*) 

567 
apply (rule if_type [THEN lam_type]) 

568 
apply (blast dest: apply_funtype) 

569 
apply (blast elim!: mem_irrefl dest: apply_funtype) 

570 
(*Proving it's injective*) 

571 
apply (simp (no_asm_simp)) 

572 
apply blast 

573 
done 

574 

46820  575 
lemma cons_eqpoll_consD: "[ cons(u,A) \<approx> cons(v,B); u\<notin>A; v\<notin>B ] ==> A \<approx> B" 
13221  576 
apply (simp add: eqpoll_iff) 
577 
apply (blast intro: cons_lepoll_consD) 

578 
done 

579 

580 
(*Lemma suggested by Mike Fourman*) 

581 
lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) ==> m \<lesssim> n" 

582 
apply (unfold succ_def) 

583 
apply (erule cons_lepoll_consD) 

584 
apply (rule mem_not_refl)+ 

585 
done 

586 

46877  587 

46935  588 
lemma nat_lepoll_imp_le: 
589 
"m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n" 

590 
proof (induct m arbitrary: n rule: nat_induct) 

591 
case 0 thus ?case by (blast intro!: nat_0_le) 

592 
next 

593 
case (succ m) 

594 
show ?case using `n \<in> nat` 

595 
proof (cases rule: natE) 

596 
case 0 thus ?thesis using succ 

597 
by (simp add: lepoll_def inj_def) 

598 
next 

599 
case (succ n') thus ?thesis using succ.hyps ` succ(m) \<lesssim> n` 

600 
by (blast intro!: succ_leI dest!: succ_lepoll_succD) 

601 
qed 

602 
qed 

13221  603 

46953  604 
lemma nat_eqpoll_iff: "[ m \<in> nat; n \<in> nat ] ==> m \<approx> n \<longleftrightarrow> m = n" 
13221  605 
apply (rule iffI) 
606 
apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE) 

607 
apply (simp add: eqpoll_refl) 

608 
done 

609 

610 
(*The object of all this work: every natural number is a (finite) cardinal*) 

46820  611 
lemma nat_into_Card: 
47042  612 
assumes n: "n \<in> nat" shows "Card(n)" 
613 
proof (unfold Card_def cardinal_def, rule sym) 

614 
have "Ord(n)" using n by auto 

615 
moreover 

616 
{ fix i 

617 
assume "i < n" "i \<approx> n" 

618 
hence False using n 

619 
by (auto simp add: lt_nat_in_nat [THEN nat_eqpoll_iff]) 

620 
} 

621 
ultimately show "(\<mu> i. i \<approx> n) = n" by (auto intro!: Least_equality) 

622 
qed 

13221  623 

624 
lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] 

625 
lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] 

626 

627 

628 
(*Part of Kunen's Lemma 10.6*) 

46877  629 
lemma succ_lepoll_natE: "[ succ(n) \<lesssim> n; n \<in> nat ] ==> P" 
13221  630 
by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto) 
631 

46820  632 
lemma nat_lepoll_imp_ex_eqpoll_n: 
13221  633 
"[ n \<in> nat; nat \<lesssim> X ] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y" 
634 
apply (unfold lepoll_def eqpoll_def) 

635 
apply (fast del: subsetI subsetCE 

636 
intro!: subset_SIs 

637 
dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj] 

46820  638 
elim!: restrict_bij 
13221  639 
inj_is_fun [THEN fun_is_rel, THEN image_subset]) 
640 
done 

641 

642 

643 
(** lepoll, \<prec> and natural numbers **) 

644 

46877  645 
lemma lepoll_succ: "i \<lesssim> succ(i)" 
646 
by (blast intro: subset_imp_lepoll) 

647 

46820  648 
lemma lepoll_imp_lesspoll_succ: 
46877  649 
assumes A: "A \<lesssim> m" and m: "m \<in> nat" 
650 
shows "A \<prec> succ(m)" 

651 
proof  

46953  652 
{ assume "A \<approx> succ(m)" 
46877  653 
hence "succ(m) \<approx> A" by (rule eqpoll_sym) 
654 
also have "... \<lesssim> m" by (rule A) 

655 
finally have "succ(m) \<lesssim> m" . 

656 
hence False by (rule succ_lepoll_natE) (rule m) } 

657 
moreover have "A \<lesssim> succ(m)" by (blast intro: lepoll_trans A lepoll_succ) 

46953  658 
ultimately show ?thesis by (auto simp add: lesspoll_def) 
46877  659 
qed 
660 

661 
lemma lesspoll_succ_imp_lepoll: 

662 
"[ A \<prec> succ(m); m \<in> nat ] ==> A \<lesssim> m" 

663 
apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def) 

664 
apply (auto dest: inj_not_surj_succ) 

13221  665 
done 
666 

46877  667 
lemma lesspoll_succ_iff: "m \<in> nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m" 
13221  668 
by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll) 
669 

46877  670 
lemma lepoll_succ_disj: "[ A \<lesssim> succ(m); m \<in> nat ] ==> A \<lesssim> m  A \<approx> succ(m)" 
13221  671 
apply (rule disjCI) 
672 
apply (rule lesspoll_succ_imp_lepoll) 

673 
prefer 2 apply assumption 

674 
apply (simp (no_asm_simp) add: lesspoll_def) 

675 
done 

676 

677 
lemma lesspoll_cardinal_lt: "[ A \<prec> i; Ord(i) ] ==> A < i" 

678 
apply (unfold lesspoll_def, clarify) 

679 
apply (frule lepoll_cardinal_le, assumption) 

680 
apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym] 

681 
dest: lepoll_well_ord elim!: leE) 

682 
done 

683 

684 

13356  685 
subsection{*The first infinite cardinal: Omega, or nat *} 
13221  686 

687 
(*This implies Kunen's Lemma 10.6*) 

46877  688 
lemma lt_not_lepoll: 
689 
assumes n: "n<i" "n \<in> nat" shows "~ i \<lesssim> n" 

690 
proof  

691 
{ assume i: "i \<lesssim> n" 

692 
have "succ(n) \<lesssim> i" using n 

46953  693 
by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll]) 
46877  694 
also have "... \<lesssim> n" by (rule i) 
695 
finally have "succ(n) \<lesssim> n" . 

696 
hence False by (rule succ_lepoll_natE) (rule n) } 

697 
thus ?thesis by auto 

698 
qed 

13221  699 

46877  700 
text{*A slightly weaker version of @{text nat_eqpoll_iff}*} 
701 
lemma Ord_nat_eqpoll_iff: 

702 
assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n" 

47016  703 
using i nat_into_Ord [OF n] 
704 
proof (cases rule: Ord_linear_lt) 

705 
case lt 

46877  706 
hence "i \<in> nat" by (rule lt_nat_in_nat) (rule n) 
46953  707 
thus ?thesis by (simp add: nat_eqpoll_iff n) 
46877  708 
next 
47016  709 
case eq 
46953  710 
thus ?thesis by (simp add: eqpoll_refl) 
46877  711 
next 
47016  712 
case gt 
46953  713 
hence "~ i \<lesssim> n" using n by (rule lt_not_lepoll) 
46877  714 
hence "~ i \<approx> n" using n by (blast intro: eqpoll_imp_lepoll) 
715 
moreover have "i \<noteq> n" using `n<i` by auto 

716 
ultimately show ?thesis by blast 

717 
qed 

13221  718 

719 
lemma Card_nat: "Card(nat)" 

46877  720 
proof  
721 
{ fix i 

46953  722 
assume i: "i < nat" "i \<approx> nat" 
723 
hence "~ nat \<lesssim> i" 

724 
by (simp add: lt_def lt_not_lepoll) 

725 
hence False using i 

46877  726 
by (simp add: eqpoll_iff) 
727 
} 

46953  728 
hence "(\<mu> i. i \<approx> nat) = nat" by (blast intro: Least_equality eqpoll_refl) 
46877  729 
thus ?thesis 
46953  730 
by (auto simp add: Card_def cardinal_def) 
46877  731 
qed 
13221  732 

733 
(*Allows showing that i is a limit cardinal*) 

46820  734 
lemma nat_le_cardinal: "nat \<le> i ==> nat \<le> i" 
13221  735 
apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst]) 
736 
apply (erule cardinal_mono) 

737 
done 

738 

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

739 
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

740 
by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

741 

13221  742 

13356  743 
subsection{*Towards Cardinal Arithmetic *} 
13221  744 
(** Congruence laws for successor, cardinal addition and multiplication **) 
745 

746 
(*Congruence law for cons under equipollence*) 

46820  747 
lemma cons_lepoll_cong: 
748 
"[ A \<lesssim> B; b \<notin> B ] ==> cons(a,A) \<lesssim> cons(b,B)" 

13221  749 
apply (unfold lepoll_def, safe) 
46820  750 
apply (rule_tac x = "\<lambda>y\<in>cons (a,A) . if y=a then b else f`y" in exI) 
46953  751 
apply (rule_tac d = "%z. if z \<in> B then converse (f) `z else a" in lam_injective) 
46820  752 
apply (safe elim!: consE') 
13221  753 
apply simp_all 
46820  754 
apply (blast intro: inj_is_fun [THEN apply_type])+ 
13221  755 
done 
756 

757 
lemma cons_eqpoll_cong: 

46820  758 
"[ A \<approx> B; a \<notin> A; b \<notin> B ] ==> cons(a,A) \<approx> cons(b,B)" 
13221  759 
by (simp add: eqpoll_iff cons_lepoll_cong) 
760 

761 
lemma cons_lepoll_cons_iff: 

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

762 
"[ a \<notin> A; b \<notin> B ] ==> cons(a,A) \<lesssim> cons(b,B) \<longleftrightarrow> A \<lesssim> B" 
13221  763 
by (blast intro: cons_lepoll_cong cons_lepoll_consD) 
764 

765 
lemma cons_eqpoll_cons_iff: 

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

766 
"[ a \<notin> A; b \<notin> B ] ==> cons(a,A) \<approx> cons(b,B) \<longleftrightarrow> A \<approx> B" 
13221  767 
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD) 
768 

769 
lemma singleton_eqpoll_1: "{a} \<approx> 1" 

770 
apply (unfold succ_def) 

771 
apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong]) 

772 
done 

773 

774 
lemma cardinal_singleton: "{a} = 1" 

775 
apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans]) 

776 
apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq]) 

777 
done 

778 

46820  779 
lemma not_0_is_lepoll_1: "A \<noteq> 0 ==> 1 \<lesssim> A" 
13221  780 
apply (erule not_emptyE) 
781 
apply (rule_tac a = "cons (x, A{x}) " in subst) 

782 
apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \<lesssim> cons (x, A{x})" in subst) 

783 
prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto) 

784 
done 

785 

786 
(*Congruence law for succ under equipollence*) 

787 
lemma succ_eqpoll_cong: "A \<approx> B ==> succ(A) \<approx> succ(B)" 

788 
apply (unfold succ_def) 

789 
apply (simp add: cons_eqpoll_cong mem_not_refl) 

790 
done 

791 

792 
(*Congruence law for + under equipollence*) 

793 
lemma sum_eqpoll_cong: "[ A \<approx> C; B \<approx> D ] ==> A+B \<approx> C+D" 

794 
apply (unfold eqpoll_def) 

795 
apply (blast intro!: sum_bij) 

796 
done 

797 

798 
(*Congruence law for * under equipollence*) 

46820  799 
lemma prod_eqpoll_cong: 
13221  800 
"[ A \<approx> C; B \<approx> D ] ==> A*B \<approx> C*D" 
801 
apply (unfold eqpoll_def) 

802 
apply (blast intro!: prod_bij) 

803 
done 

804 

46820  805 
lemma inj_disjoint_eqpoll: 
46953  806 
"[ f \<in> inj(A,B); A \<inter> B = 0 ] ==> A \<union> (B  range(f)) \<approx> B" 
13221  807 
apply (unfold eqpoll_def) 
808 
apply (rule exI) 

46953  809 
apply (rule_tac c = "%x. if x \<in> A then f`x else x" 
810 
and d = "%y. if y \<in> range (f) then converse (f) `y else y" 

13221  811 
in lam_bijective) 
812 
apply (blast intro!: if_type inj_is_fun [THEN apply_type]) 

813 
apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype]) 

46820  814 
apply (safe elim!: UnE') 
13221  815 
apply (simp_all add: inj_is_fun [THEN apply_rangeI]) 
46820  816 
apply (blast intro: inj_converse_fun [THEN apply_type])+ 
13221  817 
done 
818 

819 

13356  820 
subsection{*Lemmas by Krzysztof Grabczewski*} 
821 

822 
(*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*) 

13221  823 

46953  824 
text{*If @{term A} has at most @{term"n+1"} elements and @{term"a \<in> A"} 
46877  825 
then @{term"A{a}"} has at most @{term n}.*} 
46820  826 
lemma Diff_sing_lepoll: 
46877  827 
"[ a \<in> A; A \<lesssim> succ(n) ] ==> A  {a} \<lesssim> n" 
13221  828 
apply (unfold succ_def) 
829 
apply (rule cons_lepoll_consD) 

830 
apply (rule_tac [3] mem_not_refl) 

831 
apply (erule cons_Diff [THEN ssubst], safe) 

832 
done 

833 

46877  834 
text{*If @{term A} has at least @{term"n+1"} elements then @{term"A{a}"} has at least @{term n}.*} 
46820  835 
lemma lepoll_Diff_sing: 
46877  836 
assumes A: "succ(n) \<lesssim> A" shows "n \<lesssim> A  {a}" 
837 
proof  

838 
have "cons(n,n) \<lesssim> A" using A 

839 
by (unfold succ_def) 

46953  840 
also have "... \<lesssim> cons(a, A{a})" 
46877  841 
by (blast intro: subset_imp_lepoll) 
842 
finally have "cons(n,n) \<lesssim> cons(a, A{a})" . 

843 
thus ?thesis 

46953  844 
by (blast intro: cons_lepoll_consD mem_irrefl) 
46877  845 
qed 
13221  846 

46877  847 
lemma Diff_sing_eqpoll: "[ a \<in> A; A \<approx> succ(n) ] ==> A  {a} \<approx> n" 
46820  848 
by (blast intro!: eqpollI 
849 
elim!: eqpollE 

13221  850 
intro: Diff_sing_lepoll lepoll_Diff_sing) 
851 

46877  852 
lemma lepoll_1_is_sing: "[ A \<lesssim> 1; a \<in> A ] ==> A = {a}" 
13221  853 
apply (frule Diff_sing_lepoll, assumption) 
854 
apply (drule lepoll_0_is_0) 

855 
apply (blast elim: equalityE) 

856 
done 

857 

46820  858 
lemma Un_lepoll_sum: "A \<union> B \<lesssim> A+B" 
13221  859 
apply (unfold lepoll_def) 
46877  860 
apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x\<in>A then Inl (x) else Inr (x)" in exI) 
861 
apply (rule_tac d = "%z. snd (z)" in lam_injective) 

46820  862 
apply force 
13221  863 
apply (simp add: Inl_def Inr_def) 
864 
done 

865 

866 
lemma well_ord_Un: 

46820  867 
"[ well_ord(X,R); well_ord(Y,S) ] ==> \<exists>T. well_ord(X \<union> Y, T)" 
868 
by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]], 

13221  869 
assumption) 
870 

871 
(*Krzysztof Grabczewski*) 

46820  872 
lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 ==> A \<union> B \<approx> A + B" 
13221  873 
apply (unfold eqpoll_def) 
46877  874 
apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a \<in> A then Inl (a) else Inr (a)" in exI) 
875 
apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective) 

13221  876 
apply auto 
877 
done 

878 

879 

13244  880 
subsection {*Finite and infinite sets*} 
13221  881 

47018  882 
lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)" 
883 
apply (unfold Finite_def) 

884 
apply (blast intro: eqpoll_trans eqpoll_sym) 

885 
done 

886 

13244  887 
lemma Finite_0 [simp]: "Finite(0)" 
13221  888 
apply (unfold Finite_def) 
889 
apply (blast intro!: eqpoll_refl nat_0I) 

890 
done 

891 

47018  892 
lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))" 
13221  893 
apply (unfold Finite_def) 
47018  894 
apply (case_tac "y \<in> x") 
895 
apply (simp add: cons_absorb) 

896 
apply (erule bexE) 

897 
apply (rule bexI) 

898 
apply (erule_tac [2] nat_succI) 

899 
apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl) 

900 
done 

901 

902 
lemma Finite_succ: "Finite(x) ==> Finite(succ(x))" 

903 
apply (unfold succ_def) 

904 
apply (erule Finite_cons) 

13221  905 
done 
906 

47018  907 
lemma lepoll_nat_imp_Finite: 
908 
assumes A: "A \<lesssim> n" and n: "n \<in> nat" shows "Finite(A)" 

909 
proof  

910 
have "A \<lesssim> n \<Longrightarrow> Finite(A)" using n 

911 
proof (induct n) 

912 
case 0 

913 
hence "A = 0" by (rule lepoll_0_is_0) 

914 
thus ?case by simp 

915 
next 

916 
case (succ n) 

917 
hence "A \<lesssim> n \<or> A \<approx> succ(n)" by (blast dest: lepoll_succ_disj) 

918 
thus ?case using succ by (auto simp add: Finite_def) 

919 
qed 

920 
thus ?thesis using A . 

921 
qed 

922 

46820  923 
lemma lesspoll_nat_is_Finite: 
13221  924 
"A \<prec> nat ==> Finite(A)" 
925 
apply (unfold Finite_def) 

46820  926 
apply (blast dest: ltD lesspoll_cardinal_lt 
13221  927 
lesspoll_imp_eqpoll [THEN eqpoll_sym]) 
928 
done 

929 

46820  930 
lemma lepoll_Finite: 
46877  931 
assumes Y: "Y \<lesssim> X" and X: "Finite(X)" shows "Finite(Y)" 
932 
proof  

46953  933 
obtain n where n: "n \<in> nat" "X \<approx> n" using X 
934 
by (auto simp add: Finite_def) 

46877  935 
have "Y \<lesssim> X" by (rule Y) 
936 
also have "... \<approx> n" by (rule n) 

937 
finally have "Y \<lesssim> n" . 

938 
thus ?thesis using n by (simp add: lepoll_nat_imp_Finite) 

939 
qed 

13221  940 

45602  941 
lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite] 
13221  942 

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

943 
lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) \<longleftrightarrow> Finite(x)" 
13244  944 
by (blast intro: Finite_cons subset_Finite) 
945 

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

946 
lemma Finite_succ_iff [iff]: "Finite(succ(x)) \<longleftrightarrow> Finite(x)" 
13244  947 
by (simp add: succ_def) 
948 

47018  949 
lemma Finite_Int: "Finite(A)  Finite(B) ==> Finite(A \<inter> B)" 
950 
by (blast intro: subset_Finite) 

951 

952 
lemmas Finite_Diff = Diff_subset [THEN subset_Finite] 

953 

46820  954 
lemma nat_le_infinite_Ord: 
955 
"[ Ord(i); ~ Finite(i) ] ==> nat \<le> i" 

13221  956 
apply (unfold Finite_def) 
957 
apply (erule Ord_nat [THEN [2] Ord_linear2]) 

958 
prefer 2 apply assumption 

959 
apply (blast intro!: eqpoll_refl elim!: ltE) 

960 
done 

961 

46820  962 
lemma Finite_imp_well_ord: 
963 
"Finite(A) ==> \<exists>r. well_ord(A,r)" 

13221  964 
apply (unfold Finite_def eqpoll_def) 
965 
apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord) 

966 
done 

967 

13244  968 
lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0" 
969 
by (fast dest!: lepoll_0_is_0) 

970 

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

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

973 

974 
lemma Finite_Fin_lemma [rule_format]: 

46820  975 
"n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) \<longrightarrow> A \<in> Fin(X)" 
13244  976 
apply (induct_tac n) 
977 
apply (rule allI) 

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

979 
apply (rule allI) 

980 
apply (rule impI) 

981 
apply (erule conjE) 

982 
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption) 

983 
apply (frule Diff_sing_eqpoll, assumption) 

984 
apply (erule allE) 

985 
apply (erule impE, fast) 

986 
apply (drule subsetD, assumption) 

987 
apply (drule Fin.consI, assumption) 

988 
apply (simp add: cons_Diff) 

989 
done 

990 

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

46820  992 
by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
13244  993 

46953  994 
lemma Fin_lemma [rule_format]: "n \<in> nat ==> \<forall>A. A \<approx> n \<longrightarrow> A \<in> Fin(A)" 
13244  995 
apply (induct_tac n) 
996 
apply (simp add: eqpoll_0_iff, clarify) 

46953  997 
apply (subgoal_tac "\<exists>u. u \<in> A") 
13244  998 
apply (erule exE) 
46471  999 
apply (rule Diff_sing_eqpoll [elim_format]) 
13244  1000 
prefer 2 apply assumption 
1001 
apply assumption 

13784  1002 
apply (rule_tac b = A in cons_Diff [THEN subst], assumption) 
13244  1003 
apply (rule Fin.consI, blast) 
1004 
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD]) 

1005 
(*Now for the lemma assumed above*) 

1006 
apply (unfold eqpoll_def) 

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

1008 
done 

1009 

46820  1010 
lemma Finite_into_Fin: "Finite(A) ==> A \<in> Fin(A)" 
13244  1011 
apply (unfold Finite_def) 
1012 
apply (blast intro: Fin_lemma) 

1013 
done 

1014 

46820  1015 
lemma Fin_into_Finite: "A \<in> Fin(U) ==> Finite(A)" 
13244  1016 
by (fast intro!: Finite_0 Finite_cons elim: Fin_induct) 
1017 

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

1018 
lemma Finite_Fin_iff: "Finite(A) \<longleftrightarrow> A \<in> Fin(A)" 
13244  1019 
by (blast intro: Finite_into_Fin Fin_into_Finite) 
1020 

46820  1021 
lemma Finite_Un: "[ Finite(A); Finite(B) ] ==> Finite(A \<union> B)" 
1022 
by (blast intro!: Fin_into_Finite Fin_UnI 

13244  1023 
dest!: Finite_into_Fin 
46820  1024 
intro: Un_upper1 [THEN Fin_mono, THEN subsetD] 
13244  1025 
Un_upper2 [THEN Fin_mono, THEN subsetD]) 
1026 

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

1027 
lemma Finite_Un_iff [simp]: "Finite(A \<union> B) \<longleftrightarrow> (Finite(A) & Finite(B))" 
46820  1028 
by (blast intro: subset_Finite Finite_Un) 
14883  1029 

1030 
text{*The converse must hold too.*} 

46820  1031 
lemma Finite_Union: "[ \<forall>y\<in>X. Finite(y); Finite(X) ] ==> Finite(\<Union>(X))" 
13244  1032 
apply (simp add: Finite_Fin_iff) 
1033 
apply (rule Fin_UnionI) 

1034 
apply (erule Fin_induct, simp) 

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

1036 
done 

1037 

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

13524  1039 
lemma Finite_induct [case_names 0 cons, induct set: Finite]: 
13244  1040 
"[ Finite(A); P(0); 
46820  1041 
!! x B. [ Finite(B); x \<notin> B; P(B) ] ==> P(cons(x, B)) ] 
13244  1042 
==> P(A)" 
46820  1043 
apply (erule Finite_into_Fin [THEN Fin_induct]) 
13244  1044 
apply (blast intro: Fin_into_Finite)+ 
1045 
done 

1046 

1047 
(*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A{a}) *) 

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

1049 
apply (unfold Finite_def) 

46877  1050 
apply (case_tac "a \<in> A") 
13244  1051 
apply (subgoal_tac [2] "A{a}=A", auto) 
1052 
apply (rule_tac x = "succ (n) " in bexI) 

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

13784  1054 
apply (drule_tac a = a and b = n in cons_eqpoll_cong) 
13244  1055 
apply (auto dest: mem_irrefl) 
1056 
done 

1057 

1058 
(*Sidi Ehmety. And the contrapositive of this says 

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

46820  1060 
lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(AB) \<longrightarrow> Finite(A)" 
13244  1061 
apply (erule Finite_induct, auto) 
46953  1062 
apply (case_tac "x \<in> A") 
13244  1063 
apply (subgoal_tac [2] "Acons (x, B) = A  B") 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset

1064 
apply (subgoal_tac "A  cons (x, B) = (A  B)  {x}", simp) 
13244  1065 
apply (drule Diff_sing_Finite, auto) 
1066 
done 

1067 

1068 
lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))" 

1069 
by (erule Finite_induct, simp_all) 

1070 

1071 
lemma Finite_RepFun_iff_lemma [rule_format]: 

46820  1072 
"[Finite(x); !!x y. f(x)=f(y) ==> x=y] 
1073 
==> \<forall>A. x = RepFun(A,f) \<longrightarrow> Finite(A)" 

13244  1074 
apply (erule Finite_induct) 
46820  1075 
apply clarify 
13244  1076 
apply (case_tac "A=0", simp) 
46820  1077 
apply (blast del: allE, clarify) 
1078 
apply (subgoal_tac "\<exists>z\<in>A. x = f(z)") 

1079 
prefer 2 apply (blast del: allE elim: equalityE, clarify) 

13244  1080 
apply (subgoal_tac "B = {f(u) . u \<in> A  {z}}") 
46820  1081 
apply (blast intro: Diff_sing_Finite) 
1082 
apply (thin_tac "\<forall>A. ?P(A) \<longrightarrow> Finite(A)") 

1083 
apply (rule equalityI) 

1084 
apply (blast intro: elim: equalityE) 

1085 
apply (blast intro: elim: equalityCE) 

13244  1086 
done 
1087 

1088 
text{*I don't know why, but if the premise is expressed using metaconnectives 

1089 
then the simplifier cannot prove it automatically in conditional rewriting.*} 

1090 
lemma Finite_RepFun_iff: 

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

1091 
"(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) \<longleftrightarrow> Finite(A)" 
46820  1092 
by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f]) 
13244  1093 

1094 
lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))" 

46820  1095 
apply (erule Finite_induct) 
1096 
apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) 

13244  1097 
done 
1098 

1099 
lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)" 

1100 
apply (subgoal_tac "Finite({{x} . x \<in> A})") 

46820  1101 
apply (simp add: Finite_RepFun_iff ) 
1102 
apply (blast intro: subset_Finite) 

13244  1103 
done 
1104 

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

1105 
lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \<longleftrightarrow> Finite(A)" 
13244  1106 
by (blast intro: Finite_Pow Finite_Pow_imp_Finite) 
1107 

47101  1108 
lemma Finite_cardinal_iff: 
1109 
assumes i: "Ord(i)" shows "Finite(i) \<longleftrightarrow> Finite(i)" 

1110 
by (auto simp add: Finite_def) (blast intro: eqpoll_trans eqpoll_sym Ord_cardinal_eqpoll [OF i])+ 

13244  1111 

13221  1112 

1113 
(*Krzysztof Grabczewski's proof that the converse of a finite, wellordered 

1114 
set is wellordered. Proofs simplified by lcp. *) 

1115 

46877  1116 
lemma nat_wf_on_converse_Memrel: "n \<in> nat ==> wf[n](converse(Memrel(n)))" 
47018  1117 
proof (induct n rule: nat_induct) 
1118 
case 0 thus ?case by (blast intro: wf_onI) 

1119 
next 

1120 
case (succ x) 

1121 
hence wfx: "\<And>Z. Z = 0 \<or> (\<exists>z\<in>Z. \<forall>y. z \<in> y \<and> z \<in> x \<and> y \<in> x \<and> z \<in> x \<longrightarrow> y \<notin> Z)" 

1122 
by (simp add: wf_on_def wf_def) {*not easy to erase the duplicate @{term"z \<in> x"}!*} 

1123 
show ?case 

1124 
proof (rule wf_onI) 

1125 
fix Z u 

1126 
assume Z: "u \<in> Z" "\<forall>z\<in>Z. \<exists>y\<in>Z. \<langle>y, z\<rangle> \<in> converse(Memrel(succ(x)))" 

1127 
show False 

1128 
proof (cases "x \<in> Z") 

1129 
case True thus False using Z 

1130 
by (blast elim: mem_irrefl mem_asym) 

1131 
next 

1132 
case False thus False using wfx [of Z] Z 

1133 
by blast 

1134 
qed 

1135 
qed 

1136 
qed 

13221  1137 

46877  1138 
lemma nat_well_ord_converse_Memrel: "n \<in> nat ==> well_ord(n,converse(Memrel(n)))" 
13221  1139 
apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel]) 
47018  1140 
apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel) 
13221  1141 
done 
1142 

1143 
lemma well_ord_converse: 

46820  1144 
"[well_ord(A,r); 
13221  1145 
well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) ] 
1146 
==> well_ord(A,converse(r))" 

1147 
apply (rule well_ord_Int_iff [THEN iffD1]) 

1148 
apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption) 

1149 
apply (simp add: rvimage_converse converse_Int converse_prod 

1150 
ordertype_ord_iso [THEN ord_iso_rvimage_eq]) 

1151 
done 

1152 

1153 
lemma ordertype_eq_n: 

46953  1154 
assumes r: "well_ord(A,r)" and A: "A \<approx> n" and n: "n \<in> nat" 
46877  1155 
shows "ordertype(A,r) = n" 
1156 
proof  

46953  1157 
have "ordertype(A,r) \<approx> A" 
1158 
by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r) 

46877  1159 
also have "... \<approx> n" by (rule A) 
1160 
finally have "ordertype(A,r) \<approx> n" . 

1161 
thus ?thesis 

46953  1162 
by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r) 
46877  1163 
qed 
13221  1164 

46820  1165 
lemma Finite_well_ord_converse: 
13221  1166 
"[ Finite(A); well_ord(A,r) ] ==> well_ord(A,converse(r))" 
1167 
apply (unfold Finite_def) 

1168 
apply (rule well_ord_converse, assumption) 

1169 
apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel) 

1170 
done 

1171 

46877  1172 
lemma nat_into_Finite: "n \<in> nat ==> Finite(n)" 
47018  1173 
by (auto simp add: Finite_def intro: eqpoll_refl) 
13221  1174 

46877  1175 
lemma nat_not_Finite: "~ Finite(nat)" 
1176 
proof  

1177 
{ fix n 

1178 
assume n: "n \<in> nat" "nat \<approx> n" 

46953  1179 
have "n \<in> nat" by (rule n) 
46877  1180 
also have "... = n" using n 
46953  1181 
by (simp add: Ord_nat_eqpoll_iff Ord_nat) 
46877  1182 
finally have "n \<in> n" . 
46953  1183 
hence False 
1184 
by (blast elim: mem_irrefl) 

46877  1185 
} 
1186 
thus ?thesis 

46953  1187 
by (auto simp add: Finite_def) 
46877  1188 
qed 
14076  1189 

435  1190 
end 