src/HOL/Transcendental.thy

 
 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 ^ nat(floor i) else 1 / b ^ nat(floor (- i)))
+    else if \<lfloor>i\<rfloor> = i then (if 0 \<le> i then b ^ nat \<lfloor>i\<rfloor> else 1 / b ^ nat \<lfloor>- i\<rfloor>)
     else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
   by (auto simp: powr_int)
 
 lemma powr_one:
   fixes x::real shows "0 \<le> x \<Longrightarrow> x powr 1 = x"

 proof -
   have xle: "x < (1 + real_of_int \<lfloor>x/pi\<rfloor>) * pi"
     using floor_correct [of "x/pi"]
     by (simp add: add.commute divide_less_eq)
   obtain n where "real n * pi \<le> x" "x < real (Suc n) * pi"
-    apply (rule that [of "nat (floor (x/pi))"] )
+    apply (rule that [of "nat \<lfloor>x/pi\<rfloor>"])
     using assms
     apply (simp_all add: xle)
     apply (metis floor_less_iff less_irrefl mult_imp_div_pos_less not_le pi_gt_zero)
     done
   then have x: "0 \<le> x - n * pi" "(x - n * pi) \<le> pi" "cos (x - n * pi) = 0"