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.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.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.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.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.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.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.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