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;
nipkow@10213
     1
(*  Title:      HOL/Transitive_Closure.thy
nipkow@10213
     2
    ID:         $Id$
nipkow@10213
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@10213
     4
    Copyright   1992  University of Cambridge
nipkow@10213
     5
nipkow@10213
     6
Relfexive and Transitive closure of a relation
nipkow@10213
     7
nipkow@10213
     8
rtrancl is reflexive/transitive closure;
nipkow@10213
     9
trancl  is transitive closure
nipkow@10213
    10
reflcl  is reflexive closure
nipkow@10213
    11
wenzelm@10331
    12
These postfix operators have MAXIMUM PRIORITY, forcing their operands
wenzelm@10331
    13
to be atomic.
nipkow@10213
    14
*)
nipkow@10213
    15
wenzelm@10980
    16
theory Transitive_Closure = Lfp + Relation
wenzelm@10980
    17
files ("Transitive_Closure_lemmas.ML"):
nipkow@10213
    18
nipkow@10213
    19
constdefs
wenzelm@10331
    20
  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
wenzelm@10331
    21
  "r^* == lfp (%s. Id Un (r O s))"
nipkow@10213
    22
wenzelm@10331
    23
  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
wenzelm@10331
    24
  "r^+ ==  r O rtrancl r"
nipkow@10213
    25
nipkow@10213
    26
syntax
wenzelm@10331
    27
  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
nipkow@10213
    28
translations
nipkow@10213
    29
  "r^=" == "r Un Id"
nipkow@10213
    30
wenzelm@10827
    31
syntax (xsymbols)
wenzelm@10331
    32
  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
wenzelm@10331
    33
  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
wenzelm@10331
    34
  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
wenzelm@10331
    35
wenzelm@10980
    36
use "Transitive_Closure_lemmas.ML"
wenzelm@10980
    37
nipkow@10213
    38
end