src/HOL/Log.thy
changeset 45916 758671e966a0
parent 45915 0e5a87b772f9
child 45930 2a882ef2cd73
     1.1 --- a/src/HOL/Log.thy	Thu Dec 15 17:21:29 2011 +0100
     1.2 +++ b/src/HOL/Log.thy	Mon Dec 19 13:58:54 2011 +0100
     1.3 @@ -87,16 +87,16 @@
     1.4  lemma log_ln: "ln x = log (exp(1)) x"
     1.5  by (simp add: log_def)
     1.6  
     1.7 -lemma DERIV_log: "x > 0 ==> DERIV (%y. log b y) x :> 1 / (ln b * x)"
     1.8 -  apply (subst log_def)
     1.9 -  apply (subgoal_tac "(%y. ln y / ln b) = (%y. (1 / ln b) * ln y)")
    1.10 -  apply (erule ssubst)
    1.11 -  apply (subgoal_tac "1 / (ln b * x) = (1 / ln b) * (1 / x)")
    1.12 -  apply (erule ssubst)
    1.13 -  apply (rule DERIV_cmult)
    1.14 -  apply (erule DERIV_ln_divide)
    1.15 -  apply auto
    1.16 -done
    1.17 +lemma DERIV_log: assumes "x > 0" shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
    1.18 +proof -
    1.19 +  def lb \<equiv> "1 / ln b"
    1.20 +  moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
    1.21 +    using `x > 0` by (auto intro!: DERIV_intros)
    1.22 +  ultimately show ?thesis
    1.23 +    by (simp add: log_def)
    1.24 +qed
    1.25 +
    1.26 +lemmas DERIV_log[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    1.27  
    1.28  lemma powr_log_cancel [simp]:
    1.29       "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powr (log a x) = x"