src/HOL/Transcendental.thy
changeset 54230 b1d955791529
parent 53602 0ae3db699a3e
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Transcendental.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -453,7 +453,7 @@
     1.4    apply simp
     1.5    apply (simp only: lemma_termdiff1 setsum_right_distrib)
     1.6    apply (rule setsum_cong [OF refl])
     1.7 -  apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
     1.8 +  apply (simp add: less_iff_Suc_add)
     1.9    apply (clarify)
    1.10    apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
    1.11                del: setsum_op_ivl_Suc power_Suc)
    1.12 @@ -1129,8 +1129,7 @@
    1.13    by (rule inverse_unique [symmetric], simp add: mult_exp_exp)
    1.14  
    1.15  lemma exp_diff: "exp (x - y) = exp x / exp y"
    1.16 -  unfolding diff_minus divide_inverse
    1.17 -  by (simp add: exp_add exp_minus)
    1.18 +  using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
    1.19  
    1.20  
    1.21  subsubsection {* Properties of the Exponential Function on Reals *}
    1.22 @@ -2410,13 +2409,13 @@
    1.23    using sin_cos_minus_lemma [where x=x] by simp
    1.24  
    1.25  lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
    1.26 -  by (simp add: diff_minus sin_add)
    1.27 +  using sin_add [of x "- y"] by simp
    1.28  
    1.29  lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
    1.30    by (simp add: sin_diff mult_commute)
    1.31  
    1.32  lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
    1.33 -  by (simp add: diff_minus cos_add)
    1.34 +  using cos_add [of x "- y"] by simp
    1.35  
    1.36  lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
    1.37    by (simp add: cos_diff mult_commute)
    1.38 @@ -2526,8 +2525,9 @@
    1.39          by (simp add: inverse_eq_divide less_divide_eq)
    1.40      }
    1.41      note *** = this
    1.42 +    have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
    1.43      from ** show ?thesis by (rule sumr_pos_lt_pair)
    1.44 -      (simp add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] ***)
    1.45 +      (simp add: divide_inverse mult_assoc [symmetric] ***)
    1.46    qed
    1.47    ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
    1.48      by (rule order_less_trans)
    1.49 @@ -2810,7 +2810,7 @@
    1.50  apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
    1.51  apply (force simp add: minus_equation_iff [of x])
    1.52  apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
    1.53 -apply (auto simp add: cos_add)
    1.54 +apply (auto simp add: cos_diff cos_add)
    1.55  done
    1.56  
    1.57  (* ditto: but to a lesser extent *)
    1.58 @@ -3833,7 +3833,7 @@
    1.59                by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
    1.60              from DERIV_add_minus[OF this DERIV_arctan]
    1.61              show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
    1.62 -              unfolding diff_minus by auto
    1.63 +              by auto
    1.64            qed
    1.65            hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
    1.66              using `-r < a` `b < r` by auto
    1.67 @@ -3922,9 +3922,10 @@
    1.68        }
    1.69        hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
    1.70        moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
    1.71 -        unfolding diff_minus divide_inverse
    1.72 +        unfolding diff_conv_add_uminus divide_inverse
    1.73          by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
    1.74 -          isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
    1.75 +          isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
    1.76 +          simp del: add_uminus_conv_diff)
    1.77        ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
    1.78          by (rule LIM_less_bound)
    1.79        hence "?diff 1 n \<le> ?a 1 n" by auto