--- 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)
--- 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)
--- 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)