workaround for definition violating type discipline
authorhaftmann
Sat Nov 18 00:20:21 2006 +0100 (2006-11-18)
changeset 214144cb808163adc
parent 21413 0951647209f2
child 21415 39f98c88f88a
workaround for definition violating type discipline
src/HOL/Relation_Power.thy
     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