replace (- 1) with -1
authorhuffman
Thu May 31 23:02:16 2007 +0200 (2007-05-31)
changeset 231773004310c95b1
parent 23176 40a760921d94
child 23178 07ba6b58b3d2
replace (- 1) with -1
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Thu May 31 22:23:50 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu May 31 23:02:16 2007 +0200
     1.3 @@ -421,7 +421,7 @@
     1.4  
     1.5  lemma HFinite_sin [simp]:
     1.6       "sumhr (0, whn, %n. (if even(n) then 0 else  
     1.7 -              ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
     1.8 +              (-1 ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
     1.9                \<in> HFinite"
    1.10  unfolding sumhr_app
    1.11  apply (simp only: star_zero_def starfun2_star_of)
    1.12 @@ -447,7 +447,7 @@
    1.13  
    1.14  lemma HFinite_cos [simp]:
    1.15       "sumhr (0, whn, %n. (if even(n) then  
    1.16 -            ((- 1) ^ (n div 2))/(real (fact n)) else  
    1.17 +            (-1 ^ (n div 2))/(real (fact n)) else  
    1.18              0) * x ^ n) \<in> HFinite"
    1.19  unfolding sumhr_app
    1.20  apply (simp only: star_zero_def starfun2_star_of)
     2.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Thu May 31 22:23:50 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Thu May 31 23:02:16 2007 +0200
     2.3 @@ -243,7 +243,7 @@
     2.4                (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
     2.5                diff n t / real (fact n) * h ^ n"
     2.6  apply (cut_tac f = "%x. f (-x)"
     2.7 -        and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
     2.8 +        and diff = "%n x. (-1 ^ n) * diff n (-x)"
     2.9          and h = "-h" and n = n in Maclaurin_objl)
    2.10  apply (simp)
    2.11  apply safe
    2.12 @@ -412,7 +412,7 @@
    2.13       "\<exists>t. abs t \<le> abs x &
    2.14         sin x =
    2.15         (\<Sum>m=0..<n. (if even m then 0
    2.16 -                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    2.17 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    2.18                         x ^ m)
    2.19        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    2.20  apply (cut_tac f = sin and n = n and x = x
    2.21 @@ -432,7 +432,7 @@
    2.22  lemma Maclaurin_sin_expansion:
    2.23       "\<exists>t. sin x =
    2.24         (\<Sum>m=0..<n. (if even m then 0
    2.25 -                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    2.26 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    2.27                         x ^ m)
    2.28        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    2.29  apply (insert Maclaurin_sin_expansion2 [of x n]) 
    2.30 @@ -446,7 +446,7 @@
    2.31         \<exists>t. 0 < t & t < x &
    2.32         sin x =
    2.33         (\<Sum>m=0..<n. (if even m then 0
    2.34 -                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    2.35 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    2.36                         x ^ m)
    2.37        + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
    2.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)
    2.39 @@ -464,7 +464,7 @@
    2.40         \<exists>t. 0 < t & t \<le> x &
    2.41         sin x =
    2.42         (\<Sum>m=0..<n. (if even m then 0
    2.43 -                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    2.44 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    2.45                         x ^ m)
    2.46        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    2.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)
    2.48 @@ -482,14 +482,14 @@
    2.49  
    2.50  lemma sumr_cos_zero_one [simp]:
    2.51   "(\<Sum>m=0..<(Suc n).
    2.52 -     (if even m then (- 1) ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
    2.53 +     (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
    2.54  by (induct "n", auto)
    2.55  
    2.56  lemma Maclaurin_cos_expansion:
    2.57       "\<exists>t. abs t \<le> abs x &
    2.58         cos x =
    2.59         (\<Sum>m=0..<n. (if even m
    2.60 -                       then (- 1) ^ (m div 2)/(real (fact m))
    2.61 +                       then -1 ^ (m div 2)/(real (fact m))
    2.62                         else 0) *
    2.63                         x ^ m)
    2.64        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    2.65 @@ -512,7 +512,7 @@
    2.66         \<exists>t. 0 < t & t < x &
    2.67         cos x =
    2.68         (\<Sum>m=0..<n. (if even m
    2.69 -                       then (- 1) ^ (m div 2)/(real (fact m))
    2.70 +                       then -1 ^ (m div 2)/(real (fact m))
    2.71                         else 0) *
    2.72                         x ^ m)
    2.73        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    2.74 @@ -531,7 +531,7 @@
    2.75         \<exists>t. x < t & t < 0 &
    2.76         cos x =
    2.77         (\<Sum>m=0..<n. (if even m
    2.78 -                       then (- 1) ^ (m div 2)/(real (fact m))
    2.79 +                       then -1 ^ (m div 2)/(real (fact m))
    2.80                         else 0) *
    2.81                         x ^ m)
    2.82        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
    2.83 @@ -554,7 +554,7 @@
    2.84  by auto
    2.85  
    2.86  lemma Maclaurin_sin_bound:
    2.87 -  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    2.88 +  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    2.89    x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
    2.90  proof -
    2.91    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
    2.92 @@ -576,7 +576,7 @@
    2.93        ?diff n t / real (fact n) * x ^ n" by fast
    2.94    have diff_m_0:
    2.95      "\<And>m. ?diff m 0 = (if even m then 0
    2.96 -         else (- 1) ^ ((m - Suc 0) div 2))"
    2.97 +         else -1 ^ ((m - Suc 0) div 2))"
    2.98      apply (subst even_even_mod_4_iff)
    2.99      apply (cut_tac m=m in mod_exhaust_less_4)
   2.100      apply (elim disjE, simp_all)
     3.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 22:23:50 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 23:02:16 2007 +0200
     3.3 @@ -444,11 +444,11 @@
     3.4  definition
     3.5    sin :: "real => real" where
     3.6    "sin x = (\<Sum>n. (if even(n) then 0 else
     3.7 -             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
     3.8 +             (-1 ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
     3.9   
    3.10  definition
    3.11    cos :: "real => real" where
    3.12 -  "cos x = (\<Sum>n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
    3.13 +  "cos x = (\<Sum>n. (if even(n) then (-1 ^ (n div 2))/(real (fact n)) 
    3.14                              else 0) * x ^ n)"
    3.15  
    3.16  lemma summable_exp_generic:
    3.17 @@ -498,7 +498,7 @@
    3.18  lemma summable_sin: 
    3.19       "summable (%n.  
    3.20             (if even n then 0  
    3.21 -           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
    3.22 +           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
    3.23                  x ^ n)"
    3.24  apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
    3.25  apply (rule_tac [2] summable_exp)
    3.26 @@ -509,7 +509,7 @@
    3.27  lemma summable_cos: 
    3.28        "summable (%n.  
    3.29             (if even n then  
    3.30 -           (- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
    3.31 +           -1 ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
    3.32  apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
    3.33  apply (rule_tac [2] summable_exp)
    3.34  apply (rule_tac x = 0 in exI)
    3.35 @@ -518,12 +518,12 @@
    3.36  
    3.37  lemma lemma_STAR_sin [simp]:
    3.38       "(if even n then 0  
    3.39 -       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
    3.40 +       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
    3.41  by (induct "n", auto)
    3.42  
    3.43  lemma lemma_STAR_cos [simp]:
    3.44       "0 < n -->  
    3.45 -      (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
    3.46 +      -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
    3.47  by (induct "n", auto)
    3.48  
    3.49  lemma lemma_STAR_cos1 [simp]:
    3.50 @@ -532,7 +532,7 @@
    3.51  by (induct "n", auto)
    3.52  
    3.53  lemma lemma_STAR_cos2 [simp]:
    3.54 -  "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) *  0 ^ n 
    3.55 +  "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n 
    3.56                           else 0) = 0"
    3.57  apply (induct "n")
    3.58  apply (case_tac [2] "n", auto)
    3.59 @@ -543,13 +543,13 @@
    3.60  
    3.61  lemma sin_converges: 
    3.62        "(%n. (if even n then 0  
    3.63 -            else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
    3.64 +            else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
    3.65                   x ^ n) sums sin(x)"
    3.66  unfolding sin_def by (rule summable_sin [THEN summable_sums])
    3.67  
    3.68  lemma cos_converges: 
    3.69        "(%n. (if even n then  
    3.70 -           (- 1) ^ (n div 2)/(real (fact n))  
    3.71 +           -1 ^ (n div 2)/(real (fact n))  
    3.72             else 0) * x ^ n) sums cos(x)"
    3.73  unfolding cos_def by (rule summable_cos [THEN summable_sums])
    3.74  
    3.75 @@ -566,9 +566,9 @@
    3.76  
    3.77  lemma sin_fdiffs: 
    3.78        "diffs(%n. if even n then 0  
    3.79 -           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n)))  
    3.80 +           else -1 ^ ((n - Suc 0) div 2)/(real (fact n)))  
    3.81         = (%n. if even n then  
    3.82 -                 (- 1) ^ (n div 2)/(real (fact n))  
    3.83 +                 -1 ^ (n div 2)/(real (fact n))  
    3.84                else 0)"
    3.85  by (auto intro!: ext 
    3.86           simp add: diffs_def divide_inverse real_of_nat_def
    3.87 @@ -576,17 +576,17 @@
    3.88  
    3.89  lemma sin_fdiffs2: 
    3.90         "diffs(%n. if even n then 0  
    3.91 -           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) n  
    3.92 +           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) n  
    3.93         = (if even n then  
    3.94 -                 (- 1) ^ (n div 2)/(real (fact n))  
    3.95 +                 -1 ^ (n div 2)/(real (fact n))  
    3.96                else 0)"
    3.97  by (simp only: sin_fdiffs)
    3.98  
    3.99  lemma cos_fdiffs: 
   3.100        "diffs(%n. if even n then  
   3.101 -                 (- 1) ^ (n div 2)/(real (fact n)) else 0)  
   3.102 +                 -1 ^ (n div 2)/(real (fact n)) else 0)  
   3.103         = (%n. - (if even n then 0  
   3.104 -           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))"
   3.105 +           else -1 ^ ((n - Suc 0)div 2)/(real (fact n))))"
   3.106  by (auto intro!: ext 
   3.107           simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
   3.108           simp del: mult_Suc of_nat_Suc)
   3.109 @@ -594,16 +594,16 @@
   3.110  
   3.111  lemma cos_fdiffs2: 
   3.112        "diffs(%n. if even n then  
   3.113 -                 (- 1) ^ (n div 2)/(real (fact n)) else 0) n 
   3.114 +                 -1 ^ (n div 2)/(real (fact n)) else 0) n 
   3.115         = - (if even n then 0  
   3.116 -           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
   3.117 +           else -1 ^ ((n - Suc 0)div 2)/(real (fact n)))"
   3.118  by (simp only: cos_fdiffs)
   3.119  
   3.120  text{*Now at last we can get the derivatives of exp, sin and cos*}
   3.121  
   3.122  lemma lemma_sin_minus:
   3.123       "- sin x = (\<Sum>n. - ((if even n then 0 
   3.124 -                  else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
   3.125 +                  else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
   3.126  by (auto intro!: sums_unique sums_minus sin_converges)
   3.127  
   3.128  lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /# real (fact n))"
   3.129 @@ -622,13 +622,13 @@
   3.130  lemma lemma_sin_ext:
   3.131       "sin = (%x. \<Sum>n. 
   3.132                     (if even n then 0  
   3.133 -                       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
   3.134 +                       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
   3.135                     x ^ n)"
   3.136  by (auto intro!: ext simp add: sin_def)
   3.137  
   3.138  lemma lemma_cos_ext:
   3.139       "cos = (%x. \<Sum>n. 
   3.140 -                   (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) *
   3.141 +                   (if even n then -1 ^ (n div 2)/(real (fact n)) else 0) *
   3.142                     x ^ n)"
   3.143  by (auto intro!: ext simp add: cos_def)
   3.144  
   3.145 @@ -1003,7 +1003,7 @@
   3.146  lemma cos_zero [simp]: "cos 0 = 1"
   3.147  apply (simp add: cos_def)
   3.148  apply (rule sums_unique [symmetric])
   3.149 -apply (cut_tac n = 1 and f = "(%n. (if even n then (- 1) ^ (n div 2) / (real (fact n)) else 0) * 0 ^ n)" in lemma_series_zero2)
   3.150 +apply (cut_tac n = 1 and f = "(%n. (if even n then -1 ^ (n div 2) / (real (fact n)) else 0) * 0 ^ n)" in lemma_series_zero2)
   3.151  apply auto
   3.152  done
   3.153  
   3.154 @@ -1243,12 +1243,12 @@
   3.155     hence define pi.*}
   3.156  
   3.157  lemma sin_paired:
   3.158 -     "(%n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
   3.159 +     "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
   3.160        sums  sin x"
   3.161  proof -
   3.162    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
   3.163              (if even k then 0
   3.164 -             else (- 1) ^ ((k - Suc 0) div 2) / real (fact k)) *
   3.165 +             else -1 ^ ((k - Suc 0) div 2) / real (fact k)) *
   3.166              x ^ k) 
   3.167  	sums sin x"
   3.168      unfolding sin_def
   3.169 @@ -1259,8 +1259,8 @@
   3.170  lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
   3.171  apply (subgoal_tac 
   3.172         "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
   3.173 -              (- 1) ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1)) 
   3.174 -     sums (\<Sum>n. (- 1) ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
   3.175 +              -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1)) 
   3.176 +     sums (\<Sum>n. -1 ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
   3.177   prefer 2
   3.178   apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp) 
   3.179  apply (rotate_tac 2)
   3.180 @@ -1312,10 +1312,10 @@
   3.181  done
   3.182  
   3.183  lemma cos_paired:
   3.184 -     "(%n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
   3.185 +     "(%n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
   3.186  proof -
   3.187    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
   3.188 -            (if even k then (- 1) ^ (k div 2) / real (fact k) else 0) *
   3.189 +            (if even k then -1 ^ (k div 2) / real (fact k) else 0) *
   3.190              x ^ k) 
   3.191          sums cos x"
   3.192      unfolding cos_def
   3.193 @@ -1334,7 +1334,7 @@
   3.194  apply (rule neg_less_iff_less [THEN iffD1]) 
   3.195  apply (frule sums_unique, auto)
   3.196  apply (rule_tac y =
   3.197 - "\<Sum>n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
   3.198 + "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
   3.199         in order_less_trans)
   3.200  apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
   3.201  apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)