src/HOL/Transitive_Closure.thy
author wenzelm
Fri Jan 26 00:15:36 2001 +0100 (2001-01-26)
changeset 10980 0a45f2efaaec
parent 10827 a7ac8e1e024b
child 10996 74e970389def
permissions -rw-r--r--
Transitive_Closure turned into new-style theory;
     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 theory Transitive_Closure = Lfp + Relation
    17 files ("Transitive_Closure_lemmas.ML"):
    18 
    19 constdefs
    20   rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    21   "r^* == lfp (%s. Id Un (r O s))"
    22 
    23   trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
    24   "r^+ ==  r O rtrancl r"
    25 
    26 syntax
    27   "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
    28 translations
    29   "r^=" == "r Un Id"
    30 
    31 syntax (xsymbols)
    32   rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    33   trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    34   "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    35 
    36 use "Transitive_Closure_lemmas.ML"
    37 
    38 end