# HG changeset patch
# User hoelzl
# Date 1324299534 -3600
# Node ID 758671e966a0ebbc9c5592ae33702607ebc49434
# Parent  0e5a87b772f918baeb52f0c02549f86f70df3ffe
isarfied proof; add log to DERIV_intros

diff -r 0e5a87b772f9 -r 758671e966a0 src/HOL/Log.thy
--- a/src/HOL/Log.thy	Thu Dec 15 17:21:29 2011 +0100
+++ b/src/HOL/Log.thy	Mon Dec 19 13:58:54 2011 +0100
@@ -87,16 +87,16 @@
 lemma log_ln: "ln x = log (exp(1)) x"
 by (simp add: log_def)
 
-lemma DERIV_log: "x > 0 ==> DERIV (%y. log b y) x :> 1 / (ln b * x)"
-  apply (subst log_def)
-  apply (subgoal_tac "(%y. ln y / ln b) = (%y. (1 / ln b) * ln y)")
-  apply (erule ssubst)
-  apply (subgoal_tac "1 / (ln b * x) = (1 / ln b) * (1 / x)")
-  apply (erule ssubst)
-  apply (rule DERIV_cmult)
-  apply (erule DERIV_ln_divide)
-  apply auto
-done
+lemma DERIV_log: assumes "x > 0" shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
+proof -
+  def lb \<equiv> "1 / ln b"
+  moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
+    using `x > 0` by (auto intro!: DERIV_intros)
+  ultimately show ?thesis
+    by (simp add: log_def)
+qed
+
+lemmas DERIV_log[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
 
 lemma powr_log_cancel [simp]:
      "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powr (log a x) = x"