src/HOL/Trancl.thy
author clasohm
Thu, 19 Oct 1995 13:25:03 +0100
changeset 1287 84f44b84d584
parent 1128 64b30e3cc6d4
child 1301 42782316d510
permissions -rw-r--r--
corrected spelling of title (to test new CVS loginfo)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1287
84f44b84d584 corrected spelling of title (to test new CVS loginfo)
clasohm
parents: 1128
diff changeset
     1
(*  Title: 	HOL/Trancl.thy
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents: 972
diff changeset
     6
Relfexive and Transitive closure of a relation
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents: 972
diff changeset
     8
rtrancl is refl&transitive closure;  trancl is transitive closure
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents: 972
diff changeset
    11
Trancl = Lfp + Relation + 
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
consts
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
    rtrancl :: "('a * 'a)set => ('a * 'a)set"	("(_^*)" [100] 100)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
    trancl  :: "('a * 'a)set => ('a * 'a)set"	("(_^+)" [100] 100)  
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
defs   
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
rtrancl_def	"r^* == lfp(%s. id Un (r O s))"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
trancl_def	"r^+ == r O rtrancl(r)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
end