src/HOL/Relation_Power.thy
author nipkow
Wed Aug 04 19:12:15 2004 +0200 (2004-08-04)
changeset 15112 6f0772a94299
parent 12338 de0f4a63baa5
child 15131 c69542757a4d
permissions -rw-r--r--
added a thm
     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 = Nat:
    16 
    17 instance
    18   set :: (type) 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 :: (type, type) 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 lemma funpow_add: "f ^ (m+n) = f^m o f^n"
    33 by(induct m) simp_all
    34 
    35 end