src/HOL/Transitive_Closure.thy
author wenzelm
Wed Oct 25 18:32:02 2000 +0200 (2000-10-25)
changeset 10331 7411e4659d4a
parent 10213 01c2744a3786
child 10565 7f7c1c3511e2
permissions -rw-r--r--
more "xsymbols" syntax;
     1 (*  Title:      HOL/Transitive_Closure.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
    13 to be atomic.
    14 *)
    15 
    16 Transitive_Closure = 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 translations
    28   "r^=" == "r Un Id"
    29 
    30 syntax (xsymbols)
    31   rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    32   trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    33   "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    34 
    35 end