--- a/src/HOL/Transcendental.thy Tue May 13 16:18:16 2014 +0200
+++ b/src/HOL/Transcendental.thy Tue May 13 22:14:12 2014 +0200
@@ -1963,6 +1963,12 @@
lemma ln_powr: "ln (x powr y) = y * ln x"
by (simp add: powr_def)
+lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) = ln b / n"
+by(simp add: root_powr_inverse ln_powr)
+
+lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) = log b a / n"
+by(simp add: log_def ln_root)
+
lemma log_powr: "log b (x powr y) = y * log b x"
by (simp add: log_def ln_powr)
@@ -1978,6 +1984,9 @@
lemma log_base_powr: "log (a powr b) x = log a x / b"
by (simp add: log_def ln_powr)
+lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
+by(simp add: log_def ln_root)
+
lemma ln_bound: "1 <= x ==> ln x <= x"
apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
apply simp