# HG changeset patch
# User huffman
# Date 1180645336 -7200
# Node ID 3004310c95b153298b63dc7e1b4240aa22b86c80
# Parent  40a760921d94a7f81412383725d1c422892af0f3
replace (- 1) with -1

diff -r 40a760921d94 -r 3004310c95b1 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Thu May 31 22:23:50 2007 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu May 31 23:02:16 2007 +0200
@@ -421,7 +421,7 @@
 
 lemma HFinite_sin [simp]:
      "sumhr (0, whn, %n. (if even(n) then 0 else  
-              ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
+              (-1 ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
               \<in> HFinite"
 unfolding sumhr_app
 apply (simp only: star_zero_def starfun2_star_of)
@@ -447,7 +447,7 @@
 
 lemma HFinite_cos [simp]:
      "sumhr (0, whn, %n. (if even(n) then  
-            ((- 1) ^ (n div 2))/(real (fact n)) else  
+            (-1 ^ (n div 2))/(real (fact n)) else  
             0) * x ^ n) \<in> HFinite"
 unfolding sumhr_app
 apply (simp only: star_zero_def starfun2_star_of)
diff -r 40a760921d94 -r 3004310c95b1 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Thu May 31 22:23:50 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Thu May 31 23:02:16 2007 +0200
@@ -243,7 +243,7 @@
               (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
               diff n t / real (fact n) * h ^ n"
 apply (cut_tac f = "%x. f (-x)"
-        and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
+        and diff = "%n x. (-1 ^ n) * diff n (-x)"
         and h = "-h" and n = n in Maclaurin_objl)
 apply (simp)
 apply safe
@@ -412,7 +412,7 @@
      "\<exists>t. abs t \<le> abs x &
        sin x =
        (\<Sum>m=0..<n. (if even m then 0
-                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
                        x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = sin and n = n and x = x
@@ -432,7 +432,7 @@
 lemma Maclaurin_sin_expansion:
      "\<exists>t. sin x =
        (\<Sum>m=0..<n. (if even m then 0
-                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
                        x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (insert Maclaurin_sin_expansion2 [of x n]) 
@@ -446,7 +446,7 @@
        \<exists>t. 0 < t & t < x &
        sin x =
        (\<Sum>m=0..<n. (if even m then 0
-                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
                        x ^ m)
       + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
 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)
@@ -464,7 +464,7 @@
        \<exists>t. 0 < t & t \<le> x &
        sin x =
        (\<Sum>m=0..<n. (if even m then 0
-                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
                        x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 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)
@@ -482,14 +482,14 @@
 
 lemma sumr_cos_zero_one [simp]:
  "(\<Sum>m=0..<(Suc n).
-     (if even m then (- 1) ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
+     (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
 by (induct "n", auto)
 
 lemma Maclaurin_cos_expansion:
      "\<exists>t. abs t \<le> abs x &
        cos x =
        (\<Sum>m=0..<n. (if even m
-                       then (- 1) ^ (m div 2)/(real (fact m))
+                       then -1 ^ (m div 2)/(real (fact m))
                        else 0) *
                        x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
@@ -512,7 +512,7 @@
        \<exists>t. 0 < t & t < x &
        cos x =
        (\<Sum>m=0..<n. (if even m
-                       then (- 1) ^ (m div 2)/(real (fact m))
+                       then -1 ^ (m div 2)/(real (fact m))
                        else 0) *
                        x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
@@ -531,7 +531,7 @@
        \<exists>t. x < t & t < 0 &
        cos x =
        (\<Sum>m=0..<n. (if even m
-                       then (- 1) ^ (m div 2)/(real (fact m))
+                       then -1 ^ (m div 2)/(real (fact m))
                        else 0) *
                        x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
@@ -554,7 +554,7 @@
 by auto
 
 lemma Maclaurin_sin_bound:
-  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
 proof -
   have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
@@ -576,7 +576,7 @@
       ?diff n t / real (fact n) * x ^ n" by fast
   have diff_m_0:
     "\<And>m. ?diff m 0 = (if even m then 0
-         else (- 1) ^ ((m - Suc 0) div 2))"
+         else -1 ^ ((m - Suc 0) div 2))"
     apply (subst even_even_mod_4_iff)
     apply (cut_tac m=m in mod_exhaust_less_4)
     apply (elim disjE, simp_all)
diff -r 40a760921d94 -r 3004310c95b1 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 22:23:50 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 23:02:16 2007 +0200
@@ -444,11 +444,11 @@
 definition
   sin :: "real => real" where
   "sin x = (\<Sum>n. (if even(n) then 0 else
-             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
+             (-1 ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
  
 definition
   cos :: "real => real" where
-  "cos x = (\<Sum>n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
+  "cos x = (\<Sum>n. (if even(n) then (-1 ^ (n div 2))/(real (fact n)) 
                             else 0) * x ^ n)"
 
 lemma summable_exp_generic:
@@ -498,7 +498,7 @@
 lemma summable_sin: 
      "summable (%n.  
            (if even n then 0  
-           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
+           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
                 x ^ n)"
 apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
 apply (rule_tac [2] summable_exp)
@@ -509,7 +509,7 @@
 lemma summable_cos: 
       "summable (%n.  
            (if even n then  
-           (- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
+           -1 ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
 apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
 apply (rule_tac [2] summable_exp)
 apply (rule_tac x = 0 in exI)
@@ -518,12 +518,12 @@
 
 lemma lemma_STAR_sin [simp]:
      "(if even n then 0  
-       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
+       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
 by (induct "n", auto)
 
 lemma lemma_STAR_cos [simp]:
      "0 < n -->  
-      (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
+      -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
 by (induct "n", auto)
 
 lemma lemma_STAR_cos1 [simp]:
@@ -532,7 +532,7 @@
 by (induct "n", auto)
 
 lemma lemma_STAR_cos2 [simp]:
-  "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) *  0 ^ n 
+  "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n 
                          else 0) = 0"
 apply (induct "n")
 apply (case_tac [2] "n", auto)
@@ -543,13 +543,13 @@
 
 lemma sin_converges: 
       "(%n. (if even n then 0  
-            else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
+            else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
                  x ^ n) sums sin(x)"
 unfolding sin_def by (rule summable_sin [THEN summable_sums])
 
 lemma cos_converges: 
       "(%n. (if even n then  
-           (- 1) ^ (n div 2)/(real (fact n))  
+           -1 ^ (n div 2)/(real (fact n))  
            else 0) * x ^ n) sums cos(x)"
 unfolding cos_def by (rule summable_cos [THEN summable_sums])
 
@@ -566,9 +566,9 @@
 
 lemma sin_fdiffs: 
       "diffs(%n. if even n then 0  
-           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n)))  
+           else -1 ^ ((n - Suc 0) div 2)/(real (fact n)))  
        = (%n. if even n then  
-                 (- 1) ^ (n div 2)/(real (fact n))  
+                 -1 ^ (n div 2)/(real (fact n))  
               else 0)"
 by (auto intro!: ext 
          simp add: diffs_def divide_inverse real_of_nat_def
@@ -576,17 +576,17 @@
 
 lemma sin_fdiffs2: 
        "diffs(%n. if even n then 0  
-           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) n  
+           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) n  
        = (if even n then  
-                 (- 1) ^ (n div 2)/(real (fact n))  
+                 -1 ^ (n div 2)/(real (fact n))  
               else 0)"
 by (simp only: sin_fdiffs)
 
 lemma cos_fdiffs: 
       "diffs(%n. if even n then  
-                 (- 1) ^ (n div 2)/(real (fact n)) else 0)  
+                 -1 ^ (n div 2)/(real (fact n)) else 0)  
        = (%n. - (if even n then 0  
-           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))"
+           else -1 ^ ((n - Suc 0)div 2)/(real (fact n))))"
 by (auto intro!: ext 
          simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
          simp del: mult_Suc of_nat_Suc)
@@ -594,16 +594,16 @@
 
 lemma cos_fdiffs2: 
       "diffs(%n. if even n then  
-                 (- 1) ^ (n div 2)/(real (fact n)) else 0) n 
+                 -1 ^ (n div 2)/(real (fact n)) else 0) n 
        = - (if even n then 0  
-           else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
+           else -1 ^ ((n - Suc 0)div 2)/(real (fact n)))"
 by (simp only: cos_fdiffs)
 
 text{*Now at last we can get the derivatives of exp, sin and cos*}
 
 lemma lemma_sin_minus:
      "- sin x = (\<Sum>n. - ((if even n then 0 
-                  else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
+                  else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
 by (auto intro!: sums_unique sums_minus sin_converges)
 
 lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /# real (fact n))"
@@ -622,13 +622,13 @@
 lemma lemma_sin_ext:
      "sin = (%x. \<Sum>n. 
                    (if even n then 0  
-                       else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
+                       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
                    x ^ n)"
 by (auto intro!: ext simp add: sin_def)
 
 lemma lemma_cos_ext:
      "cos = (%x. \<Sum>n. 
-                   (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) *
+                   (if even n then -1 ^ (n div 2)/(real (fact n)) else 0) *
                    x ^ n)"
 by (auto intro!: ext simp add: cos_def)
 
@@ -1003,7 +1003,7 @@
 lemma cos_zero [simp]: "cos 0 = 1"
 apply (simp add: cos_def)
 apply (rule sums_unique [symmetric])
-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)
+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)
 apply auto
 done
 
@@ -1243,12 +1243,12 @@
    hence define pi.*}
 
 lemma sin_paired:
-     "(%n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
+     "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
       sums  sin x"
 proof -
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
             (if even k then 0
-             else (- 1) ^ ((k - Suc 0) div 2) / real (fact k)) *
+             else -1 ^ ((k - Suc 0) div 2) / real (fact k)) *
             x ^ k) 
 	sums sin x"
     unfolding sin_def
@@ -1259,8 +1259,8 @@
 lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
 apply (subgoal_tac 
        "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
-              (- 1) ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1)) 
-     sums (\<Sum>n. (- 1) ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
+              -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1)) 
+     sums (\<Sum>n. -1 ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
  prefer 2
  apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp) 
 apply (rotate_tac 2)
@@ -1312,10 +1312,10 @@
 done
 
 lemma cos_paired:
-     "(%n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
+     "(%n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
 proof -
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
-            (if even k then (- 1) ^ (k div 2) / real (fact k) else 0) *
+            (if even k then -1 ^ (k div 2) / real (fact k) else 0) *
             x ^ k) 
         sums cos x"
     unfolding cos_def
@@ -1334,7 +1334,7 @@
 apply (rule neg_less_iff_less [THEN iffD1]) 
 apply (frule sums_unique, auto)
 apply (rule_tac y =
- "\<Sum>n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
+ "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
        in order_less_trans)
 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
 apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)