src/HOL/Hyperreal/MacLaurin.thy
changeset 23177 3004310c95b1
parent 23069 cdfff0241c12
child 23242 e1526d5fa80d
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Thu May 31 22:23:50 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Thu May 31 23:02:16 2007 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4                (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
     1.5                diff n t / real (fact n) * h ^ n"
     1.6  apply (cut_tac f = "%x. f (-x)"
     1.7 -        and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
     1.8 +        and diff = "%n x. (-1 ^ n) * diff n (-x)"
     1.9          and h = "-h" and n = n in Maclaurin_objl)
    1.10  apply (simp)
    1.11  apply safe
    1.12 @@ -412,7 +412,7 @@
    1.13       "\<exists>t. abs t \<le> abs x &
    1.14         sin x =
    1.15         (\<Sum>m=0..<n. (if even m then 0
    1.16 -                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    1.17 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    1.18                         x ^ m)
    1.19        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    1.20  apply (cut_tac f = sin and n = n and x = x
    1.21 @@ -432,7 +432,7 @@
    1.22  lemma Maclaurin_sin_expansion:
    1.23       "\<exists>t. sin x =
    1.24         (\<Sum>m=0..<n. (if even m then 0
    1.25 -                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    1.26 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    1.27                         x ^ m)
    1.28        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    1.29  apply (insert Maclaurin_sin_expansion2 [of x n]) 
    1.30 @@ -446,7 +446,7 @@
    1.31         \<exists>t. 0 < t & t < x &
    1.32         sin x =
    1.33         (\<Sum>m=0..<n. (if even m then 0
    1.34 -                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    1.35 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    1.36                         x ^ m)
    1.37        + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
    1.38  apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
    1.39 @@ -464,7 +464,7 @@
    1.40         \<exists>t. 0 < t & t \<le> x &
    1.41         sin x =
    1.42         (\<Sum>m=0..<n. (if even m then 0
    1.43 -                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    1.44 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    1.45                         x ^ m)
    1.46        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    1.47  apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
    1.48 @@ -482,14 +482,14 @@
    1.49  
    1.50  lemma sumr_cos_zero_one [simp]:
    1.51   "(\<Sum>m=0..<(Suc n).
    1.52 -     (if even m then (- 1) ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
    1.53 +     (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
    1.54  by (induct "n", auto)
    1.55  
    1.56  lemma Maclaurin_cos_expansion:
    1.57       "\<exists>t. abs t \<le> abs x &
    1.58         cos x =
    1.59         (\<Sum>m=0..<n. (if even m
    1.60 -                       then (- 1) ^ (m div 2)/(real (fact m))
    1.61 +                       then -1 ^ (m div 2)/(real (fact m))
    1.62                         else 0) *
    1.63                         x ^ m)
    1.64        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    1.65 @@ -512,7 +512,7 @@
    1.66         \<exists>t. 0 < t & t < x &
    1.67         cos x =
    1.68         (\<Sum>m=0..<n. (if even m
    1.69 -                       then (- 1) ^ (m div 2)/(real (fact m))
    1.70 +                       then -1 ^ (m div 2)/(real (fact m))
    1.71                         else 0) *
    1.72                         x ^ m)
    1.73        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    1.74 @@ -531,7 +531,7 @@
    1.75         \<exists>t. x < t & t < 0 &
    1.76         cos x =
    1.77         (\<Sum>m=0..<n. (if even m
    1.78 -                       then (- 1) ^ (m div 2)/(real (fact m))
    1.79 +                       then -1 ^ (m div 2)/(real (fact m))
    1.80                         else 0) *
    1.81                         x ^ m)
    1.82        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    1.83 @@ -554,7 +554,7 @@
    1.84  by auto
    1.85  
    1.86  lemma Maclaurin_sin_bound:
    1.87 -  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    1.88 +  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    1.89    x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
    1.90  proof -
    1.91    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
    1.92 @@ -576,7 +576,7 @@
    1.93        ?diff n t / real (fact n) * x ^ n" by fast
    1.94    have diff_m_0:
    1.95      "\<And>m. ?diff m 0 = (if even m then 0
    1.96 -         else (- 1) ^ ((m - Suc 0) div 2))"
    1.97 +         else -1 ^ ((m - Suc 0) div 2))"
    1.98      apply (subst even_even_mod_4_iff)
    1.99      apply (cut_tac m=m in mod_exhaust_less_4)
   1.100      apply (elim disjE, simp_all)