1.1 --- a/src/HOL/Log.thy	Wed Apr 18 14:29:16 2012 +0200
     1.2 +++ b/src/HOL/Log.thy	Wed Apr 18 14:29:17 2012 +0200
     1.3 @@ -199,12 +199,26 @@
     1.4    apply (subst powr_add, simp, simp)
     1.5  done
     1.6  
     1.7 -lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0
     1.8 -  else x powr (real n))"
     1.9 +lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
    1.10    apply (case_tac "x = 0", simp, simp)
    1.11    apply (rule powr_realpow [THEN sym], simp)
    1.12  done
    1.13  
    1.14 +lemma powr_int:
    1.15 +  assumes "x > 0"
    1.16 +  shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
    1.17 +proof cases
    1.18 +  assume "i < 0"
    1.19 +  have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps)
    1.20 +  show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric])
    1.21 +qed (simp add: assms powr_realpow[symmetric])
    1.22 +
    1.23 +lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x^numeral n"
    1.24 +  using powr_realpow[of x "numeral n"] by simp
    1.25 +
    1.26 +lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr neg_numeral n = 1 / x^numeral n"
    1.27 +  using powr_int[of x "neg_numeral n"] by simp
    1.28 +
    1.29  lemma root_powr_inverse:
    1.30    "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
    1.31  by (auto simp: root_def powr_realpow[symmetric] powr_powr)