# HG changeset patch
# User haftmann
# Date 1163805621 -3600
# Node ID 4cb808163adc7f902ec9106a0d394cb25cb3a2d2
# Parent  0951647209f2d00668c0184405b07b5d3491fcec
workaround for definition violating type discipline

diff -r 0951647209f2 -r 4cb808163adc src/HOL/Relation_Power.thy
--- 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