src/HOL/Trancl.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1916 43521f79f016
child 3499 ce1664057431
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@1475
     1
(*  Title:      HOL/Trancl.thy
clasohm@923
     2
    ID:         $Id$
clasohm@1475
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1992  University of Cambridge
clasohm@923
     5
nipkow@1128
     6
Relfexive and Transitive closure of a relation
clasohm@923
     7
paulson@1642
     8
rtrancl is reflexive/transitive closure;
paulson@1642
     9
trancl  is transitive closure
paulson@1642
    10
reflcl  is reflexive closure
paulson@1916
    11
paulson@1916
    12
These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
paulson@1916
    13
      atomic.
clasohm@923
    14
*)
clasohm@923
    15
nipkow@1128
    16
Trancl = Lfp + Relation + 
clasohm@1558
    17
clasohm@1558
    18
constdefs
paulson@1916
    19
  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 1000)
clasohm@1558
    20
  "r^*  ==  lfp(%s. id Un (r O s))"
clasohm@1558
    21
paulson@1916
    22
  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 1000)
clasohm@1558
    23
  "r^+  ==  r O rtrancl(r)"
clasohm@1558
    24
nipkow@1301
    25
syntax
paulson@1916
    26
  reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 1000)
clasohm@1558
    27
nipkow@1301
    28
translations
clasohm@1558
    29
  "r^=" == "r Un id"
clasohm@1558
    30
clasohm@923
    31
end