# HG changeset patch
# User hoelzl
# Date 1397042121 -7200
# Node ID 5b82c58b665c259318b2a9d37179abc4b8c91248
# Parent  39ac12b655aba1c8a6624dfd3bd9d2db24ed024c
generalize ln/log_powr; add log_base_powr/pow

diff -r 39ac12b655ab -r 5b82c58b665c src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 09 10:04:31 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 09 13:15:21 2014 +0200
@@ -1804,12 +1804,7 @@
     hence pow_gt0: "(0::real) < 2^nat (-e)" by auto
     hence inv_gt0: "(0::real) < inverse (2^nat (-e))" by auto
     show ?thesis using False unfolding bl_def[symmetric] using `0 < real m` `0 \<le> bl`
-      apply (simp add: ln_mult lne)
-      apply (cases "e=0")
-        apply (cases "bl = 0", simp_all add: powr_minus ln_inverse ln_powr)
-        apply (simp add: ln_inverse lne)
-        apply (cases "bl = 0", simp_all add: ln_inverse ln_powr field_simps)
-      done
+      by (auto simp add: lne ln_mult ln_powr ln_div field_simps)
   qed
 qed
 
diff -r 39ac12b655ab -r 5b82c58b665c src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Apr 09 10:04:31 2014 +0200
+++ b/src/HOL/Transcendental.thy	Wed Apr 09 13:15:21 2014 +0200
@@ -1968,19 +1968,23 @@
 lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
 
-lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
-  unfolding powr_def by simp
-
-lemma log_powr: "0 < x ==> 0 \<le> y ==> log b (x powr y) = y * log b x"
-  apply (cases "y = 0")
-  apply force
-  apply (auto simp add: log_def ln_powr field_simps)
-  done
-
-lemma log_nat_power: "0 < x ==> log b (x^n) = real n * log b x"
-  apply (subst powr_realpow [symmetric])
-  apply (auto simp add: log_powr)
-  done
+lemma ln_powr: "ln (x powr y) = y * ln x"
+  by (simp add: powr_def)
+
+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_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
+  by (simp add: log_def)
+
+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 ln_bound: "1 <= x ==> ln x <= x"
   apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")