| author | clasohm |
| Mon, 05 Feb 1996 21:27:16 +0100 | |
| changeset 1475 | 7f5a4cd08209 |
| parent 1301 | 42782316d510 |
| child 1558 | 9c6ebfab4e05 |
| permissions | -rw-r--r-- |
| 1475 | 1 |
(* Title: HOL/Trancl.thy |
| 923 | 2 |
ID: $Id$ |
| 1475 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
| 923 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
972
diff
changeset
|
6 |
Relfexive and Transitive closure of a relation |
| 923 | 7 |
|
| 1301 | 8 |
rtrancl is refl&transitive closure; |
9 |
trancl is transitive closure |
|
10 |
reflcl is reflexive closure |
|
| 923 | 11 |
*) |
12 |
||
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
972
diff
changeset
|
13 |
Trancl = Lfp + Relation + |
| 923 | 14 |
consts |
| 1475 | 15 |
rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100)
|
16 |
trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
|
|
| 1301 | 17 |
syntax |
18 |
reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [100] 100)
|
|
| 923 | 19 |
defs |
| 1475 | 20 |
rtrancl_def "r^* == lfp(%s. id Un (r O s))" |
21 |
trancl_def "r^+ == r O rtrancl(r)" |
|
| 1301 | 22 |
translations |
23 |
"r^=" == "r Un id" |
|
| 923 | 24 |
end |