1.1 --- a/src/HOL/Ln.thy	Wed Dec 01 06:50:54 2010 -0800
     1.2 +++ b/src/HOL/Ln.thy	Wed Dec 01 20:59:29 2010 +0100
     1.3 @@ -9,13 +9,13 @@
     1.4  begin
     1.5  
     1.6  lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n. 
     1.7 -  inverse(real (fact (n+2))) * (x ^ (n+2)))"
     1.8 +  inverse(fact (n+2)) * (x ^ (n+2)))"
     1.9  proof -
    1.10 -  have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"
    1.11 +  have "exp x = suminf (%n. inverse(fact n) * (x ^ n))"
    1.12      by (simp add: exp_def)
    1.13 -  also from summable_exp have "... = (SUM n : {0..<2}. 
    1.14 -      inverse(real (fact n)) * (x ^ n)) + suminf (%n.
    1.15 -      inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")
    1.16 +  also from summable_exp have "... = (SUM n::nat : {0..<2}. 
    1.17 +      inverse(fact n) * (x ^ n)) + suminf (%n.
    1.18 +      inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
    1.19      by (rule suminf_split_initial_segment)
    1.20    also have "?a = 1 + x"
    1.21      by (simp add: numerals)
    1.22 @@ -23,7 +23,7 @@
    1.23  qed
    1.24  
    1.25  lemma exp_tail_after_first_two_terms_summable: 
    1.26 -  "summable (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))"
    1.27 +  "summable (%n. inverse(fact (n+2)) * (x ^ (n+2)))"
    1.28  proof -
    1.29    note summable_exp
    1.30    thus ?thesis
    1.31 @@ -31,20 +31,19 @@
    1.32  qed
    1.33  
    1.34  lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
    1.35 -    shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
    1.36 +    shows "inverse (fact ((n::nat) + 2)) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
    1.37  proof (induct n)
    1.38 -  show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <= 
    1.39 +  show "inverse (fact ((0::nat) + 2)) * x ^ (0 + 2) <= 
    1.40        x ^ 2 / 2 * (1 / 2) ^ 0"
    1.41      by (simp add: real_of_nat_Suc power2_eq_square)
    1.42  next
    1.43    fix n :: nat
    1.44 -  assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
    1.45 +  assume c: "inverse (fact (n + 2)) * x ^ (n + 2)
    1.46         <= x ^ 2 / 2 * (1 / 2) ^ n"
    1.47 -  show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
    1.48 +  show "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2)
    1.49             <= x ^ 2 / 2 * (1 / 2) ^ Suc n"
    1.50    proof -
    1.51 -    have "inverse(real (fact (Suc n + 2))) <= 
    1.52 -        (1 / 2) *inverse (real (fact (n+2)))"
    1.53 +    have "inverse(fact (Suc n + 2)) <= (1/2) * inverse (fact (n+2))"
    1.54      proof -
    1.55        have "Suc n + 2 = Suc (n + 2)" by simp
    1.56        then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)" 
    1.57 @@ -57,12 +56,12 @@
    1.58          by (rule real_of_nat_mult)
    1.59        finally have "real (fact (Suc n + 2)) = 
    1.60           real (Suc (n + 2)) * real (fact (n + 2))" .
    1.61 -      then have "inverse(real (fact (Suc n + 2))) = 
    1.62 -         inverse(real (Suc (n + 2))) * inverse(real (fact (n + 2)))"
    1.63 +      then have "inverse(fact (Suc n + 2)) = 
    1.64 +         inverse(Suc (n + 2)) * inverse(fact (n + 2))"
    1.65          apply (rule ssubst)
    1.66          apply (rule inverse_mult_distrib)
    1.67          done
    1.68 -      also have "... <= (1/2) * inverse(real (fact (n + 2)))"
    1.69 +      also have "... <= (1/2) * inverse(fact (n + 2))"
    1.70          apply (rule mult_right_mono)
    1.71          apply (subst inverse_eq_divide)
    1.72          apply simp
    1.73 @@ -78,8 +77,8 @@
    1.74        apply (rule mult_nonneg_nonneg, rule a)+
    1.75        apply (rule zero_le_power, rule a)
    1.76        done
    1.77 -    ultimately have "inverse (real (fact (Suc n + 2))) *  x ^ (Suc n + 2) <=
    1.78 -        (1 / 2 * inverse (real (fact (n + 2)))) * x ^ (n + 2)"
    1.79 +    ultimately have "inverse (fact (Suc n + 2)) *  x ^ (Suc n + 2) <=
    1.80 +        (1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)"
    1.81        apply (rule mult_mono)
    1.82        apply (rule mult_nonneg_nonneg)
    1.83        apply simp
    1.84 @@ -88,7 +87,7 @@
    1.85        apply (rule zero_le_power)
    1.86        apply (rule a)
    1.87        done
    1.88 -    also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"
    1.89 +    also have "... = 1 / 2 * (inverse (fact (n + 2)) * x ^ (n + 2))"
    1.90        by simp
    1.91      also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
    1.92        apply (rule mult_left_mono)
    1.93 @@ -122,12 +121,12 @@
    1.94  proof -
    1.95    assume a: "0 <= x"
    1.96    assume b: "x <= 1"
    1.97 -  have c: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) * 
    1.98 +  have c: "exp x = 1 + x + suminf (%n. inverse(fact (n+2)) * 
    1.99        (x ^ (n+2)))"
   1.100      by (rule exp_first_two_terms)
   1.101 -  moreover have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <= x^2"
   1.102 +  moreover have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2"
   1.103    proof -
   1.104 -    have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <=
   1.105 +    have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
   1.106          suminf (%n. (x^2/2) * ((1/2)^n))"
   1.107        apply (rule summable_le)
   1.108        apply (auto simp only: aux1 prems)