src/CCL/Trancl.thy
changeset 0 a5a9c433f639
child 1474 3f7d67927fe2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/Trancl.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,28 @@
     1.4 +(*  Title: 	CCL/trancl.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Transitive closure of a relation
    1.10 +*)
    1.11 +
    1.12 +Trancl = CCL +
    1.13 +
    1.14 +consts
    1.15 +    trans   :: "i set => o" 	              (*transitivity predicate*)
    1.16 +    id	    :: "i set"
    1.17 +    rtrancl :: "i set => i set"	              ("(_^*)" [100] 100)
    1.18 +    trancl  :: "i set => i set"	              ("(_^+)" [100] 100)  
    1.19 +    O	    :: "[i set,i set] => i set"       (infixr 60)
    1.20 +
    1.21 +rules   
    1.22 +
    1.23 +trans_def	"trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    1.24 +comp_def	(*composition of relations*)
    1.25 +		"r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    1.26 +id_def		(*the identity relation*)
    1.27 +		"id == {p. EX x. p = <x,x>}"
    1.28 +rtrancl_def	"r^* == lfp(%s. id Un (r O s))"
    1.29 +trancl_def	"r^+ == r O rtrancl(r)"
    1.30 +
    1.31 +end