src/HOL/Hyperreal/Transcendental.thy
 changeset 23177 3004310c95b1 parent 23176 40a760921d94 child 23241 5f12b40a95bf
```     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 22:23:50 2007 +0200
1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 23:02:16 2007 +0200
1.3 @@ -444,11 +444,11 @@
1.4  definition
1.5    sin :: "real => real" where
1.6    "sin x = (\<Sum>n. (if even(n) then 0 else
1.7 -             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
1.8 +             (-1 ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
1.9
1.10  definition
1.11    cos :: "real => real" where
1.12 -  "cos x = (\<Sum>n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n))
1.13 +  "cos x = (\<Sum>n. (if even(n) then (-1 ^ (n div 2))/(real (fact n))
1.14                              else 0) * x ^ n)"
1.15
1.16  lemma summable_exp_generic:
1.17 @@ -498,7 +498,7 @@
1.18  lemma summable_sin:
1.19       "summable (%n.
1.20             (if even n then 0
1.21 -           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *
1.22 +           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *
1.23                  x ^ n)"
1.24  apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
1.25  apply (rule_tac [2] summable_exp)
1.26 @@ -509,7 +509,7 @@
1.27  lemma summable_cos:
1.28        "summable (%n.
1.29             (if even n then
1.30 -           (- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
1.31 +           -1 ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
1.32  apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
1.33  apply (rule_tac [2] summable_exp)
1.34  apply (rule_tac x = 0 in exI)
1.35 @@ -518,12 +518,12 @@
1.36
1.37  lemma lemma_STAR_sin [simp]:
1.38       "(if even n then 0
1.39 -       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
1.40 +       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
1.41  by (induct "n", auto)
1.42
1.43  lemma lemma_STAR_cos [simp]:
1.44       "0 < n -->
1.45 -      (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
1.46 +      -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
1.47  by (induct "n", auto)
1.48
1.49  lemma lemma_STAR_cos1 [simp]:
1.50 @@ -532,7 +532,7 @@
1.51  by (induct "n", auto)
1.52
1.53  lemma lemma_STAR_cos2 [simp]:
1.54 -  "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) *  0 ^ n
1.55 +  "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n
1.56                           else 0) = 0"
1.57  apply (induct "n")
1.58  apply (case_tac [2] "n", auto)
1.59 @@ -543,13 +543,13 @@
1.60
1.61  lemma sin_converges:
1.62        "(%n. (if even n then 0
1.63 -            else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *
1.64 +            else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *
1.65                   x ^ n) sums sin(x)"
1.66  unfolding sin_def by (rule summable_sin [THEN summable_sums])
1.67
1.68  lemma cos_converges:
1.69        "(%n. (if even n then
1.70 -           (- 1) ^ (n div 2)/(real (fact n))
1.71 +           -1 ^ (n div 2)/(real (fact n))
1.72             else 0) * x ^ n) sums cos(x)"
1.73  unfolding cos_def by (rule summable_cos [THEN summable_sums])
1.74
1.75 @@ -566,9 +566,9 @@
1.76
1.77  lemma sin_fdiffs:
1.78        "diffs(%n. if even n then 0
1.79 -           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n)))
1.80 +           else -1 ^ ((n - Suc 0) div 2)/(real (fact n)))
1.81         = (%n. if even n then
1.82 -                 (- 1) ^ (n div 2)/(real (fact n))
1.83 +                 -1 ^ (n div 2)/(real (fact n))
1.84                else 0)"
1.85  by (auto intro!: ext
1.86           simp add: diffs_def divide_inverse real_of_nat_def
1.87 @@ -576,17 +576,17 @@
1.88
1.89  lemma sin_fdiffs2:
1.90         "diffs(%n. if even n then 0
1.91 -           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) n
1.92 +           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) n
1.93         = (if even n then
1.94 -                 (- 1) ^ (n div 2)/(real (fact n))
1.95 +                 -1 ^ (n div 2)/(real (fact n))
1.96                else 0)"
1.97  by (simp only: sin_fdiffs)
1.98
1.99  lemma cos_fdiffs:
1.100        "diffs(%n. if even n then
1.101 -                 (- 1) ^ (n div 2)/(real (fact n)) else 0)
1.102 +                 -1 ^ (n div 2)/(real (fact n)) else 0)
1.103         = (%n. - (if even n then 0
1.104 -           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))"
1.105 +           else -1 ^ ((n - Suc 0)div 2)/(real (fact n))))"
1.106  by (auto intro!: ext
1.107           simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
1.108           simp del: mult_Suc of_nat_Suc)
1.109 @@ -594,16 +594,16 @@
1.110
1.111  lemma cos_fdiffs2:
1.112        "diffs(%n. if even n then
1.113 -                 (- 1) ^ (n div 2)/(real (fact n)) else 0) n
1.114 +                 -1 ^ (n div 2)/(real (fact n)) else 0) n
1.115         = - (if even n then 0
1.116 -           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
1.117 +           else -1 ^ ((n - Suc 0)div 2)/(real (fact n)))"
1.118  by (simp only: cos_fdiffs)
1.119
1.120  text{*Now at last we can get the derivatives of exp, sin and cos*}
1.121
1.122  lemma lemma_sin_minus:
1.123       "- sin x = (\<Sum>n. - ((if even n then 0
1.124 -                  else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
1.125 +                  else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
1.126  by (auto intro!: sums_unique sums_minus sin_converges)
1.127
1.128  lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /# real (fact n))"
1.129 @@ -622,13 +622,13 @@
1.130  lemma lemma_sin_ext:
1.131       "sin = (%x. \<Sum>n.
1.132                     (if even n then 0
1.133 -                       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *
1.134 +                       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *
1.135                     x ^ n)"
1.136  by (auto intro!: ext simp add: sin_def)
1.137
1.138  lemma lemma_cos_ext:
1.139       "cos = (%x. \<Sum>n.
1.140 -                   (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) *
1.141 +                   (if even n then -1 ^ (n div 2)/(real (fact n)) else 0) *
1.142                     x ^ n)"
1.143  by (auto intro!: ext simp add: cos_def)
1.144
1.145 @@ -1003,7 +1003,7 @@
1.146  lemma cos_zero [simp]: "cos 0 = 1"
1.148  apply (rule sums_unique [symmetric])
1.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)
1.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)
1.151  apply auto
1.152  done
1.153
1.154 @@ -1243,12 +1243,12 @@
1.155     hence define pi.*}
1.156
1.157  lemma sin_paired:
1.158 -     "(%n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1))
1.159 +     "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1))
1.160        sums  sin x"
1.161  proof -
1.162    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
1.163              (if even k then 0
1.164 -             else (- 1) ^ ((k - Suc 0) div 2) / real (fact k)) *
1.165 +             else -1 ^ ((k - Suc 0) div 2) / real (fact k)) *
1.166              x ^ k)
1.167  	sums sin x"
1.168      unfolding sin_def
1.169 @@ -1259,8 +1259,8 @@
1.170  lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
1.171  apply (subgoal_tac
1.172         "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
1.173 -              (- 1) ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1))
1.174 -     sums (\<Sum>n. (- 1) ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
1.175 +              -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1))
1.176 +     sums (\<Sum>n. -1 ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
1.177   prefer 2
1.178   apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp)
1.179  apply (rotate_tac 2)
1.180 @@ -1312,10 +1312,10 @@
1.181  done
1.182
1.183  lemma cos_paired:
1.184 -     "(%n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
1.185 +     "(%n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
1.186  proof -
1.187    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
1.188 -            (if even k then (- 1) ^ (k div 2) / real (fact k) else 0) *
1.189 +            (if even k then -1 ^ (k div 2) / real (fact k) else 0) *
1.190              x ^ k)
1.191          sums cos x"
1.192      unfolding cos_def
1.193 @@ -1334,7 +1334,7 @@
1.194  apply (rule neg_less_iff_less [THEN iffD1])
1.195  apply (frule sums_unique, auto)
1.196  apply (rule_tac y =
1.197 - "\<Sum>n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
1.198 + "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
1.199         in order_less_trans)
1.200  apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
1.201  apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
```