src/CCL/Trancl.thy
changeset 1474 3f7d67927fe2
parent 0 a5a9c433f639
child 17456 bcf7544875b2
     1.1 --- a/src/CCL/Trancl.thy	Mon Feb 05 13:44:28 1996 +0100
     1.2 +++ b/src/CCL/Trancl.thy	Mon Feb 05 14:44:09 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	CCL/trancl.thy
     1.5 +(*  Title:      CCL/trancl.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  Transitive closure of a relation
    1.12 @@ -9,20 +9,20 @@
    1.13  Trancl = CCL +
    1.14  
    1.15  consts
    1.16 -    trans   :: "i set => o" 	              (*transitivity predicate*)
    1.17 -    id	    :: "i set"
    1.18 -    rtrancl :: "i set => i set"	              ("(_^*)" [100] 100)
    1.19 -    trancl  :: "i set => i set"	              ("(_^+)" [100] 100)  
    1.20 -    O	    :: "[i set,i set] => i set"       (infixr 60)
    1.21 +    trans   :: "i set => o"                   (*transitivity predicate*)
    1.22 +    id      :: "i set"
    1.23 +    rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
    1.24 +    trancl  :: "i set => i set"               ("(_^+)" [100] 100)  
    1.25 +    O       :: "[i set,i set] => i set"       (infixr 60)
    1.26  
    1.27  rules   
    1.28  
    1.29 -trans_def	"trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    1.30 -comp_def	(*composition of relations*)
    1.31 -		"r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    1.32 -id_def		(*the identity relation*)
    1.33 -		"id == {p. EX x. p = <x,x>}"
    1.34 -rtrancl_def	"r^* == lfp(%s. id Un (r O s))"
    1.35 -trancl_def	"r^+ == r O rtrancl(r)"
    1.36 +trans_def       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    1.37 +comp_def        (*composition of relations*)
    1.38 +                "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    1.39 +id_def          (*the identity relation*)
    1.40 +                "id == {p. EX x. p = <x,x>}"
    1.41 +rtrancl_def     "r^* == lfp(%s. id Un (r O s))"
    1.42 +trancl_def      "r^+ == r O rtrancl(r)"
    1.43  
    1.44  end