add lemmas
authornoschinl
Mon Dec 19 14:41:08 2011 +0100 (2011-12-19)
changeset 459302a882ef2cd73
parent 45916 758671e966a0
child 45931 99cf6e470816
add lemmas
src/HOL/Fact.thy
src/HOL/Log.thy
     1.1 --- a/src/HOL/Fact.thy	Mon Dec 19 13:58:54 2011 +0100
     1.2 +++ b/src/HOL/Fact.thy	Mon Dec 19 14:41:08 2011 +0100
     1.3 @@ -285,6 +285,12 @@
     1.4      (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
     1.5  by (cases m) auto
     1.6  
     1.7 +lemma fact_le_power: "fact n \<le> n^n"
     1.8 +proof (induct n)
     1.9 +  case (Suc n)
    1.10 +  then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
    1.11 +  then show ?case by (simp add: add_le_mono)
    1.12 +qed simp
    1.13  
    1.14  subsection {* @{term fact} and @{term of_nat} *}
    1.15  
     2.1 --- a/src/HOL/Log.thy	Mon Dec 19 13:58:54 2011 +0100
     2.2 +++ b/src/HOL/Log.thy	Mon Dec 19 14:41:08 2011 +0100
     2.3 @@ -60,6 +60,10 @@
     2.4  lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
     2.5  by (simp add: powr_def exp_add [symmetric] left_distrib)
     2.6  
     2.7 +lemma powr_mult_base:
     2.8 +  "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
     2.9 +using assms by (auto simp: powr_add)
    2.10 +
    2.11  lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
    2.12  by (simp add: powr_def)
    2.13  
    2.14 @@ -178,6 +182,10 @@
    2.15    apply (rule powr_realpow [THEN sym], simp)
    2.16  done
    2.17  
    2.18 +lemma root_powr_inverse:
    2.19 +  "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
    2.20 +by (auto simp: root_def powr_realpow[symmetric] powr_powr)
    2.21 +
    2.22  lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
    2.23  by (unfold powr_def, simp)
    2.24