# HG changeset patch
# User immler
# Date 1415810185 -3600
# Node ID 11b6c099f5f35cca60cbf571a22e69b698d335e3
# Parent  51890cb80b305359491a21d536a76f2212e53ef9
code equation for powr

diff -r 51890cb80b30 -r 11b6c099f5f3 src/HOL/Transcendental.thy
--- 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