src/HOL/Transcendental.thy

--- 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