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