src/HOL/Log.thy
changeset 45930 2a882ef2cd73
parent 45916 758671e966a0
child 47593 69f0af2b7d54
     1.1 --- a/src/HOL/Log.thy	Mon Dec 19 13:58:54 2011 +0100
     1.2 +++ b/src/HOL/Log.thy	Mon Dec 19 14:41:08 2011 +0100
     1.3 @@ -60,6 +60,10 @@
     1.4  lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
     1.5  by (simp add: powr_def exp_add [symmetric] left_distrib)
     1.6  
     1.7 +lemma powr_mult_base:
     1.8 +  "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
     1.9 +using assms by (auto simp: powr_add)
    1.10 +
    1.11  lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
    1.12  by (simp add: powr_def)
    1.13  
    1.14 @@ -178,6 +182,10 @@
    1.15    apply (rule powr_realpow [THEN sym], simp)
    1.16  done
    1.17  
    1.18 +lemma root_powr_inverse:
    1.19 +  "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
    1.20 +by (auto simp: root_def powr_realpow[symmetric] powr_powr)
    1.21 +
    1.22  lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
    1.23  by (unfold powr_def, simp)
    1.24