src/HOL/Trancl.thy
author nipkow
Wed Oct 25 09:48:29 1995 +0100 (1995-10-25)
changeset 1301 42782316d510
parent 1287 84f44b84d584
child 1475 7f5a4cd08209
permissions -rw-r--r--
Added various thms and tactics.
clasohm@1287
     1
(*  Title: 	HOL/Trancl.thy
clasohm@923
     2
    ID:         $Id$
clasohm@923
     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
nipkow@1301
     8
rtrancl is refl&transitive closure;
nipkow@1301
     9
trancl is transitive closure
nipkow@1301
    10
reflcl is reflexive closure
clasohm@923
    11
*)
clasohm@923
    12
nipkow@1128
    13
Trancl = Lfp + Relation + 
clasohm@923
    14
consts
clasohm@923
    15
    rtrancl :: "('a * 'a)set => ('a * 'a)set"	("(_^*)" [100] 100)
clasohm@923
    16
    trancl  :: "('a * 'a)set => ('a * 'a)set"	("(_^+)" [100] 100)  
nipkow@1301
    17
syntax
nipkow@1301
    18
    reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
clasohm@923
    19
defs   
nipkow@1301
    20
  rtrancl_def	"r^*  ==  lfp(%s. id Un (r O s))"
nipkow@1301
    21
  trancl_def	"r^+  ==  r O rtrancl(r)"
nipkow@1301
    22
translations
nipkow@1301
    23
                "r^=" == "r Un id"
clasohm@923
    24
end