1 (* Title: CCL/trancl.thy |
1 (* Title: CCL/trancl.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Transitive closure of a relation |
6 Transitive closure of a relation |
7 *) |
7 *) |
8 |
8 |
9 Trancl = CCL + |
9 Trancl = CCL + |
10 |
10 |
11 consts |
11 consts |
12 trans :: "i set => o" (*transitivity predicate*) |
12 trans :: "i set => o" (*transitivity predicate*) |
13 id :: "i set" |
13 id :: "i set" |
14 rtrancl :: "i set => i set" ("(_^*)" [100] 100) |
14 rtrancl :: "i set => i set" ("(_^*)" [100] 100) |
15 trancl :: "i set => i set" ("(_^+)" [100] 100) |
15 trancl :: "i set => i set" ("(_^+)" [100] 100) |
16 O :: "[i set,i set] => i set" (infixr 60) |
16 O :: "[i set,i set] => i set" (infixr 60) |
17 |
17 |
18 rules |
18 rules |
19 |
19 |
20 trans_def "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)" |
20 trans_def "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)" |
21 comp_def (*composition of relations*) |
21 comp_def (*composition of relations*) |
22 "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}" |
22 "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}" |
23 id_def (*the identity relation*) |
23 id_def (*the identity relation*) |
24 "id == {p. EX x. p = <x,x>}" |
24 "id == {p. EX x. p = <x,x>}" |
25 rtrancl_def "r^* == lfp(%s. id Un (r O s))" |
25 rtrancl_def "r^* == lfp(%s. id Un (r O s))" |
26 trancl_def "r^+ == r O rtrancl(r)" |
26 trancl_def "r^+ == r O rtrancl(r)" |
27 |
27 |
28 end |
28 end |