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
```