626 (*Main result: Kunen's Theorem 10.12*) |
626 (*Main result: Kunen's Theorem 10.12*) |
627 lemma InfCard_csquare_eq: |
627 lemma InfCard_csquare_eq: |
628 assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K" |
628 assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K" |
629 proof - |
629 proof - |
630 have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) |
630 have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) |
631 have "InfCard(K) \<longrightarrow> K \<otimes> K = K" |
631 show "InfCard(K) ==> K \<otimes> K = K" using OK |
632 proof (rule trans_induct [OF OK], rule impI) |
632 proof (induct rule: trans_induct) |
633 fix i |
633 case (step i) |
634 assume i: "Ord(i)" "InfCard(i)" |
634 show "i \<otimes> i = i" |
635 and ih: " \<forall>y\<in>i. InfCard(y) \<longrightarrow> y \<otimes> y = y" |
635 proof (rule le_anti_sym) |
636 show "i \<otimes> i = i" |
636 have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" |
637 proof (rule le_anti_sym) |
637 by (rule cardinal_cong, |
638 have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" |
638 simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll]) |
639 by (rule cardinal_cong, |
639 hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" |
640 simp add: i well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll]) |
640 by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype]) |
641 hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" using i |
641 moreover |
642 by (simp add: cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype]) |
642 have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using step |
643 moreover |
643 by (simp add: ordertype_csquare_le) |
644 have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using ih i |
644 ultimately show "i \<otimes> i \<le> i" by (rule le_trans) |
645 by (simp add: ordertype_csquare_le) |
645 next |
646 ultimately show "i \<otimes> i \<le> i" by (rule le_trans) |
646 show "i \<le> i \<otimes> i" using step |
647 next |
647 by (blast intro: cmult_square_le InfCard_is_Card) |
648 show "i \<le> i \<otimes> i" using i |
|
649 by (blast intro: cmult_square_le InfCard_is_Card) |
|
650 qed |
|
651 qed |
648 qed |
652 thus ?thesis using IK .. |
649 qed |
653 qed |
650 qed |
654 |
651 |
655 (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*) |
652 (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*) |
656 lemma well_ord_InfCard_square_eq: |
653 lemma well_ord_InfCard_square_eq: |
657 assumes r: "well_ord(A,r)" and I: "InfCard(|A|)" shows "A \<times> A \<approx> A" |
654 assumes r: "well_ord(A,r)" and I: "InfCard(|A|)" shows "A \<times> A \<approx> A" |
908 also have "... = m #+ n" using m n |
905 also have "... = m #+ n" using m n |
909 by (simp add: nat_cadd_eq_add [symmetric] cadd_def) |
906 by (simp add: nat_cadd_eq_add [symmetric] cadd_def) |
910 finally show ?thesis . |
907 finally show ?thesis . |
911 qed |
908 qed |
912 |
909 |
913 lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<longrightarrow> i \<in> nat | i=nat" |
910 lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<Longrightarrow> i \<in> nat | i=nat" |
914 apply (erule trans_induct3, auto) |
911 proof (induct i rule: trans_induct3) |
915 apply (blast dest!: nat_le_Limit [THEN le_imp_subset]) |
912 case 0 thus ?case by auto |
916 done |
913 next |
|
914 case (succ i) thus ?case by auto |
|
915 next |
|
916 case (limit l) thus ?case |
|
917 by (blast dest: nat_le_Limit le_imp_subset) |
|
918 qed |
917 |
919 |
918 lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)" |
920 lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)" |
919 by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) |
921 by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) |
920 |
922 |
921 lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1" |
923 lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1" |