| changeset 10213 | 01c2744a3786 |
| child 11305 | 2ce86fccc95b |
| 10212:33fe2d701ddd | 10213:01c2744a3786 |
|---|---|
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 |