src/HOL/Transitive_Closure.thy
author nipkow
Thu Oct 12 18:44:35 2000 +0200 (2000-10-12)
changeset 10213 01c2744a3786
child 10331 7411e4659d4a
permissions -rw-r--r--
*** empty log message ***
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
nipkow@10213
    12
These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
nipkow@10213
    13
      atomic.
nipkow@10213
    14
*)
nipkow@10213
    15
nipkow@10213
    16
Transitive_Closure = Lfp + Relation + 
nipkow@10213
    17
nipkow@10213
    18
constdefs
nipkow@10213
    19
  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
nipkow@10213
    20
  "r^*  ==  lfp(%s. Id Un (r O s))"
nipkow@10213
    21
nipkow@10213
    22
  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
nipkow@10213
    23
  "r^+  ==  r O rtrancl(r)"
nipkow@10213
    24
nipkow@10213
    25
syntax
nipkow@10213
    26
  "_reflcl"  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
nipkow@10213
    27
nipkow@10213
    28
translations
nipkow@10213
    29
  "r^=" == "r Un Id"
nipkow@10213
    30
nipkow@10213
    31
end