src/HOL/Transcendental.thy

   by (induct n) (simp_all add: ac_simps powr_add of_nat_Suc)
 
 lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   by (metis of_nat_numeral powr_realpow)
 
+lemma powr_real_of_int: 
+  "x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (-n)))"
+  using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
+  by (auto simp: field_simps powr_minus)  
+
 lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
 by(simp add: powr_numeral)
 
 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
   apply (case_tac "x = 0", simp, simp)