generalize ln/log_powr; add log_base_powr/pow
authorhoelzl
Wed Apr 09 13:15:21 2014 +0200 (2014-04-09)
changeset 564835b82c58b665c
parent 56482 39ac12b655ab
child 56484 c451cf8b29c8
generalize ln/log_powr; add log_base_powr/pow
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 09 10:04:31 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 09 13:15:21 2014 +0200
     1.3 @@ -1804,12 +1804,7 @@
     1.4      hence pow_gt0: "(0::real) < 2^nat (-e)" by auto
     1.5      hence inv_gt0: "(0::real) < inverse (2^nat (-e))" by auto
     1.6      show ?thesis using False unfolding bl_def[symmetric] using `0 < real m` `0 \<le> bl`
     1.7 -      apply (simp add: ln_mult lne)
     1.8 -      apply (cases "e=0")
     1.9 -        apply (cases "bl = 0", simp_all add: powr_minus ln_inverse ln_powr)
    1.10 -        apply (simp add: ln_inverse lne)
    1.11 -        apply (cases "bl = 0", simp_all add: ln_inverse ln_powr field_simps)
    1.12 -      done
    1.13 +      by (auto simp add: lne ln_mult ln_powr ln_div field_simps)
    1.14    qed
    1.15  qed
    1.16  
     2.1 --- a/src/HOL/Transcendental.thy	Wed Apr 09 10:04:31 2014 +0200
     2.2 +++ b/src/HOL/Transcendental.thy	Wed Apr 09 13:15:21 2014 +0200
     2.3 @@ -1968,19 +1968,23 @@
     2.4  lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
     2.5    by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
     2.6  
     2.7 -lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
     2.8 -  unfolding powr_def by simp
     2.9 -
    2.10 -lemma log_powr: "0 < x ==> 0 \<le> y ==> log b (x powr y) = y * log b x"
    2.11 -  apply (cases "y = 0")
    2.12 -  apply force
    2.13 -  apply (auto simp add: log_def ln_powr field_simps)
    2.14 -  done
    2.15 -
    2.16 -lemma log_nat_power: "0 < x ==> log b (x^n) = real n * log b x"
    2.17 -  apply (subst powr_realpow [symmetric])
    2.18 -  apply (auto simp add: log_powr)
    2.19 -  done
    2.20 +lemma ln_powr: "ln (x powr y) = y * ln x"
    2.21 +  by (simp add: powr_def)
    2.22 +
    2.23 +lemma log_powr: "log b (x powr y) = y * log b x"
    2.24 +  by (simp add: log_def ln_powr)
    2.25 +
    2.26 +lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
    2.27 +  by (simp add: log_powr powr_realpow [symmetric])
    2.28 +
    2.29 +lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
    2.30 +  by (simp add: log_def)
    2.31 +
    2.32 +lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
    2.33 +  by (simp add: log_def ln_realpow)
    2.34 +
    2.35 +lemma log_base_powr: "log (a powr b) x = log a x / b"
    2.36 +  by (simp add: log_def ln_powr)
    2.37  
    2.38  lemma ln_bound: "1 <= x ==> ln x <= x"
    2.39    apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")