1.1 --- a/src/HOL/Transcendental.thy Tue Jun 30 18:16:22 2009 +0200
1.2 +++ b/src/HOL/Transcendental.thy Tue Jun 30 18:21:55 2009 +0200
1.3 @@ -784,9 +784,8 @@
1.4 also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
1.5 finally show ?thesis .
1.6 qed }
1.7 - { fix n
1.8 - from DERIV_pow[of "Suc n" x0, THEN DERIV_cmult[where c="f n"]]
1.9 - show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" unfolding real_mult_assoc by auto }
1.10 + { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
1.11 + by (auto intro!: DERIV_intros simp del: power_Suc) }
1.12 { fix x assume "x \<in> {-R' <..< R'}" hence "R' \<in> {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto
1.13 have "summable (\<lambda> n. f n * x^n)"
1.14 proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI)
1.15 @@ -1416,24 +1415,17 @@
1.16 by auto
1.17
1.18 lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
1.19 -apply (rule lemma_DERIV_subst)
1.20 -apply (rule DERIV_cos_realpow2a, auto)
1.21 -done
1.22 + by (auto intro!: DERIV_intros)
1.23
1.24 (* most useful *)
1.25 lemma DERIV_cos_cos_mult3 [simp]:
1.26 "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
1.27 -apply (rule lemma_DERIV_subst)
1.28 -apply (rule DERIV_cos_cos_mult2, auto)
1.29 -done
1.30 + by (auto intro!: DERIV_intros)
1.31
1.32 lemma DERIV_sin_circle_all:
1.33 "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
1.34 (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
1.35 -apply (simp only: diff_minus, safe)
1.36 -apply (rule DERIV_add)
1.37 -apply (auto simp add: numeral_2_eq_2)
1.38 -done
1.39 + by (auto intro!: DERIV_intros)
1.40
1.41 lemma DERIV_sin_circle_all_zero [simp]:
1.42 "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
1.43 @@ -1524,11 +1516,7 @@
1.44 "\<forall>x.
1.45 DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
1.46 (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
1.47 -apply (safe, rule lemma_DERIV_subst)
1.48 -apply (best intro!: DERIV_intros intro: DERIV_chain2)
1.49 - --{*replaces the old @{text DERIV_tac}*}
1.50 -apply (auto simp add: algebra_simps)
1.51 -done
1.52 + by (auto intro!: DERIV_intros simp add: algebra_simps)
1.53
1.54 lemma sin_cos_add [simp]:
1.55 "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
1.56 @@ -1550,10 +1538,8 @@
1.57
1.58 lemma lemma_DERIV_sin_cos_minus:
1.59 "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
1.60 -apply (safe, rule lemma_DERIV_subst)
1.61 -apply (best intro!: DERIV_intros intro: DERIV_chain2)
1.62 -apply (simp add: algebra_simps)
1.63 -done
1.64 + by (auto intro!: DERIV_intros simp add: algebra_simps)
1.65 +
1.66
1.67 lemma sin_cos_minus:
1.68 "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
1.69 @@ -2121,10 +2107,7 @@
1.70
1.71 lemma lemma_DERIV_tan:
1.72 "cos x \<noteq> 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\<twosuperior>)"
1.73 -apply (rule lemma_DERIV_subst)
1.74 -apply (best intro!: DERIV_intros intro: DERIV_chain2)
1.75 -apply (auto simp add: divide_inverse numeral_2_eq_2)
1.76 -done
1.77 + by (auto intro!: DERIV_intros simp add: field_simps numeral_2_eq_2)
1.78
1.79 lemma DERIV_tan [simp]: "cos x \<noteq> 0 ==> DERIV tan x :> inverse((cos x)\<twosuperior>)"
1.80 by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
1.81 @@ -2594,11 +2577,7 @@
1.82 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
1.83
1.84 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
1.85 -apply (rule lemma_DERIV_subst)
1.86 -apply (rule_tac f = sin and g = "%x. x + k" in DERIV_chain2)
1.87 -apply (best intro!: DERIV_intros intro: DERIV_chain2)+
1.88 -apply (simp (no_asm))
1.89 -done
1.90 + by (auto intro!: DERIV_intros)
1.91
1.92 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
1.93 proof -
1.94 @@ -2639,11 +2618,7 @@
1.95 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
1.96
1.97 lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
1.98 -apply (rule lemma_DERIV_subst)
1.99 -apply (rule_tac f = cos and g = "%x. x + k" in DERIV_chain2)
1.100 -apply (best intro!: DERIV_intros intro: DERIV_chain2)+
1.101 -apply (simp (no_asm))
1.102 -done
1.103 + by (auto intro!: DERIV_intros)
1.104
1.105 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
1.106 by (auto simp add: sin_zero_iff even_mult_two_ex)