src/HOL/Trancl.thy
author paulson
Thu Apr 04 11:45:01 1996 +0200 (1996-04-04)
changeset 1642 21db0cf9a1a4
parent 1558 9c6ebfab4e05
child 1916 43521f79f016
permissions -rw-r--r--
Using new "Times" infix
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
clasohm@923
    11
*)
clasohm@923
    12
nipkow@1128
    13
Trancl = Lfp + Relation + 
clasohm@1558
    14
clasohm@1558
    15
constdefs
clasohm@1558
    16
  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [100] 100)
clasohm@1558
    17
  "r^*  ==  lfp(%s. id Un (r O s))"
clasohm@1558
    18
clasohm@1558
    19
  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [100] 100)
clasohm@1558
    20
  "r^+  ==  r O rtrancl(r)"
clasohm@1558
    21
nipkow@1301
    22
syntax
clasohm@1558
    23
  reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
clasohm@1558
    24
nipkow@1301
    25
translations
clasohm@1558
    26
  "r^=" == "r Un id"
clasohm@1558
    27
clasohm@923
    28
end