author paulson Fri Nov 13 17:15:12 2009 +0000 (2009-11-13) changeset 33667 958dc9f03611 parent 33655 c6dde2106128 child 33668 090288424d44
A little rationalisation
 src/HOL/Ln.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Ln.thy	Fri Nov 13 11:34:05 2009 +0000
1.2 +++ b/src/HOL/Ln.thy	Fri Nov 13 17:15:12 2009 +0000
1.3 @@ -342,9 +342,6 @@
1.4    apply auto
1.5  done
1.6
1.7 -lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
1.8 -  by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
1.9 -
1.10  lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"
1.11  proof -
1.12    assume "exp 1 <= x" and "x <= y"
```
```     2.1 --- a/src/HOL/Transcendental.thy	Fri Nov 13 11:34:05 2009 +0000
2.2 +++ b/src/HOL/Transcendental.thy	Fri Nov 13 17:15:12 2009 +0000
2.3 @@ -1213,6 +1213,9 @@
2.4  apply (simp_all add: abs_if isCont_ln)
2.5  done
2.6
2.7 +lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
2.8 +  by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
2.9 +
2.10  lemma ln_series: assumes "0 < x" and "x < 2"
2.11    shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))" (is "ln x = suminf (?f (x - 1))")
2.12  proof -
2.13 @@ -1702,9 +1705,8 @@
2.14  apply (drule_tac f = cos in Rolle)
2.15  apply (drule_tac [5] f = cos in Rolle)
2.16  apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def)
2.17 -apply (drule_tac y1 = xa in order_le_less_trans [THEN sin_gt_zero])
2.18 -apply (assumption, rule_tac y=y in order_less_le_trans, simp_all)
2.19 -apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all)
2.20 +apply (metis order_less_le_trans real_less_def sin_gt_zero)
2.21 +apply (metis order_less_le_trans real_less_def sin_gt_zero)
2.22  done
2.23
2.24  lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
2.25 @@ -2436,14 +2438,8 @@
2.26  apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
2.27  apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
2.28  apply (erule (1) isCont_inverse_function2 [where f=tan])
2.29 -apply (clarify, rule arctan_tan)
2.30 -apply (erule (1) order_less_le_trans)
2.31 -apply (erule (1) order_le_less_trans)
2.32 -apply (clarify, rule isCont_tan)
2.33 -apply (rule less_imp_neq [symmetric])
2.34 -apply (rule cos_gt_zero_pi)
2.35 -apply (erule (1) order_less_le_trans)
2.36 -apply (erule (1) order_le_less_trans)
2.37 +apply (metis arctan_tan order_le_less_trans order_less_le_trans)
2.38 +apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans real_less_def)
2.39  done
2.40
2.41  lemma DERIV_arcsin:
2.42 @@ -3119,8 +3115,7 @@
2.43  lemma polar_ex2:
2.44       "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a"
2.45  apply (insert polar_ex1 [where x=x and y="-y"], simp, clarify)
2.46 -apply (rule_tac x = r in exI)
2.47 -apply (rule_tac x = "-a" in exI, simp)
2.48 +apply (metis cos_minus minus_minus minus_mult_right sin_minus)
2.49  done
2.50
2.51  lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
```