--- a/src/HOL/Log.thy Mon Dec 19 17:10:45 2011 +0100
+++ b/src/HOL/Log.thy Mon Dec 19 17:10:53 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"
@@ -285,6 +285,10 @@
finally show ?thesis .
qed
+lemma tendsto_powr [tendsto_intros]:
+ "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
+ unfolding powr_def by (intro tendsto_intros)
+
(* FIXME: generalize by replacing d by with g x and g ---> d? *)
lemma tendsto_zero_powrI:
assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
--- a/src/HOL/Transcendental.thy Mon Dec 19 17:10:45 2011 +0100
+++ b/src/HOL/Transcendental.thy Mon Dec 19 17:10:53 2011 +0100
@@ -1166,6 +1166,10 @@
apply (rule isCont_inverse_function [where f=exp], simp_all)
done
+lemma tendsto_ln [tendsto_intros]:
+ "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
+ by (rule isCont_tendsto_compose [OF isCont_ln])
+
lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
apply (erule DERIV_cong [OF DERIV_exp exp_ln])