A few more lemmas from Jeremy
authorpaulson
Mon Nov 16 14:32:12 2009 +0000 (2009-11-16)
changeset 33716c7b42ad3fadf
parent 33710 ffc5176a9105
child 33717 c03edebe7408
A few more lemmas from Jeremy
src/HOL/Log.thy
     1.1 --- a/src/HOL/Log.thy	Mon Nov 16 12:09:59 2009 +0100
     1.2 +++ b/src/HOL/Log.thy	Mon Nov 16 14:32:12 2009 +0000
     1.3 @@ -87,6 +87,17 @@
     1.4  lemma log_ln: "ln x = log (exp(1)) x"
     1.5  by (simp add: log_def)
     1.6  
     1.7 +lemma DERIV_log: "x > 0 ==> DERIV (%y. log b y) x :> 1 / (ln b * x)"
     1.8 +  apply (subst log_def)
     1.9 +  apply (subgoal_tac "(%y. ln y / ln b) = (%y. (1 / ln b) * ln y)")
    1.10 +  apply (erule ssubst)
    1.11 +  apply (subgoal_tac "1 / (ln b * x) = (1 / ln b) * (1 / x)")
    1.12 +  apply (erule ssubst)
    1.13 +  apply (rule DERIV_cmult)
    1.14 +  apply (erule DERIV_ln_divide)
    1.15 +  apply auto
    1.16 +done
    1.17 +
    1.18  lemma powr_log_cancel [simp]:
    1.19       "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powr (log a x) = x"
    1.20  by (simp add: powr_def log_def)
    1.21 @@ -152,9 +163,20 @@
    1.22    apply (rule powr_realpow [THEN sym], simp)
    1.23  done
    1.24  
    1.25 -lemma ln_pwr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
    1.26 +lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
    1.27  by (unfold powr_def, simp)
    1.28  
    1.29 +lemma log_powr: "0 < x ==> 0 \<le> y ==> log b (x powr y) = y * log b x"
    1.30 +  apply (case_tac "y = 0")
    1.31 +  apply force
    1.32 +  apply (auto simp add: log_def ln_powr field_simps)
    1.33 +done
    1.34 +
    1.35 +lemma log_nat_power: "0 < x ==> log b (x^n) = real n * log b x"
    1.36 +  apply (subst powr_realpow [symmetric])
    1.37 +  apply (auto simp add: log_powr)
    1.38 +done
    1.39 +
    1.40  lemma ln_bound: "1 <= x ==> ln x <= x"
    1.41    apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
    1.42    apply simp
    1.43 @@ -207,7 +229,7 @@
    1.44    apply (rule mult_imp_le_div_pos)
    1.45    apply (assumption)
    1.46    apply (subst mult_commute)
    1.47 -  apply (subst ln_pwr [THEN sym])
    1.48 +  apply (subst ln_powr [THEN sym])
    1.49    apply auto
    1.50    apply (rule ln_bound)
    1.51    apply (erule ge_one_powr_ge_zero)