src/HOL/Relation_Power.thy
author nipkow
Fri May 18 07:56:19 2001 +0200 (2001-05-18)
changeset 11305 2ce86fccc95b
parent 10213 01c2744a3786
child 11306 6f4ed75b2dca
permissions -rw-r--r--
added ^ on functions.
     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 Both for functions and relations.
     8 *)
     9 
    10 Relation_Power = Nat +
    11 
    12 instance
    13   set :: (term) {power}   (* only ('a * 'a) set should be in power! *)
    14 
    15 primrec (relpow)
    16   "R^0 = Id"
    17   "R^(Suc n) = R O (R^n)"
    18 
    19 
    20 instance fun :: (term,term)power   (* only 'a \<Rightarrow> 'a should be in power! *)
    21 
    22 primrec (funpow)
    23   "f^0 = id"
    24   "f^(Suc n) = f o (f^n)"
    25 
    26 end