src/HOL/Relation_Power.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15112 6f0772a94299
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
     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 theory Relation_Power
    16 import Nat
    17 begin
    18 
    19 instance
    20   set :: (type) power ..  (* only ('a * 'a) set should be in power! *)
    21 
    22 primrec (relpow)
    23   "R^0 = Id"
    24   "R^(Suc n) = R O (R^n)"
    25 
    26 
    27 instance
    28   fun :: (type, type) power ..  (* only 'a => 'a should be in power! *)
    29 
    30 primrec (funpow)
    31   "f^0 = id"
    32   "f^(Suc n) = f o (f^n)"
    33 
    34 lemma funpow_add: "f ^ (m+n) = f^m o f^n"
    35 by(induct m) simp_all
    36 
    37 end