src/HOL/Transcendental.thy
changeset 56483 5b82c58b665c
parent 56479 91958d4b30f7
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Transcendental.thy	Wed Apr 09 10:04:31 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Apr 09 13:15:21 2014 +0200
     1.3 @@ -1968,19 +1968,23 @@
     1.4  lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
     1.5    by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
     1.6  
     1.7 -lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
     1.8 -  unfolding powr_def by simp
     1.9 -
    1.10 -lemma log_powr: "0 < x ==> 0 \<le> y ==> log b (x powr y) = y * log b x"
    1.11 -  apply (cases "y = 0")
    1.12 -  apply force
    1.13 -  apply (auto simp add: log_def ln_powr field_simps)
    1.14 -  done
    1.15 -
    1.16 -lemma log_nat_power: "0 < x ==> log b (x^n) = real n * log b x"
    1.17 -  apply (subst powr_realpow [symmetric])
    1.18 -  apply (auto simp add: log_powr)
    1.19 -  done
    1.20 +lemma ln_powr: "ln (x powr y) = y * ln x"
    1.21 +  by (simp add: powr_def)
    1.22 +
    1.23 +lemma log_powr: "log b (x powr y) = y * log b x"
    1.24 +  by (simp add: log_def ln_powr)
    1.25 +
    1.26 +lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
    1.27 +  by (simp add: log_powr powr_realpow [symmetric])
    1.28 +
    1.29 +lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
    1.30 +  by (simp add: log_def)
    1.31 +
    1.32 +lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
    1.33 +  by (simp add: log_def ln_realpow)
    1.34 +
    1.35 +lemma log_base_powr: "log (a powr b) x = log a x / b"
    1.36 +  by (simp add: log_def ln_powr)
    1.37  
    1.38  lemma ln_bound: "1 <= x ==> ln x <= x"
    1.39    apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")