src/HOL/Relation_Power.thy
 changeset 21414 4cb808163adc parent 20503 503ac4c5ef91 child 22737 d87ccbcc2702
```     1.1 --- a/src/HOL/Relation_Power.thy	Sat Nov 18 00:20:20 2006 +0100
1.2 +++ b/src/HOL/Relation_Power.thy	Sat Nov 18 00:20:21 2006 +0100
1.3 @@ -21,7 +21,7 @@
1.4
1.5
1.6  instance
1.7 -  fun :: (type, type) power ..
1.8 +  "fun" :: (type, type) power ..
1.9        --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
1.10
1.11  (*f^n = f o ... o f, the n-fold composition of f*)
1.12 @@ -35,6 +35,21 @@
1.13  For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need
1.14  constraints.*}
1.15
1.16 +text {*
1.17 +  Circumvent this problem for code generation:
1.18 +*}
1.19 +
1.20 +definition
1.21 +  funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
1.22 +  funpow_def: "funpow n f = f ^ n"
1.23 +
1.24 +lemmas [code inline] = funpow_def [symmetric]
1.25 +
1.26 +lemma [code func]:
1.27 +  "funpow 0 f = id"
1.28 +  "funpow (Suc n) f = f o funpow n f"
1.29 +  unfolding funpow_def by simp_all
1.30 +
1.31  lemma funpow_add: "f ^ (m+n) = f^m o f^n"
1.32    by (induct m) simp_all
1.33
```