1.1 --- a/src/ZF/Cardinal.thy	Fri Mar 16 16:32:34 2012 +0000
     1.2 +++ b/src/ZF/Cardinal.thy	Fri Mar 16 17:41:53 2012 +0000
     1.3 @@ -251,13 +251,28 @@
     1.4  apply (erule Ord_linear_lt, assumption, blast+)
     1.5  done
     1.6  
     1.7 -lemma LeastI: "[| P(i);  Ord(i) |] ==> P(\<mu> x. P(x))"
     1.8 -apply (erule rev_mp)
     1.9 -apply (erule_tac i=i in trans_induct)
    1.10 -apply (rule impI)
    1.11 -apply (rule classical)
    1.12 -apply (blast intro: Least_equality [THEN ssubst]  elim!: ltE)
    1.13 -done
    1.14 +lemma LeastI: 
    1.15 +  assumes P: "P(i)" and i: "Ord(i)" shows "P(\<mu> x. P(x))"
    1.16 +proof -
    1.17 +  { from i have "P(i) \<Longrightarrow> P(\<mu> x. P(x))"
    1.18 +      proof (induct i rule: trans_induct)
    1.19 +        case (step i) 
    1.20 +        show ?case
    1.21 +          proof (cases "P(\<mu> a. P(a))")
    1.22 +            case True thus ?thesis .
    1.23 +          next
    1.24 +            case False
    1.25 +            hence "\<And>x. x \<in> i \<Longrightarrow> ~P(x)" using step
    1.26 +              by blast
    1.27 +            hence "(\<mu> x. P(x)) = i" using step
    1.28 +              by (blast intro: Least_equality elim!: ltE) 
    1.29 +            thus ?thesis using step
    1.30 +              by simp 
    1.31 +          qed
    1.32 +      qed
    1.33 +  }
    1.34 +  thus ?thesis using P .
    1.35 +qed
    1.36  
    1.37  (*Proof is almost identical to the one above!*)
    1.38  lemma Least_le: "[| P(i);  Ord(i) |] ==> (\<mu> x. P(x)) \<le> i"
    1.39 @@ -442,10 +457,11 @@
    1.40  
    1.41  lemma cardinal_mono:
    1.42    assumes ij: "i \<le> j" shows "|i| \<le> |j|"
    1.43 -proof (cases rule: Ord_linear_le [OF Ord_cardinal Ord_cardinal])
    1.44 -  assume "|i| \<le> |j|" thus ?thesis .
    1.45 +using Ord_cardinal [of i] Ord_cardinal [of j]
    1.46 +proof (cases rule: Ord_linear_le)
    1.47 +  case le thus ?thesis .
    1.48  next
    1.49 -  assume cj: "|j| \<le> |i|"
    1.50 +  case ge
    1.51    have i: "Ord(i)" using ij
    1.52      by (simp add: lt_Ord)
    1.53    have ci: "|i| \<le> j"
    1.54 @@ -453,12 +469,12 @@
    1.55    have "|i| = ||i||"
    1.56      by (auto simp add: Ord_cardinal_idem i)
    1.57    also have "... = |j|"
    1.58 -    by (rule cardinal_eq_lemma [OF cj ci])
    1.59 +    by (rule cardinal_eq_lemma [OF ge ci])
    1.60    finally have "|i| = |j|" .
    1.61    thus ?thesis by simp
    1.62  qed
    1.63  
    1.64 -(*Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of cardinal_mono fails!*)
    1.65 +text{*Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of @{text cardinal_mono} fails!*}
    1.66  lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
    1.67  apply (rule Ord_linear2 [of i j], assumption+)
    1.68  apply (erule lt_trans2 [THEN lt_irrefl])
    1.69 @@ -478,12 +494,15 @@
    1.70  lemma well_ord_lepoll_imp_Card_le:
    1.71    assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
    1.72    shows "|A| \<le> |B|"
    1.73 -proof (rule Ord_linear_le [of "|A|" "|B|", OF Ord_cardinal Ord_cardinal], assumption)
    1.74 -  assume BA: "|B| \<le> |A|"
    1.75 +using Ord_cardinal [of A] Ord_cardinal [of B]
    1.76 +proof (cases rule: Ord_linear_le)
    1.77 +  case le thus ?thesis .
    1.78 +next
    1.79 +  case ge
    1.80    from lepoll_well_ord [OF AB wB]
    1.81    obtain s where s: "well_ord(A, s)" by blast
    1.82    have "B  \<approx> |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll)
    1.83 -  also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF BA])
    1.84 +  also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF ge])
    1.85    also have "... \<approx> A" by (rule well_ord_cardinal_eqpoll [OF s])
    1.86    finally have "B \<lesssim> A" .
    1.87    hence "A \<approx> B" by (blast intro: eqpollI AB)
    1.88 @@ -652,17 +671,16 @@
    1.89  text{*A slightly weaker version of @{text nat_eqpoll_iff}*}
    1.90  lemma Ord_nat_eqpoll_iff:
    1.91    assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n"
    1.92 -proof (cases rule: Ord_linear_lt [OF i])
    1.93 -  show "Ord(n)" using n by auto
    1.94 -next
    1.95 -  assume "i < n"
    1.96 +using i nat_into_Ord [OF n]
    1.97 +proof (cases rule: Ord_linear_lt)
    1.98 +  case lt
    1.99    hence  "i \<in> nat" by (rule lt_nat_in_nat) (rule n)
   1.100    thus ?thesis by (simp add: nat_eqpoll_iff n)
   1.101  next
   1.102 -  assume "i = n"
   1.103 +  case eq
   1.104    thus ?thesis by (simp add: eqpoll_refl)
   1.105  next
   1.106 -  assume "n < i"
   1.107 +  case gt
   1.108    hence  "~ i \<lesssim> n" using n  by (rule lt_not_lepoll)
   1.109    hence  "~ i \<approx> n" using n  by (blast intro: eqpoll_imp_lepoll)
   1.110    moreover have "i \<noteq> n" using `n<i` by auto