src/HOL/Ln.thy
 changeset 40864 4abaaadfdaf2 parent 36777 be5461582d0f child 41550 efa734d9b221
```     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.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.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)
```