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