author haftmann Fri, 17 Aug 2018 11:26:35 +0000 changeset 68774 9fc50a3e07f6 parent 68773 1db9fef36f12 child 68775 8fbfb67f6824 child 68776 403dd13cf6e9
proper code abbreviation for power on real
```--- a/src/HOL/Transcendental.thy	Fri Aug 17 11:26:34 2018 +0000
+++ b/src/HOL/Transcendental.thy	Fri Aug 17 11:26:35 2018 +0000
@@ -1693,7 +1693,7 @@

definition powr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a::ln"  (infixr "powr" 80)
\<comment> \<open>exponentation via ln and exp\<close>
-  where  [code del]: "x powr a \<equiv> if x = 0 then 0 else exp (a * ln x)"
+  where "x powr a \<equiv> if x = 0 then 0 else exp (a * ln x)"

lemma powr_0 [simp]: "0 powr z = 0"
@@ -2789,12 +2789,15 @@
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)
+definition powr_real :: "real \<Rightarrow> real \<Rightarrow> real"
+  where [code_abbrev, simp]: "powr_real = Transcendental.powr"
+
+lemma compute_powr_real [code]:
+  "powr_real b i =
+    (if b \<le> 0 then Code.abort (STR ''powr_real with nonpositive base'') (\<lambda>_. powr_real b 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))"
+     else Code.abort (STR ''powr_real with non-integer exponent'') (\<lambda>_. powr_real b i))"
+    for b i :: real
by (auto simp: powr_int)

lemma powr_one: "0 \<le> x \<Longrightarrow> x powr 1 = x"```