| author | wenzelm |
| Fri, 15 Dec 2000 17:59:30 +0100 | |
| changeset 10680 | 26e4aecf3207 |
| parent 10213 | 01c2744a3786 |
| child 11305 | 2ce86fccc95b |
| permissions | -rw-r--r-- |
| 10213 | 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 |
*) |
|
8 |
||
9 |
Relation_Power = Nat + |
|
10 |
||
11 |
instance |
|
12 |
set :: (term) {power} (* only ('a * 'a) set should be in power! *)
|
|
13 |
||
14 |
primrec (relpow) |
|
15 |
"R^0 = Id" |
|
16 |
"R^(Suc n) = R O (R^n)" |
|
17 |
||
18 |
end |