--- a/src/HOL/Relation_Power.thy Sat Nov 18 00:20:20 2006 +0100
+++ b/src/HOL/Relation_Power.thy Sat Nov 18 00:20:21 2006 +0100
@@ -21,7 +21,7 @@
instance
- fun :: (type, type) power ..
+ "fun" :: (type, type) power ..
--{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
(*f^n = f o ... o f, the n-fold composition of f*)
@@ -35,6 +35,21 @@
For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need
constraints.*}
+text {*
+ Circumvent this problem for code generation:
+*}
+
+definition
+ funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+ funpow_def: "funpow n f = f ^ n"
+
+lemmas [code inline] = funpow_def [symmetric]
+
+lemma [code func]:
+ "funpow 0 f = id"
+ "funpow (Suc n) f = f o funpow n f"
+ unfolding funpow_def by simp_all
+
lemma funpow_add: "f ^ (m+n) = f^m o f^n"
by (induct m) simp_all