src/HOL/Transcendental.thy
changeset 56479 91958d4b30f7
parent 56409 36489d77c484
child 56483 5b82c58b665c
     1.1 --- a/src/HOL/Transcendental.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Apr 09 09:37:47 2014 +0200
     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: divide_minus_left odd_Suc_mult_two_ex)
     1.8 +  by (simp del: mult_Suc, auto simp add: 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: divide_minus_left diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
    1.17 +  by (simp add: 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 simp: divide_minus_left)
    1.26 +      by (intro image_eqI[where x="arcsin x"]) auto
    1.27    qed simp
    1.28    finally show ?thesis .
    1.29  qed
    1.30 @@ -3338,14 +3338,12 @@
    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 divide_minus_left 
    1.35 -           simp del: less_divide_eq_numeral1
    1.36 +     (auto simp: le_less eventually_at dist_real_def 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 divide_minus_left 
    1.42 -           simp del: less_divide_eq_numeral1
    1.43 +     (auto simp: le_less eventually_at dist_real_def 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 @@ -3967,7 +3965,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: divide_minus_left tan_def cos_arctan sin_arctan sin_diff cos_diff)
    1.52 +    by (simp add: 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")