author | wenzelm |
Fri, 03 Nov 2000 21:31:11 +0100 | |
changeset 10383 | a092ae7bb2a6 |
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 |