equal
deleted
inserted
replaced
19 "R^0 = Id" |
19 "R^0 = Id" |
20 "R^(Suc n) = R O (R^n)" |
20 "R^(Suc n) = R O (R^n)" |
21 |
21 |
22 |
22 |
23 instance |
23 instance |
24 fun :: (type, type) power .. |
24 "fun" :: (type, type) power .. |
25 --{* only type @{typ "'a => 'a"} should be in class @{text power}!*} |
25 --{* only type @{typ "'a => 'a"} should be in class @{text power}!*} |
26 |
26 |
27 (*f^n = f o ... o f, the n-fold composition of f*) |
27 (*f^n = f o ... o f, the n-fold composition of f*) |
28 primrec (funpow) |
28 primrec (funpow) |
29 "f^0 = id" |
29 "f^0 = id" |
32 text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on |
32 text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on |
33 functions and relations has too general a domain, namely @{typ "('a * 'b)set"} |
33 functions and relations has too general a domain, namely @{typ "('a * 'b)set"} |
34 and @{typ "'a => 'b"}. Explicit type constraints may therefore be necessary. |
34 and @{typ "'a => 'b"}. Explicit type constraints may therefore be necessary. |
35 For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need |
35 For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need |
36 constraints.*} |
36 constraints.*} |
|
37 |
|
38 text {* |
|
39 Circumvent this problem for code generation: |
|
40 *} |
|
41 |
|
42 definition |
|
43 funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
44 funpow_def: "funpow n f = f ^ n" |
|
45 |
|
46 lemmas [code inline] = funpow_def [symmetric] |
|
47 |
|
48 lemma [code func]: |
|
49 "funpow 0 f = id" |
|
50 "funpow (Suc n) f = f o funpow n f" |
|
51 unfolding funpow_def by simp_all |
37 |
52 |
38 lemma funpow_add: "f ^ (m+n) = f^m o f^n" |
53 lemma funpow_add: "f ^ (m+n) = f^m o f^n" |
39 by (induct m) simp_all |
54 by (induct m) simp_all |
40 |
55 |
41 lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)" |
56 lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)" |