src/HOL/Transcendental.thy
 changeset 56409 36489d77c484 parent 56381 0556204bc230 child 56479 91958d4b30f7
```     1.1 --- a/src/HOL/Transcendental.thy	Fri Apr 04 16:43:47 2014 +0200
1.2 +++ b/src/HOL/Transcendental.thy	Thu Apr 03 23:51:52 2014 +0100
1.3 @@ -2145,7 +2145,7 @@
1.4
1.5  lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
1.6    unfolding cos_coeff_def sin_coeff_def
1.7 -  by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
1.8 +  by (simp del: mult_Suc, auto simp add: divide_minus_left odd_Suc_mult_two_ex)
1.9
1.10  lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
1.11    unfolding sin_coeff_def
1.12 @@ -2169,7 +2169,7 @@
1.13    by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
1.14
1.15  lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
1.16 -  by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
1.17 +  by (simp add: divide_minus_left diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
1.18
1.19  text{*Now at last we can get the derivatives of exp, sin and cos*}
1.20
1.21 @@ -3239,7 +3239,7 @@
1.22      assume "x \<in> {-1..1}"
1.23      then show "x \<in> sin ` {- pi / 2..pi / 2}"
1.24        using arcsin_lbound arcsin_ubound
1.25 -      by (intro image_eqI[where x="arcsin x"]) auto
1.26 +      by (intro image_eqI[where x="arcsin x"]) (auto simp: divide_minus_left)
1.27    qed simp
1.28    finally show ?thesis .
1.29  qed
1.30 @@ -3338,12 +3338,14 @@
1.31
1.32  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
1.33    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
1.34 -     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
1.35 +     (auto simp: le_less eventually_at dist_real_def divide_minus_left
1.36 +           simp del: less_divide_eq_numeral1
1.37             intro!: tan_monotone exI[of _ "pi/2"])
1.38
1.39  lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
1.40    by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
1.41 -     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
1.42 +     (auto simp: le_less eventually_at dist_real_def divide_minus_left
1.43 +           simp del: less_divide_eq_numeral1
1.44             intro!: tan_monotone exI[of _ "pi/2"])
1.45
1.46  lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
1.47 @@ -3965,7 +3967,7 @@
1.48    show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
1.49      unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
1.50      unfolding sgn_real_def
1.51 -    by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
1.52 +    by (simp add: divide_minus_left tan_def cos_arctan sin_arctan sin_diff cos_diff)
1.53  qed
1.54
1.55  theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")
```