author | nipkow |
Wed, 25 Oct 1995 09:48:29 +0100 | |
changeset 1301 | 42782316d510 |
parent 1287 | 84f44b84d584 |
child 1475 | 7f5a4cd08209 |
permissions | -rw-r--r-- |
1287
84f44b84d584
corrected spelling of title (to test new CVS loginfo)
clasohm
parents:
1128
diff
changeset
|
1 |
(* Title: HOL/Trancl.thy |
923 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
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 |
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 |
1301 | 20 |
rtrancl_def "r^* == lfp(%s. id Un (r O s))" |
21 |
trancl_def "r^+ == r O rtrancl(r)" |
|
22 |
translations |
|
23 |
"r^=" == "r Un id" |
|
923 | 24 |
end |