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.147  apply (simp add: cos_def)
   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)