--- a/src/HOL/Transcendental.thy Tue Nov 11 21:14:19 2014 +0100
+++ b/src/HOL/Transcendental.thy Wed Nov 12 17:36:25 2014 +0100
@@ -2013,6 +2013,14 @@
then show ?thesis by (simp add: assms powr_realpow[symmetric])
qed
+lemma compute_powr[code]:
+ fixes i::real
+ shows "b powr i =
+ (if b \<le> 0 then Code.abort (STR ''op powr with nonpositive base'') (\<lambda>_. b powr i)
+ else if floor i = i then (if 0 \<le> i then b ^ natfloor i else 1 / b ^ natfloor (- i))
+ else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
+ by (auto simp: natfloor_def powr_int)
+
lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
using powr_realpow [of x 1] by simp