src/HOL/Transcendental.thy

   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
 
 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)
 
 lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
   by (simp add: log_powr powr_realpow [symmetric])

 lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
   by (simp add: log_def ln_realpow)
 
 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
   apply (rule ln_add_one_self_le_self, simp)