198 apply (unfold lesspoll_def) |
198 apply (unfold lesspoll_def) |
199 apply (blast intro!: eqpollI elim!: eqpollE) |
199 apply (blast intro!: eqpollI elim!: eqpollE) |
200 done |
200 done |
201 |
201 |
202 lemma inj_not_surj_succ: |
202 lemma inj_not_surj_succ: |
203 "[| f \<in> inj(A, succ(m)); f \<notin> surj(A, succ(m)) |] ==> \<exists>f. f \<in> inj(A,m)" |
203 assumes fi: "f \<in> inj(A, succ(m))" and fns: "f \<notin> surj(A, succ(m))" |
204 apply (unfold inj_def surj_def) |
204 shows "\<exists>f. f \<in> inj(A,m)" |
205 apply (safe del: succE) |
205 proof - |
206 apply (erule swap, rule exI) |
206 from fi [THEN inj_is_fun] fns |
207 apply (rule_tac a = "\<lambda>z\<in>A. if f`z=m then y else f`z" in CollectI) |
207 obtain y where y: "y \<in> succ(m)" "\<And>x. x\<in>A \<Longrightarrow> f ` x \<noteq> y" |
208 txt{*the typing condition*} |
208 by (auto simp add: surj_def) |
209 apply (best intro!: if_type [THEN lam_type] elim: apply_funtype [THEN succE]) |
209 show ?thesis |
210 txt{*Proving it's injective*} |
210 proof |
211 apply simp |
211 show "(\<lambda>z\<in>A. if f`z = m then y else f`z) \<in> inj(A, m)" using y fi |
212 apply blast |
212 by (simp add: inj_def) |
213 done |
213 (auto intro!: if_type [THEN lam_type] intro: Pi_type dest: apply_funtype) |
|
214 qed |
|
215 qed |
214 |
216 |
215 (** Variations on transitivity **) |
217 (** Variations on transitivity **) |
216 |
218 |
217 lemma lesspoll_trans [trans]: |
219 lemma lesspoll_trans [trans]: |
218 "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z" |
220 "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z" |
315 apply (unfold Least_def) |
317 apply (unfold Least_def) |
316 apply (rule the_0, blast) |
318 apply (rule the_0, blast) |
317 done |
319 done |
318 |
320 |
319 lemma Ord_Least [intro,simp,TC]: "Ord(\<mu> x. P(x))" |
321 lemma Ord_Least [intro,simp,TC]: "Ord(\<mu> x. P(x))" |
320 apply (case_tac "\<exists>i. Ord(i) & P(i)") |
322 proof (cases "\<exists>i. Ord(i) & P(i)") |
321 apply safe |
323 case True |
322 apply (rule Least_le [THEN ltE]) |
324 then obtain i where "P(i)" "Ord(i)" by auto |
323 prefer 3 apply assumption+ |
325 hence " (\<mu> x. P(x)) \<le> i" by (rule Least_le) |
324 apply (erule Least_0 [THEN ssubst]) |
326 thus ?thesis |
325 apply (rule Ord_0) |
327 by (elim ltE) |
326 done |
328 next |
327 |
329 case False |
328 |
330 hence "(\<mu> x. P(x)) = 0" by (rule Least_0) |
329 (** Basic properties of cardinals **) |
331 thus ?thesis |
|
332 by auto |
|
333 qed |
|
334 |
|
335 |
|
336 subsection{*Basic Properties of Cardinals*} |
330 |
337 |
331 (*Not needed for simplification, but helpful below*) |
338 (*Not needed for simplification, but helpful below*) |
332 lemma Least_cong: "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (\<mu> x. P(x)) = (\<mu> x. Q(x))" |
339 lemma Least_cong: "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (\<mu> x. P(x)) = (\<mu> x. Q(x))" |
333 by simp |
340 by simp |
334 |
341 |
414 finally have "j < (\<mu> i. i \<approx> K)" . |
421 finally have "j < (\<mu> i. i \<approx> K)" . |
415 hence "False" using K |
422 hence "False" using K |
416 by (best dest: less_LeastE) |
423 by (best dest: less_LeastE) |
417 } |
424 } |
418 then show ?thesis |
425 then show ?thesis |
419 by (blast intro: CardI Card_is_Ord elim:) |
426 by (blast intro: CardI Card_is_Ord) |
420 qed |
427 qed |
421 |
428 |
422 lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a" |
429 lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a" |
423 apply (unfold lesspoll_def) |
430 apply (unfold lesspoll_def) |
424 apply (drule Card_iff_initial [THEN iffD1]) |
431 apply (drule Card_iff_initial [THEN iffD1]) |
600 apply (simp add: eqpoll_refl) |
607 apply (simp add: eqpoll_refl) |
601 done |
608 done |
602 |
609 |
603 (*The object of all this work: every natural number is a (finite) cardinal*) |
610 (*The object of all this work: every natural number is a (finite) cardinal*) |
604 lemma nat_into_Card: |
611 lemma nat_into_Card: |
605 "n \<in> nat ==> Card(n)" |
612 assumes n: "n \<in> nat" shows "Card(n)" |
606 apply (unfold Card_def cardinal_def) |
613 proof (unfold Card_def cardinal_def, rule sym) |
607 apply (subst Least_equality) |
614 have "Ord(n)" using n by auto |
608 apply (rule eqpoll_refl) |
615 moreover |
609 apply (erule nat_into_Ord) |
616 { fix i |
610 apply (simp (no_asm_simp) add: lt_nat_in_nat [THEN nat_eqpoll_iff]) |
617 assume "i < n" "i \<approx> n" |
611 apply (blast elim!: lt_irrefl)+ |
618 hence False using n |
612 done |
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 |
613 |
623 |
614 lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] |
624 lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] |
615 lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] |
625 lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] |
616 |
626 |
617 |
627 |