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
     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 Relation_Power = Nat +
    16 
    17 instance
    18   set :: (term) {power}   (* only ('a * 'a) set should be in power! *)
    19 
    20 primrec (relpow)
    21   "R^0 = Id"
    22   "R^(Suc n) = R O (R^n)"
    23 
    24 
    25 instance
    26   fun :: (term,term)power   (* only 'a => 'a should be in power! *)
    27 
    28 primrec (funpow)
    29   "f^0 = id"
    30   "f^(Suc n) = f o (f^n)"
    31 
    32 end