--- a/src/HOL/Decision_Procs/Approximation.thy Fri Aug 19 23:25:47 2011 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Aug 19 23:48:18 2011 +0200
@@ -839,7 +839,8 @@
cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
+ (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
(is "_ = ?SUM + ?rest / ?fact * ?pow")
- using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`] by auto
+ using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
+ unfolding cos_coeff_def by auto
have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
also have "\<dots> = cos (t + n * pi)" using cos_add by auto
@@ -951,7 +952,8 @@
sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
+ (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
(is "_ = ?SUM + ?rest / ?fact * ?pow")
- using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`] by auto
+ using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
+ unfolding sin_coeff_def by auto
have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add left_distrib right_distrib by auto
moreover
@@ -959,7 +961,7 @@
hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le> - ?rest " by auto
- have "0 < ?fact" by (rule real_of_nat_fact_gt_zero)
+ have "0 < ?fact" by (simp del: fact_Suc)
have "0 < ?pow" using `0 < real x` by (rule zero_less_power)
{
--- a/src/HOL/Ln.thy Fri Aug 19 23:25:47 2011 +0200
+++ b/src/HOL/Ln.thy Fri Aug 19 23:48:18 2011 +0200
@@ -65,7 +65,7 @@
apply (rule mult_right_mono)
apply (subst inverse_eq_divide)
apply simp
- apply (rule inv_real_of_nat_fact_ge_zero)
+ apply (simp del: fact_Suc)
done
finally show ?thesis .
qed
--- a/src/HOL/MacLaurin.thy Fri Aug 19 23:25:47 2011 +0200
+++ b/src/HOL/MacLaurin.thy Fri Aug 19 23:48:18 2011 +0200
@@ -417,32 +417,33 @@
cos (x + real (m) * pi / 2)"
by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
+lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
+ unfolding sin_coeff_def by simp (* TODO: move *)
+
lemma Maclaurin_sin_expansion2:
"\<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)) *
- x ^ m)
+ (\<Sum>m=0..<n. sin_coeff 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
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
apply (simp (no_asm) add: sin_expansion_lemma)
-apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
+apply (force intro!: DERIV_intros)
+apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
+apply (cases n, simp, simp)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
done
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)) *
- x ^ m)
+ (\<Sum>m=0..<n. sin_coeff m * x ^ m)
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (insert Maclaurin_sin_expansion2 [of x n])
apply (blast intro: elim:)
@@ -452,44 +453,44 @@
"[| n > 0; 0 < x |] ==>
\<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)) *
- x ^ m)
+ (\<Sum>m=0..<n. sin_coeff 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)
apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
done
lemma Maclaurin_sin_expansion4:
"0 < x ==>
\<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)) *
- x ^ m)
+ (\<Sum>m=0..<n. sin_coeff 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)
apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
done
subsection{*Maclaurin Expansion for Cosine Function*}
+lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
+ unfolding cos_coeff_def by simp (* TODO: move *)
+
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"
+ "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
by (induct "n", auto)
lemma cos_expansion_lemma:
@@ -499,10 +500,7 @@
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))
- else 0) *
- x ^ m)
+ (\<Sum>m=0..<n. cos_coeff m * x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
apply safe
@@ -515,17 +513,14 @@
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
done
lemma Maclaurin_cos_expansion2:
"[| 0 < x; n > 0 |] ==>
\<exists>t. 0 < t & t < x &
cos x =
- (\<Sum>m=0..<n. (if even m
- then -1 ^ (m div 2)/(real (fact m))
- else 0) *
- x ^ m)
+ (\<Sum>m=0..<n. cos_coeff m * x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
@@ -534,17 +529,14 @@
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
done
lemma Maclaurin_minus_cos_expansion:
"[| x < 0; n > 0 |] ==>
\<exists>t. x < t & t < 0 &
cos x =
- (\<Sum>m=0..<n. (if even m
- then -1 ^ (m div 2)/(real (fact m))
- else 0) *
- x ^ m)
+ (\<Sum>m=0..<n. cos_coeff m * x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
apply safe
@@ -553,7 +545,7 @@
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
done
(* ------------------------------------------------------------------------- *)
@@ -565,8 +557,8 @@
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)) *
- x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
+ "abs(sin x - (\<Sum>m=0..<n. sin_coeff 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"
by (rule_tac mult_right_mono,simp_all)
@@ -592,6 +584,7 @@
apply (safe dest!: mod_eqD, simp_all)
done
show ?thesis
+ unfolding sin_coeff_def
apply (subst t2)
apply (rule sin_bound_lemma)
apply (rule setsum_cong[OF refl])
--- a/src/HOL/Transcendental.thy Fri Aug 19 23:25:47 2011 +0200
+++ b/src/HOL/Transcendental.thy Fri Aug 19 23:48:18 2011 +0200
@@ -618,23 +618,6 @@
qed
-subsection{* Some properties of factorials *}
-
-lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
-by auto
-
-lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
-by auto
-
-lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
-by simp
-
-lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
-by (auto simp add: positive_imp_inverse_positive)
-
-lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
-by (auto intro: order_less_imp_le)
-
subsection {* Derivability of power series *}
lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
@@ -820,9 +803,8 @@
subsection {* Exponential Function *}
-definition
- exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
- "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
+definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
+ "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
lemma summable_exp_generic:
fixes x :: "'a::{real_normed_algebra_1,banach}"
@@ -880,14 +862,10 @@
lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
by (simp add: diffs_def)
-lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
-by (auto simp add: exp_def)
-
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
-apply (simp add: exp_def)
-apply (subst lemma_exp_ext)
-apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)")
-apply (rule_tac [2] K = "of_real (1 + norm x)" in termdiffs)
+unfolding exp_def scaleR_conv_of_real
+apply (rule DERIV_cong)
+apply (rule termdiffs [where K="of_real (1 + norm x)"])
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
apply (simp del: of_real_add)
@@ -1100,120 +1078,93 @@
subsection {* Natural Logarithm *}
-definition
- ln :: "real => real" where
+definition ln :: "real \<Rightarrow> real" where
"ln x = (THE u. exp u = x)"
lemma ln_exp [simp]: "ln (exp x) = x"
-by (simp add: ln_def)
+ by (simp add: ln_def)
lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
-by (auto dest: exp_total)
+ by (auto dest: exp_total)
lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
-apply (rule iffI)
-apply (erule subst, rule exp_gt_zero)
-apply (erule exp_ln)
-done
+ by (metis exp_gt_zero exp_ln)
lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
-by (erule subst, rule ln_exp)
+ by (erule subst, rule ln_exp)
lemma ln_one [simp]: "ln 1 = 0"
-by (rule ln_unique, simp)
+ by (rule ln_unique, simp)
lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y"
-by (rule ln_unique, simp add: exp_add)
+ by (rule ln_unique, simp add: exp_add)
lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
-by (rule ln_unique, simp add: exp_minus)
+ by (rule ln_unique, simp add: exp_minus)
lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x - ln y"
-by (rule ln_unique, simp add: exp_diff)
+ by (rule ln_unique, simp add: exp_diff)
lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
-by (rule ln_unique, simp add: exp_real_of_nat_mult)
+ by (rule ln_unique, simp add: exp_real_of_nat_mult)
lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
-by (subst exp_less_cancel_iff [symmetric], simp)
+ by (subst exp_less_cancel_iff [symmetric], simp)
lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
-by (simp add: linorder_not_less [symmetric])
+ by (simp add: linorder_not_less [symmetric])
lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
-by (simp add: order_eq_iff)
+ by (simp add: order_eq_iff)
lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
-apply (rule exp_le_cancel_iff [THEN iffD1])
-apply (simp add: exp_ge_add_one_self_aux)
-done
+ apply (rule exp_le_cancel_iff [THEN iffD1])
+ apply (simp add: exp_ge_add_one_self_aux)
+ done
lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
-by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
-
-lemma ln_ge_zero [simp]:
- assumes x: "1 \<le> x" shows "0 \<le> ln x"
-proof -
- have "0 < x" using x by arith
- hence "exp 0 \<le> exp (ln x)"
- by (simp add: x)
- thus ?thesis by (simp only: exp_le_cancel_iff)
-qed
-
-lemma ln_ge_zero_imp_ge_one:
- assumes ln: "0 \<le> ln x"
- and x: "0 < x"
- shows "1 \<le> x"
-proof -
- from ln have "ln 1 \<le> ln x" by simp
- thus ?thesis by (simp add: x del: ln_one)
-qed
-
-lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
-by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
-
-lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
-by (insert ln_ge_zero_iff [of x], arith)
-
-lemma ln_gt_zero:
- assumes x: "1 < x" shows "0 < ln x"
-proof -
- have "0 < x" using x by arith
- hence "exp 0 < exp (ln x)" by (simp add: x)
- thus ?thesis by (simp only: exp_less_cancel_iff)
-qed
-
-lemma ln_gt_zero_imp_gt_one:
- assumes ln: "0 < ln x"
- and x: "0 < x"
- shows "1 < x"
-proof -
- from ln have "ln 1 < ln x" by simp
- thus ?thesis by (simp add: x del: ln_one)
-qed
-
-lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
-by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
-
-lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
-by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
-
-lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
-by simp
+ by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
+
+lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
+ using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_ge_zero_imp_ge_one: "\<lbrakk>0 \<le> ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 \<le> x"
+ using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> (0 \<le> ln x) = (1 \<le> x)"
+ using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x < 0) = (x < 1)"
+ using ln_less_cancel_iff [of x 1] by simp
+
+lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
+ using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_gt_zero_imp_gt_one: "\<lbrakk>0 < ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x"
+ using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> (0 < ln x) = (1 < x)"
+ using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x = 0) = (x = 1)"
+ using ln_inj_iff [of x 1] by simp
+
+lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0"
+ by simp
lemma exp_ln_eq: "exp u = x ==> ln x = u"
-by auto
+ by (rule ln_unique) (* TODO: delete *)
lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
-apply (subgoal_tac "isCont ln (exp (ln x))", simp)
-apply (rule isCont_inverse_function [where f=exp], simp_all)
-done
+ apply (subgoal_tac "isCont ln (exp (ln x))", simp)
+ apply (rule isCont_inverse_function [where f=exp], simp_all)
+ done
lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
-apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
-apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
-apply (simp_all add: abs_if isCont_ln)
-done
+ apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
+ apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
+ apply (simp_all add: abs_if isCont_ln)
+ done
lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
@@ -1253,60 +1204,30 @@
subsection {* Sine and Cosine *}
-definition
- sin_coeff :: "nat \<Rightarrow> real" where
+definition sin_coeff :: "nat \<Rightarrow> real" where
"sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
-definition
- cos_coeff :: "nat \<Rightarrow> real" where
+definition cos_coeff :: "nat \<Rightarrow> real" where
"cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
-definition
- sin :: "real => real" where
- "sin x = (\<Sum>n. sin_coeff n * x ^ n)"
-
-definition
- cos :: "real => real" where
- "cos x = (\<Sum>n. cos_coeff n * x ^ n)"
+definition sin :: "real \<Rightarrow> real" where
+ "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
+
+definition cos :: "real \<Rightarrow> real" where
+ "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
unfolding sin_coeff_def
-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)
+apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done
lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
unfolding cos_coeff_def
-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)
+apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done
-lemma lemma_STAR_sin:
- "(if even n then 0
- else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos:
- "0 < n -->
- -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos1:
- "0 < n -->
- (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos2:
- "(\<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)
-done
-
lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
unfolding sin_def by (rule summable_sin [THEN summable_sums])
@@ -1336,22 +1257,15 @@
lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))"
by (auto intro!: sums_unique sums_minus sin_converges)
-lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
- by (auto simp add: sin_def)
-
-lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
- by (auto simp add: cos_def)
-
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
-apply (simp add: cos_def)
-apply (subst lemma_sin_ext)
+unfolding sin_def cos_def
apply (auto simp add: sin_fdiffs2 [symmetric])
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
done
lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
-apply (subst lemma_cos_ext)
+unfolding cos_def
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
@@ -1378,196 +1292,122 @@
lemma cos_zero [simp]: "cos 0 = 1"
unfolding cos_def cos_coeff_def by (simp add: powser_zero)
-lemma DERIV_sin_sin_mult [simp]:
- "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"
-by (rule DERIV_mult, auto)
-
-lemma DERIV_sin_sin_mult2 [simp]:
- "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
-apply (cut_tac x = x in DERIV_sin_sin_mult)
-apply (auto simp add: mult_assoc)
-done
-
-lemma DERIV_sin_realpow2 [simp]:
- "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
-
-lemma DERIV_sin_realpow2a [simp]:
- "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2)
-
-lemma DERIV_cos_cos_mult [simp]:
- "DERIV (%x. cos(x)*cos(x)) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
-by (rule DERIV_mult, auto)
-
-lemma DERIV_cos_cos_mult2 [simp]:
- "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
-apply (cut_tac x = x in DERIV_cos_cos_mult)
-apply (auto simp add: mult_ac)
-done
-
-lemma DERIV_cos_realpow2 [simp]:
- "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
-by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
-
-lemma DERIV_cos_realpow2a [simp]:
- "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2)
-
lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
-by auto
-
-lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
- by (auto intro!: DERIV_intros)
-
-(* most useful *)
-lemma DERIV_cos_cos_mult3 [simp]:
- "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
- by (auto intro!: DERIV_intros)
-
-lemma DERIV_sin_circle_all:
- "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
- (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
- by (auto intro!: DERIV_intros)
-
-lemma DERIV_sin_circle_all_zero [simp]:
- "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
-by (cut_tac DERIV_sin_circle_all, auto)
-
-lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
-apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all])
-apply (auto simp add: numeral_2_eq_2)
-done
-
-lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
-apply (subst add_commute)
-apply (rule sin_cos_squared_add)
-done
+ by (rule DERIV_cong) (* TODO: delete *)
+
+lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
+proof -
+ have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
+ by (auto intro!: DERIV_intros)
+ hence "(sin x)\<twosuperior> + (cos x)\<twosuperior> = (sin 0)\<twosuperior> + (cos 0)\<twosuperior>"
+ by (rule DERIV_isconst_all)
+ thus "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1" by simp
+qed
+
+lemma sin_cos_squared_add2 [simp]: "(cos x)\<twosuperior> + (sin x)\<twosuperior> = 1"
+ by (subst add_commute, rule sin_cos_squared_add)
lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
-apply (cut_tac x = x in sin_cos_squared_add2)
-apply (simp add: power2_eq_square)
-done
+ using sin_cos_squared_add2 [unfolded power2_eq_square] .
lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
-apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
-apply simp
-done
+ unfolding eq_diff_eq by (rule sin_cos_squared_add)
lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
-apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
-apply simp
-done
+ unfolding eq_diff_eq by (rule sin_cos_squared_add2)
lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
-by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
+ by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
-apply (insert abs_sin_le_one [of x])
-apply (simp add: abs_le_iff del: abs_sin_le_one)
-done
+ using abs_sin_le_one [of x] unfolding abs_le_iff by simp
lemma sin_le_one [simp]: "sin x \<le> 1"
-apply (insert abs_sin_le_one [of x])
-apply (simp add: abs_le_iff del: abs_sin_le_one)
-done
+ using abs_sin_le_one [of x] unfolding abs_le_iff by simp
lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
-by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
+ by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
-apply (insert abs_cos_le_one [of x])
-apply (simp add: abs_le_iff del: abs_cos_le_one)
-done
+ using abs_cos_le_one [of x] unfolding abs_le_iff by simp
lemma cos_le_one [simp]: "cos x \<le> 1"
-apply (insert abs_cos_le_one [of x])
-apply (simp add: abs_le_iff del: abs_cos_le_one)
-done
+ using abs_cos_le_one [of x] unfolding abs_le_iff by simp
lemma DERIV_fun_pow: "DERIV g x :> m ==>
DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
unfolding One_nat_def
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
apply (rule DERIV_pow, auto)
done
lemma DERIV_fun_exp:
"DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
apply (rule_tac f = exp in DERIV_chain2)
apply (rule DERIV_exp, auto)
done
lemma DERIV_fun_sin:
"DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
apply (rule_tac f = sin in DERIV_chain2)
apply (rule DERIV_sin, auto)
done
lemma DERIV_fun_cos:
"DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
apply (rule_tac f = cos in DERIV_chain2)
apply (rule DERIV_cos, auto)
done
-(* lemma *)
-lemma lemma_DERIV_sin_cos_add:
- "\<forall>x.
- DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
- (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
- by (auto intro!: DERIV_intros simp add: algebra_simps)
-
-lemma sin_cos_add [simp]:
+lemma sin_cos_add_lemma:
"(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
(cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
-apply (cut_tac y = 0 and x = x and y7 = y
- in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
-apply (auto simp add: numeral_2_eq_2)
-done
+ (is "?f x = 0")
+proof -
+ have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
+ by (auto intro!: DERIV_intros simp add: algebra_simps)
+ hence "?f x = ?f 0"
+ by (rule DERIV_isconst_all)
+ thus ?thesis by simp
+qed
lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
-apply (cut_tac x = x and y = y in sin_cos_add)
-apply (simp del: sin_cos_add)
-done
+ using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
-apply (cut_tac x = x and y = y in sin_cos_add)
-apply (simp del: sin_cos_add)
-done
-
-lemma lemma_DERIV_sin_cos_minus:
- "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
- by (auto intro!: DERIV_intros simp add: algebra_simps)
-
-
-lemma sin_cos_minus:
- "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
-apply (cut_tac y = 0 and x = x
- in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
-apply simp
-done
+ using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
+
+lemma sin_cos_minus_lemma:
+ "(sin(-x) + sin(x))\<twosuperior> + (cos(-x) - cos(x))\<twosuperior> = 0" (is "?f x = 0")
+proof -
+ have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
+ by (auto intro!: DERIV_intros simp add: algebra_simps)
+ hence "?f x = ?f 0"
+ by (rule DERIV_isconst_all)
+ thus ?thesis by simp
+qed
lemma sin_minus [simp]: "sin (-x) = -sin(x)"
- using sin_cos_minus [where x=x] by simp
+ using sin_cos_minus_lemma [where x=x] by simp
lemma cos_minus [simp]: "cos (-x) = cos(x)"
- using sin_cos_minus [where x=x] by simp
+ using sin_cos_minus_lemma [where x=x] by simp
lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
-by (simp add: diff_minus sin_add)
+ by (simp add: diff_minus sin_add)
lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
-by (simp add: sin_diff mult_commute)
+ by (simp add: sin_diff mult_commute)
lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
-by (simp add: diff_minus cos_add)
+ by (simp add: diff_minus cos_add)
lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
-by (simp add: cos_diff mult_commute)
+ by (simp add: cos_diff mult_commute)
lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
using sin_add [where x=x and y=x] by simp
@@ -1579,8 +1419,7 @@
subsection {* The Constant Pi *}
-definition
- pi :: "real" where
+definition pi :: "real" where
"pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
@@ -1701,7 +1540,8 @@
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
del: fact_Suc)
apply (rule real_mult_inverse_cancel2)
-apply (rule real_of_nat_fact_gt_zero)+
+apply (simp del: fact_Suc)
+apply (simp del: fact_Suc)
apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
apply (subst fact_lemma)
apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
@@ -2467,7 +2307,7 @@
lemma DERIV_arcsin:
"\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
-apply (rule lemma_DERIV_subst [OF DERIV_sin])
+apply (rule DERIV_cong [OF DERIV_sin])
apply (simp add: cos_arcsin)
apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
apply (rule power_strict_mono, simp, simp, simp)
@@ -2480,7 +2320,7 @@
lemma DERIV_arccos:
"\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<twosuperior>))"
apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
-apply (rule lemma_DERIV_subst [OF DERIV_cos])
+apply (rule DERIV_cong [OF DERIV_cos])
apply (simp add: sin_arccos)
apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
apply (rule power_strict_mono, simp, simp, simp)
@@ -2492,7 +2332,7 @@
lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<twosuperior>)"
apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
-apply (rule lemma_DERIV_subst [OF DERIV_tan])
+apply (rule DERIV_cong [OF DERIV_tan])
apply (rule cos_arctan_not_zero)
apply (simp add: power_inverse tan_sec [symmetric])
apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp)
@@ -2581,8 +2421,8 @@
lemma tan_60: "tan (pi / 3) = sqrt 3"
unfolding tan_def by (simp add: sin_60 cos_60)
-lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
- by (auto intro!: DERIV_intros)
+lemma DERIV_sin_add: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
+ by (auto intro!: DERIV_intros) (* TODO: delete *)
lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
proof -