summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Relation_Power.thy

author | nipkow |

Fri May 18 12:09:13 2001 +0200 (2001-05-18) | |

changeset 11306 | 6f4ed75b2dca |

parent 11305 | 2ce86fccc95b |

child 12338 | de0f4a63baa5 |

permissions | -rw-r--r-- |

added comments

1 (* Title: HOL/Relation_Power.thy

2 ID: $Id$

3 Author: Tobias Nipkow

4 Copyright 1996 TU Muenchen

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

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 *)

15 Relation_Power = Nat +

17 instance

18 set :: (term) {power} (* only ('a * 'a) set should be in power! *)

20 primrec (relpow)

21 "R^0 = Id"

22 "R^(Suc n) = R O (R^n)"

25 instance

26 fun :: (term,term)power (* only 'a => 'a should be in power! *)

28 primrec (funpow)

29 "f^0 = id"

30 "f^(Suc n) = f o (f^n)"

32 end