# HG changeset patch
# User nipkow
# Date 1400012052 -7200
# Node ID efa2a83d548b618e6c7e6a970d1afcc24c1ab00b
# Parent  4fca7e1470e2bcefe1a59dfc68eda48cb902ea34
added lemmas

diff -r 4fca7e1470e2 -r efa2a83d548b 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