src/ZF/CardinalArith.thy
changeset 46935 38ecb2dc3636
parent 46907 eea3eb057fea
child 46952 5e1bcfdcb175
     1.1 --- a/src/ZF/CardinalArith.thy	Wed Mar 14 14:53:48 2012 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Wed Mar 14 17:19:08 2012 +0000
     1.3 @@ -628,28 +628,25 @@
     1.4    assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
     1.5  proof -
     1.6    have  OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) 
     1.7 -  have "InfCard(K) \<longrightarrow> K \<otimes> K = K"
     1.8 -    proof (rule trans_induct [OF OK], rule impI)
     1.9 -      fix i
    1.10 -      assume i: "Ord(i)" "InfCard(i)"
    1.11 -         and ih: " \<forall>y\<in>i. InfCard(y) \<longrightarrow> y \<otimes> y = y"
    1.12 -      show "i \<otimes> i = i"
    1.13 -        proof (rule le_anti_sym)
    1.14 -          have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" 
    1.15 -            by (rule cardinal_cong, 
    1.16 -                simp add: i well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
    1.17 -          hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" using i
    1.18 -            by (simp add: cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
    1.19 -          moreover
    1.20 -          have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using ih i
    1.21 -            by (simp add: ordertype_csquare_le) 
    1.22 -          ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
    1.23 -        next
    1.24 -          show "i \<le> i \<otimes> i" using i
    1.25 -            by (blast intro: cmult_square_le InfCard_is_Card) 
    1.26 -        qed
    1.27 +  show "InfCard(K) ==> K \<otimes> K = K" using OK
    1.28 +  proof (induct rule: trans_induct)
    1.29 +    case (step i)
    1.30 +    show "i \<otimes> i = i"
    1.31 +    proof (rule le_anti_sym)
    1.32 +      have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" 
    1.33 +        by (rule cardinal_cong, 
    1.34 +          simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
    1.35 +      hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" 
    1.36 +        by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
    1.37 +      moreover
    1.38 +      have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using step
    1.39 +        by (simp add: ordertype_csquare_le) 
    1.40 +      ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
    1.41 +    next
    1.42 +      show "i \<le> i \<otimes> i" using step
    1.43 +        by (blast intro: cmult_square_le InfCard_is_Card) 
    1.44      qed
    1.45 -  thus ?thesis using IK ..
    1.46 +  qed
    1.47  qed
    1.48  
    1.49  (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
    1.50 @@ -910,10 +907,15 @@
    1.51    finally show ?thesis .
    1.52  qed
    1.53  
    1.54 -lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<longrightarrow> i \<in> nat | i=nat"
    1.55 -apply (erule trans_induct3, auto)
    1.56 -apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
    1.57 -done
    1.58 +lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<Longrightarrow> i \<in> nat | i=nat"
    1.59 +proof (induct i rule: trans_induct3)
    1.60 +  case 0 thus ?case by auto
    1.61 +next
    1.62 +  case (succ i) thus ?case by auto
    1.63 +next
    1.64 +  case (limit l) thus ?case
    1.65 +    by (blast dest: nat_le_Limit le_imp_subset)
    1.66 +qed
    1.67  
    1.68  lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)"
    1.69  by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)