src/HOL/Trancl.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5608 a82a038a3e7a
child 6906 46652582f831
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 reflexive/transitive closure;
     9 trancl  is transitive closure
    10 reflcl  is reflexive closure
    11 
    12 These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
    13       atomic.
    14 *)
    15 
    16 Trancl = Lfp + Relation + 
    17 
    18 constdefs
    19   rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
    20   "r^*  ==  lfp(%s. Id Un (r O s))"
    21 
    22   trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
    23   "r^+  ==  r O rtrancl(r)"
    24 
    25 syntax
    26   reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
    27 
    28 translations
    29   "r^=" == "r Un Id"
    30 
    31 end