src/HOL/Trancl.thy
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1558 9c6ebfab4e05
child 1642 21db0cf9a1a4
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     1 (*  Title:      HOL/Trancl.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Relfexive and Transitive closure of a relation
     7 
     8 rtrancl is refl&transitive closure;
     9 trancl is transitive closure
    10 reflcl is reflexive closure
    11 *)
    12 
    13 Trancl = Lfp + Relation + 
    14 
    15 constdefs
    16   rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [100] 100)
    17   "r^*  ==  lfp(%s. id Un (r O s))"
    18 
    19   trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [100] 100)
    20   "r^+  ==  r O rtrancl(r)"
    21 
    22 syntax
    23   reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
    24 
    25 translations
    26   "r^=" == "r Un id"
    27 
    28 end