438 also have "... \<lesssim> j" |
438 also have "... \<lesssim> j" |
439 by (blast intro: le_imp_lepoll i) |
439 by (blast intro: le_imp_lepoll i) |
440 finally show "i \<lesssim> j" . |
440 finally show "i \<lesssim> j" . |
441 qed |
441 qed |
442 |
442 |
443 lemma cardinal_mono: "i \<le> j ==> |i| \<le> |j|" |
443 lemma cardinal_mono: |
444 apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le) |
444 assumes ij: "i \<le> j" shows "|i| \<le> |j|" |
445 apply (safe intro!: Ord_cardinal le_eqI) |
445 proof (cases rule: Ord_linear_le [OF Ord_cardinal Ord_cardinal]) |
446 apply (rule cardinal_eq_lemma) |
446 assume "|i| \<le> |j|" thus ?thesis . |
447 prefer 2 apply assumption |
447 next |
448 apply (erule le_trans) |
448 assume cj: "|j| \<le> |i|" |
449 apply (erule ltE) |
449 have i: "Ord(i)" using ij |
450 apply (erule Ord_cardinal_le) |
450 by (simp add: lt_Ord) |
451 done |
451 have ci: "|i| \<le> j" |
|
452 by (blast intro: Ord_cardinal_le ij le_trans i) |
|
453 have "|i| = ||i||" |
|
454 by (auto simp add: Ord_cardinal_idem i) |
|
455 also have "... = |j|" |
|
456 by (rule cardinal_eq_lemma [OF cj ci]) |
|
457 finally have "|i| = |j|" . |
|
458 thus ?thesis by simp |
|
459 qed |
452 |
460 |
453 (*Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of cardinal_mono fails!*) |
461 (*Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of cardinal_mono fails!*) |
454 lemma cardinal_lt_imp_lt: "[| |i| < |j|; Ord(i); Ord(j) |] ==> i < j" |
462 lemma cardinal_lt_imp_lt: "[| |i| < |j|; Ord(i); Ord(j) |] ==> i < j" |
455 apply (rule Ord_linear2 [of i j], assumption+) |
463 apply (rule Ord_linear2 [of i j], assumption+) |
456 apply (erule lt_trans2 [THEN lt_irrefl]) |
464 apply (erule lt_trans2 [THEN lt_irrefl]) |
457 apply (erule cardinal_mono) |
465 apply (erule cardinal_mono) |
458 done |
466 done |
459 |
467 |
460 lemma Card_lt_imp_lt: "[| |i| < K; Ord(i); Card(K) |] ==> i < K" |
468 lemma Card_lt_imp_lt: "[| |i| < K; Ord(i); Card(K) |] ==> i < K" |
461 apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq) |
469 by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq) |
462 done |
|
463 |
470 |
464 lemma Card_lt_iff: "[| Ord(i); Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)" |
471 lemma Card_lt_iff: "[| Ord(i); Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)" |
465 by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1]) |
472 by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1]) |
466 |
473 |
467 lemma Card_le_iff: "[| Ord(i); Card(K) |] ==> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)" |
474 lemma Card_le_iff: "[| Ord(i); Card(K) |] ==> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)" |
530 apply (unfold succ_def) |
537 apply (unfold succ_def) |
531 apply (erule cons_lepoll_consD) |
538 apply (erule cons_lepoll_consD) |
532 apply (rule mem_not_refl)+ |
539 apply (rule mem_not_refl)+ |
533 done |
540 done |
534 |
541 |
|
542 |
535 lemma nat_lepoll_imp_le [rule_format]: |
543 lemma nat_lepoll_imp_le [rule_format]: |
536 "m:nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n" |
544 "m \<in> nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n" |
537 apply (induct_tac m) |
545 apply (induct_tac m) |
538 apply (blast intro!: nat_0_le) |
546 apply (blast intro!: nat_0_le) |
539 apply (rule ballI) |
547 apply (rule ballI) |
540 apply (erule_tac n = n in natE) |
548 apply (erule_tac n = n in natE) |
541 apply (simp (no_asm_simp) add: lepoll_def inj_def) |
549 apply (simp (no_asm_simp) add: lepoll_def inj_def) |
542 apply (blast intro!: succ_leI dest!: succ_lepoll_succD) |
550 apply (blast intro!: succ_leI dest!: succ_lepoll_succD) |
543 done |
551 done |
544 |
552 |
545 lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n" |
553 lemma nat_eqpoll_iff: "[| m \<in> nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n" |
546 apply (rule iffI) |
554 apply (rule iffI) |
547 apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE) |
555 apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE) |
548 apply (simp add: eqpoll_refl) |
556 apply (simp add: eqpoll_refl) |
549 done |
557 done |
550 |
558 |
562 lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] |
570 lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] |
563 lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] |
571 lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] |
564 |
572 |
565 |
573 |
566 (*Part of Kunen's Lemma 10.6*) |
574 (*Part of Kunen's Lemma 10.6*) |
567 lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n; n:nat |] ==> P" |
575 lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n; n \<in> nat |] ==> P" |
568 by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto) |
576 by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto) |
569 |
577 |
570 lemma nat_lepoll_imp_ex_eqpoll_n: |
578 lemma nat_lepoll_imp_ex_eqpoll_n: |
571 "[| n \<in> nat; nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y" |
579 "[| n \<in> nat; nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y" |
572 apply (unfold lepoll_def eqpoll_def) |
580 apply (unfold lepoll_def eqpoll_def) |
578 done |
586 done |
579 |
587 |
580 |
588 |
581 (** lepoll, \<prec> and natural numbers **) |
589 (** lepoll, \<prec> and natural numbers **) |
582 |
590 |
|
591 lemma lepoll_succ: "i \<lesssim> succ(i)" |
|
592 by (blast intro: subset_imp_lepoll) |
|
593 |
583 lemma lepoll_imp_lesspoll_succ: |
594 lemma lepoll_imp_lesspoll_succ: |
584 "[| A \<lesssim> m; m:nat |] ==> A \<prec> succ(m)" |
595 assumes A: "A \<lesssim> m" and m: "m \<in> nat" |
585 apply (unfold lesspoll_def) |
596 shows "A \<prec> succ(m)" |
586 apply (rule conjI) |
597 proof - |
587 apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans]) |
598 { assume "A \<approx> succ(m)" |
588 apply (rule notI) |
599 hence "succ(m) \<approx> A" by (rule eqpoll_sym) |
589 apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) |
600 also have "... \<lesssim> m" by (rule A) |
590 apply (drule lepoll_trans, assumption) |
601 finally have "succ(m) \<lesssim> m" . |
591 apply (erule succ_lepoll_natE, assumption) |
602 hence False by (rule succ_lepoll_natE) (rule m) } |
592 done |
603 moreover have "A \<lesssim> succ(m)" by (blast intro: lepoll_trans A lepoll_succ) |
|
604 ultimately show ?thesis by (auto simp add: lesspoll_def) |
|
605 qed |
593 |
606 |
594 lemma lesspoll_succ_imp_lepoll: |
607 lemma lesspoll_succ_imp_lepoll: |
595 "[| A \<prec> succ(m); m:nat |] ==> A \<lesssim> m" |
608 "[| A \<prec> succ(m); m \<in> nat |] ==> A \<lesssim> m" |
596 apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def, clarify) |
609 apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def) |
597 apply (blast intro!: inj_not_surj_succ) |
610 apply (auto dest: inj_not_surj_succ) |
598 done |
611 done |
599 |
612 |
600 lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m" |
613 lemma lesspoll_succ_iff: "m \<in> nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m" |
601 by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll) |
614 by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll) |
602 |
615 |
603 lemma lepoll_succ_disj: "[| A \<lesssim> succ(m); m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)" |
616 lemma lepoll_succ_disj: "[| A \<lesssim> succ(m); m \<in> nat |] ==> A \<lesssim> m | A \<approx> succ(m)" |
604 apply (rule disjCI) |
617 apply (rule disjCI) |
605 apply (rule lesspoll_succ_imp_lepoll) |
618 apply (rule lesspoll_succ_imp_lepoll) |
606 prefer 2 apply assumption |
619 prefer 2 apply assumption |
607 apply (simp (no_asm_simp) add: lesspoll_def) |
620 apply (simp (no_asm_simp) add: lesspoll_def) |
608 done |
621 done |
616 |
629 |
617 |
630 |
618 subsection{*The first infinite cardinal: Omega, or nat *} |
631 subsection{*The first infinite cardinal: Omega, or nat *} |
619 |
632 |
620 (*This implies Kunen's Lemma 10.6*) |
633 (*This implies Kunen's Lemma 10.6*) |
621 lemma lt_not_lepoll: "[| n<i; n:nat |] ==> ~ i \<lesssim> n" |
634 lemma lt_not_lepoll: |
622 apply (rule notI) |
635 assumes n: "n<i" "n \<in> nat" shows "~ i \<lesssim> n" |
623 apply (rule succ_lepoll_natE [of n]) |
636 proof - |
624 apply (rule lepoll_trans [of _ i]) |
637 { assume i: "i \<lesssim> n" |
625 apply (erule ltE) |
638 have "succ(n) \<lesssim> i" using n |
626 apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+) |
639 by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll]) |
627 done |
640 also have "... \<lesssim> n" by (rule i) |
628 |
641 finally have "succ(n) \<lesssim> n" . |
629 lemma Ord_nat_eqpoll_iff: "[| Ord(i); n:nat |] ==> i \<approx> n \<longleftrightarrow> i=n" |
642 hence False by (rule succ_lepoll_natE) (rule n) } |
630 apply (rule iffI) |
643 thus ?thesis by auto |
631 prefer 2 apply (simp add: eqpoll_refl) |
644 qed |
632 apply (rule Ord_linear_lt [of i n]) |
645 |
633 apply (simp_all add: nat_into_Ord) |
646 text{*A slightly weaker version of @{text nat_eqpoll_iff}*} |
634 apply (erule lt_nat_in_nat [THEN nat_eqpoll_iff, THEN iffD1], assumption+) |
647 lemma Ord_nat_eqpoll_iff: |
635 apply (rule lt_not_lepoll [THEN notE], assumption+) |
648 assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n" |
636 apply (erule eqpoll_imp_lepoll) |
649 proof (cases rule: Ord_linear_lt [OF i]) |
637 done |
650 show "Ord(n)" using n by auto |
|
651 next |
|
652 assume "i < n" |
|
653 hence "i \<in> nat" by (rule lt_nat_in_nat) (rule n) |
|
654 thus ?thesis by (simp add: nat_eqpoll_iff n) |
|
655 next |
|
656 assume "i = n" |
|
657 thus ?thesis by (simp add: eqpoll_refl) |
|
658 next |
|
659 assume "n < i" |
|
660 hence "~ i \<lesssim> n" using n by (rule lt_not_lepoll) |
|
661 hence "~ i \<approx> n" using n by (blast intro: eqpoll_imp_lepoll) |
|
662 moreover have "i \<noteq> n" using `n<i` by auto |
|
663 ultimately show ?thesis by blast |
|
664 qed |
638 |
665 |
639 lemma Card_nat: "Card(nat)" |
666 lemma Card_nat: "Card(nat)" |
640 apply (unfold Card_def cardinal_def) |
667 proof - |
641 apply (subst Least_equality) |
668 { fix i |
642 apply (rule eqpoll_refl) |
669 assume i: "i < nat" "i \<approx> nat" |
643 apply (rule Ord_nat) |
670 hence "~ nat \<lesssim> i" |
644 apply (erule ltE) |
671 by (simp add: lt_def lt_not_lepoll) |
645 apply (simp_all add: eqpoll_iff lt_not_lepoll ltI) |
672 hence False using i |
646 done |
673 by (simp add: eqpoll_iff) |
|
674 } |
|
675 hence "(\<mu> i. i \<approx> nat) = nat" by (blast intro: Least_equality eqpoll_refl) |
|
676 thus ?thesis |
|
677 by (auto simp add: Card_def cardinal_def) |
|
678 qed |
647 |
679 |
648 (*Allows showing that |i| is a limit cardinal*) |
680 (*Allows showing that |i| is a limit cardinal*) |
649 lemma nat_le_cardinal: "nat \<le> i ==> nat \<le> |i|" |
681 lemma nat_le_cardinal: "nat \<le> i ==> nat \<le> |i|" |
650 apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst]) |
682 apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst]) |
651 apply (erule cardinal_mono) |
683 apply (erule cardinal_mono) |
734 |
766 |
735 subsection{*Lemmas by Krzysztof Grabczewski*} |
767 subsection{*Lemmas by Krzysztof Grabczewski*} |
736 |
768 |
737 (*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*) |
769 (*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*) |
738 |
770 |
739 (*If A has at most n+1 elements and a:A then A-{a} has at most n.*) |
771 text{*If @{term A} has at most @{term"n+1"} elements and @{term"a \<in> A"} |
|
772 then @{term"A-{a}"} has at most @{term n}.*} |
740 lemma Diff_sing_lepoll: |
773 lemma Diff_sing_lepoll: |
741 "[| a:A; A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n" |
774 "[| a \<in> A; A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n" |
742 apply (unfold succ_def) |
775 apply (unfold succ_def) |
743 apply (rule cons_lepoll_consD) |
776 apply (rule cons_lepoll_consD) |
744 apply (rule_tac [3] mem_not_refl) |
777 apply (rule_tac [3] mem_not_refl) |
745 apply (erule cons_Diff [THEN ssubst], safe) |
778 apply (erule cons_Diff [THEN ssubst], safe) |
746 done |
779 done |
747 |
780 |
748 (*If A has at least n+1 elements then A-{a} has at least n.*) |
781 text{*If @{term A} has at least @{term"n+1"} elements then @{term"A-{a}"} has at least @{term n}.*} |
749 lemma lepoll_Diff_sing: |
782 lemma lepoll_Diff_sing: |
750 "[| succ(n) \<lesssim> A |] ==> n \<lesssim> A - {a}" |
783 assumes A: "succ(n) \<lesssim> A" shows "n \<lesssim> A - {a}" |
751 apply (unfold succ_def) |
784 proof - |
752 apply (rule cons_lepoll_consD) |
785 have "cons(n,n) \<lesssim> A" using A |
753 apply (rule_tac [2] mem_not_refl) |
786 by (unfold succ_def) |
754 prefer 2 apply blast |
787 also have "... \<lesssim> cons(a, A-{a})" |
755 apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans]) |
788 by (blast intro: subset_imp_lepoll) |
756 done |
789 finally have "cons(n,n) \<lesssim> cons(a, A-{a})" . |
757 |
790 thus ?thesis |
758 lemma Diff_sing_eqpoll: "[| a:A; A \<approx> succ(n) |] ==> A - {a} \<approx> n" |
791 by (blast intro: cons_lepoll_consD mem_irrefl) |
|
792 qed |
|
793 |
|
794 lemma Diff_sing_eqpoll: "[| a \<in> A; A \<approx> succ(n) |] ==> A - {a} \<approx> n" |
759 by (blast intro!: eqpollI |
795 by (blast intro!: eqpollI |
760 elim!: eqpollE |
796 elim!: eqpollE |
761 intro: Diff_sing_lepoll lepoll_Diff_sing) |
797 intro: Diff_sing_lepoll lepoll_Diff_sing) |
762 |
798 |
763 lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a:A |] ==> A = {a}" |
799 lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a \<in> A |] ==> A = {a}" |
764 apply (frule Diff_sing_lepoll, assumption) |
800 apply (frule Diff_sing_lepoll, assumption) |
765 apply (drule lepoll_0_is_0) |
801 apply (drule lepoll_0_is_0) |
766 apply (blast elim: equalityE) |
802 apply (blast elim: equalityE) |
767 done |
803 done |
768 |
804 |
769 lemma Un_lepoll_sum: "A \<union> B \<lesssim> A+B" |
805 lemma Un_lepoll_sum: "A \<union> B \<lesssim> A+B" |
770 apply (unfold lepoll_def) |
806 apply (unfold lepoll_def) |
771 apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x:A then Inl (x) else Inr (x) " in exI) |
807 apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x\<in>A then Inl (x) else Inr (x)" in exI) |
772 apply (rule_tac d = "%z. snd (z) " in lam_injective) |
808 apply (rule_tac d = "%z. snd (z)" in lam_injective) |
773 apply force |
809 apply force |
774 apply (simp add: Inl_def Inr_def) |
810 apply (simp add: Inl_def Inr_def) |
775 done |
811 done |
776 |
812 |
777 lemma well_ord_Un: |
813 lemma well_ord_Un: |
780 assumption) |
816 assumption) |
781 |
817 |
782 (*Krzysztof Grabczewski*) |
818 (*Krzysztof Grabczewski*) |
783 lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 ==> A \<union> B \<approx> A + B" |
819 lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 ==> A \<union> B \<approx> A + B" |
784 apply (unfold eqpoll_def) |
820 apply (unfold eqpoll_def) |
785 apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a:A then Inl (a) else Inr (a) " in exI) |
821 apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a \<in> A then Inl (a) else Inr (a)" in exI) |
786 apply (rule_tac d = "%z. case (%x. x, %x. x, z) " in lam_bijective) |
822 apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective) |
787 apply auto |
823 apply auto |
788 done |
824 done |
789 |
825 |
790 |
826 |
791 subsection {*Finite and infinite sets*} |
827 subsection {*Finite and infinite sets*} |
793 lemma Finite_0 [simp]: "Finite(0)" |
829 lemma Finite_0 [simp]: "Finite(0)" |
794 apply (unfold Finite_def) |
830 apply (unfold Finite_def) |
795 apply (blast intro!: eqpoll_refl nat_0I) |
831 apply (blast intro!: eqpoll_refl nat_0I) |
796 done |
832 done |
797 |
833 |
798 lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n; n:nat |] ==> Finite(A)" |
834 lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n; n \<in> nat |] ==> Finite(A)" |
799 apply (unfold Finite_def) |
835 apply (unfold Finite_def) |
800 apply (erule rev_mp) |
836 apply (erule rev_mp) |
801 apply (erule nat_induct) |
837 apply (erule nat_induct) |
802 apply (blast dest!: lepoll_0_is_0 intro!: eqpoll_refl nat_0I) |
838 apply (blast dest!: lepoll_0_is_0 intro!: eqpoll_refl nat_0I) |
803 apply (blast dest!: lepoll_succ_disj) |
839 apply (blast dest!: lepoll_succ_disj) |
809 apply (blast dest: ltD lesspoll_cardinal_lt |
845 apply (blast dest: ltD lesspoll_cardinal_lt |
810 lesspoll_imp_eqpoll [THEN eqpoll_sym]) |
846 lesspoll_imp_eqpoll [THEN eqpoll_sym]) |
811 done |
847 done |
812 |
848 |
813 lemma lepoll_Finite: |
849 lemma lepoll_Finite: |
814 "[| Y \<lesssim> X; Finite(X) |] ==> Finite(Y)" |
850 assumes Y: "Y \<lesssim> X" and X: "Finite(X)" shows "Finite(Y)" |
815 apply (unfold Finite_def) |
851 proof - |
816 apply (blast elim!: eqpollE |
852 obtain n where n: "n \<in> nat" "X \<approx> n" using X |
817 intro: lepoll_trans [THEN lepoll_nat_imp_Finite |
853 by (auto simp add: Finite_def) |
818 [unfolded Finite_def]]) |
854 have "Y \<lesssim> X" by (rule Y) |
819 done |
855 also have "... \<approx> n" by (rule n) |
|
856 finally have "Y \<lesssim> n" . |
|
857 thus ?thesis using n by (simp add: lepoll_nat_imp_Finite) |
|
858 qed |
820 |
859 |
821 lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite] |
860 lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite] |
822 |
861 |
823 lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \<inter> B)" |
862 lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \<inter> B)" |
824 by (blast intro: subset_Finite) |
863 by (blast intro: subset_Finite) |
945 done |
984 done |
946 |
985 |
947 (*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) |
986 (*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) |
948 lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)" |
987 lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)" |
949 apply (unfold Finite_def) |
988 apply (unfold Finite_def) |
950 apply (case_tac "a:A") |
989 apply (case_tac "a \<in> A") |
951 apply (subgoal_tac [2] "A-{a}=A", auto) |
990 apply (subgoal_tac [2] "A-{a}=A", auto) |
952 apply (rule_tac x = "succ (n) " in bexI) |
991 apply (rule_tac x = "succ (n) " in bexI) |
953 apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ") |
992 apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ") |
954 apply (drule_tac a = a and b = n in cons_eqpoll_cong) |
993 apply (drule_tac a = a and b = n in cons_eqpoll_cong) |
955 apply (auto dest: mem_irrefl) |
994 apply (auto dest: mem_irrefl) |
1008 |
1047 |
1009 |
1048 |
1010 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered |
1049 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered |
1011 set is well-ordered. Proofs simplified by lcp. *) |
1050 set is well-ordered. Proofs simplified by lcp. *) |
1012 |
1051 |
1013 lemma nat_wf_on_converse_Memrel: "n:nat ==> wf[n](converse(Memrel(n)))" |
1052 lemma nat_wf_on_converse_Memrel: "n \<in> nat ==> wf[n](converse(Memrel(n)))" |
1014 apply (erule nat_induct) |
1053 apply (erule nat_induct) |
1015 apply (blast intro: wf_onI) |
1054 apply (blast intro: wf_onI) |
1016 apply (rule wf_onI) |
1055 apply (rule wf_onI) |
1017 apply (simp add: wf_on_def wf_def) |
1056 apply (simp add: wf_on_def wf_def) |
1018 apply (case_tac "x:Z") |
1057 apply (case_tac "x:Z") |
1021 apply (blast elim: mem_irrefl mem_asym) |
1060 apply (blast elim: mem_irrefl mem_asym) |
1022 txt{*other case*} |
1061 txt{*other case*} |
1023 apply (drule_tac x = Z in spec, blast) |
1062 apply (drule_tac x = Z in spec, blast) |
1024 done |
1063 done |
1025 |
1064 |
1026 lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))" |
1065 lemma nat_well_ord_converse_Memrel: "n \<in> nat ==> well_ord(n,converse(Memrel(n)))" |
1027 apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel]) |
1066 apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel]) |
1028 apply (unfold well_ord_def) |
1067 apply (unfold well_ord_def) |
1029 apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel) |
1068 apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel) |
1030 done |
1069 done |
1031 |
1070 |
1038 apply (simp add: rvimage_converse converse_Int converse_prod |
1077 apply (simp add: rvimage_converse converse_Int converse_prod |
1039 ordertype_ord_iso [THEN ord_iso_rvimage_eq]) |
1078 ordertype_ord_iso [THEN ord_iso_rvimage_eq]) |
1040 done |
1079 done |
1041 |
1080 |
1042 lemma ordertype_eq_n: |
1081 lemma ordertype_eq_n: |
1043 "[| well_ord(A,r); A \<approx> n; n:nat |] ==> ordertype(A,r)=n" |
1082 assumes r: "well_ord(A,r)" and A: "A \<approx> n" and n: "n \<in> nat" |
1044 apply (rule Ord_ordertype [THEN Ord_nat_eqpoll_iff, THEN iffD1], assumption+) |
1083 shows "ordertype(A,r) = n" |
1045 apply (rule eqpoll_trans) |
1084 proof - |
1046 prefer 2 apply assumption |
1085 have "ordertype(A,r) \<approx> A" |
1047 apply (unfold eqpoll_def) |
1086 by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r) |
1048 apply (blast intro!: ordermap_bij [THEN bij_converse_bij]) |
1087 also have "... \<approx> n" by (rule A) |
1049 done |
1088 finally have "ordertype(A,r) \<approx> n" . |
|
1089 thus ?thesis |
|
1090 by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r) |
|
1091 qed |
1050 |
1092 |
1051 lemma Finite_well_ord_converse: |
1093 lemma Finite_well_ord_converse: |
1052 "[| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))" |
1094 "[| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))" |
1053 apply (unfold Finite_def) |
1095 apply (unfold Finite_def) |
1054 apply (rule well_ord_converse, assumption) |
1096 apply (rule well_ord_converse, assumption) |
1055 apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel) |
1097 apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel) |
1056 done |
1098 done |
1057 |
1099 |
1058 lemma nat_into_Finite: "n:nat ==> Finite(n)" |
1100 lemma nat_into_Finite: "n \<in> nat ==> Finite(n)" |
1059 apply (unfold Finite_def) |
1101 apply (unfold Finite_def) |
1060 apply (fast intro!: eqpoll_refl) |
1102 apply (fast intro!: eqpoll_refl) |
1061 done |
1103 done |
1062 |
1104 |
1063 lemma nat_not_Finite: "~Finite(nat)" |
1105 lemma nat_not_Finite: "~ Finite(nat)" |
1064 apply (unfold Finite_def, clarify) |
1106 proof - |
1065 apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp) |
1107 { fix n |
1066 apply (insert Card_nat) |
1108 assume n: "n \<in> nat" "nat \<approx> n" |
1067 apply (simp add: Card_def) |
1109 have "n \<in> nat" by (rule n) |
1068 apply (drule le_imp_subset) |
1110 also have "... = n" using n |
1069 apply (blast elim: mem_irrefl) |
1111 by (simp add: Ord_nat_eqpoll_iff Ord_nat) |
1070 done |
1112 finally have "n \<in> n" . |
|
1113 hence False |
|
1114 by (blast elim: mem_irrefl) |
|
1115 } |
|
1116 thus ?thesis |
|
1117 by (auto simp add: Finite_def) |
|
1118 qed |
1071 |
1119 |
1072 end |
1120 end |