src/HOL/Relation_Power.thy
 author nipkow Mon Aug 16 14:22:27 2004 +0200 (2004-08-16) changeset 15131 c69542757a4d parent 15112 6f0772a94299 child 15140 322485b816ac permissions -rw-r--r--
```     1 (*  Title:      HOL/Relation_Power.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow
```
```     4     Copyright   1996  TU Muenchen
```
```     5
```
```     6 R^n = R O ... O R, the n-fold composition of R
```
```     7 f^n = f o ... o f, the n-fold composition of f
```
```     8
```
```     9 WARNING: due to the limits of Isabelle's type classes, ^ on functions and
```
```    10 relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
```
```    11 This means that it may be necessary to attach explicit type constraints.
```
```    12 Examples: range(f^n) = A and Range(R^n) = B need constraints.
```
```    13 *)
```
```    14
```
```    15 theory Relation_Power
```
```    16 import Nat
```
```    17 begin
```
```    18
```
```    19 instance
```
```    20   set :: (type) power ..  (* only ('a * 'a) set should be in power! *)
```
```    21
```
```    22 primrec (relpow)
```
```    23   "R^0 = Id"
```
```    24   "R^(Suc n) = R O (R^n)"
```
```    25
```
```    26
```
```    27 instance
```
```    28   fun :: (type, type) power ..  (* only 'a => 'a should be in power! *)
```
```    29
```
```    30 primrec (funpow)
```
```    31   "f^0 = id"
```
```    32   "f^(Suc n) = f o (f^n)"
```
```    33
```
```    34 lemma funpow_add: "f ^ (m+n) = f^m o f^n"
```
```    35 by(induct m) simp_all
```
```    36
```
```    37 end
```