src/HOL/Transcendental.thy
changeset 58981 11b6c099f5f3
parent 58889 5b7a9633cfa8
child 58984 ae0c56c485ae
     1.1 --- a/src/HOL/Transcendental.thy	Tue Nov 11 21:14:19 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Nov 12 17:36:25 2014 +0100
     1.3 @@ -2013,6 +2013,14 @@
     1.4    then show ?thesis by (simp add: assms powr_realpow[symmetric])
     1.5  qed
     1.6  
     1.7 +lemma compute_powr[code]:
     1.8 +  fixes i::real
     1.9 +  shows "b powr i =
    1.10 +    (if b \<le> 0 then Code.abort (STR ''op powr with nonpositive base'') (\<lambda>_. b powr i)
    1.11 +    else if floor i = i then (if 0 \<le> i then b ^ natfloor i else 1 / b ^ natfloor (- i))
    1.12 +    else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
    1.13 +  by (auto simp: natfloor_def powr_int)
    1.14 +
    1.15  lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
    1.16    using powr_realpow [of x 1] by simp
    1.17