author hoelzl Tue, 30 Jun 2009 18:25:55 +0200 changeset 31883 9e5bdbae677d parent 31882 3578434d645d child 31884 6129dea3d8a9
DERIV_ln is proved in Transcendental and in Ln, use Transcendental to prove Ln.
 src/HOL/Ln.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Ln.thy	Tue Jun 30 18:24:00 2009 +0200
+++ b/src/HOL/Ln.thy	Tue Jun 30 18:25:55 2009 +0200
@@ -343,43 +343,7 @@
done

lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
-  apply (unfold deriv_def, unfold LIM_eq, clarsimp)
-  apply (rule exI)
-  apply (rule conjI)
-  prefer 2
-  apply clarsimp
-  apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) =
-      (ln (1 + xa / x) - xa / x) / xa")
-  apply (erule ssubst)
-  apply (subst abs_divide)
-  apply (rule mult_imp_div_pos_less)
-  apply force
-  apply (rule order_le_less_trans)
-  apply (rule abs_ln_one_plus_x_minus_x_bound)
-  apply (subst abs_divide)
-  apply (subst abs_of_pos, assumption)
-  apply (erule mult_imp_div_pos_le)
-  apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
-  apply force
-  apply assumption
-  apply (simp add: power2_eq_square mult_compare_simps)
-  apply (rule mult_imp_div_pos_less)
-  apply (rule mult_pos_pos, assumption, assumption)
-  apply (subgoal_tac "xa * xa = abs xa * abs xa")
-  apply (erule ssubst)
-  apply (subgoal_tac "abs xa * (abs xa * 2) < abs xa * (r * (x * x))")
-  apply (simp only: mult_ac)
-  apply (rule mult_strict_left_mono)
-  apply (erule conjE, assumption)
-  apply force
-  apply simp
-  apply (subst ln_div [THEN sym])
-  apply arith