Email Gateway (Aug 18 2022 at 12:21): Email Gateway (Aug 18 2022 at 12:21):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Transitive_Closure.thy defines
inductive_set
trancl :: "('a × 'a) set => ('a × 'a) set" ("(_^+)" [1000] 999)
for r :: "('a × 'a) set"
where
r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
| trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==>
(b, c) : r ==> (a, c) : r^+"
but this doesn't seem to work right with new style relations, e.g.
term "(less :: nat => nat => bool)^+"
produces a type error. Is there a transitive closure operator for new
style relations?
Thanks,
Randy
Email Gateway (Aug 18 2022 at 12:21):From: Amine Chaieb <chaieb@in.tum.de>
The type is not correct -- you need st of type 'a * 'a set. You need to
uncurry "less".
trancl (split less) should work.
Amine.
Randy Pollack wrote:
Email Gateway (Aug 18 2022 at 12:21):From: Alexander Krauss <krauss@in.tum.de>
Is there a transitive closure operator for new
style relations?
Yes. The curried versions of these predicates are "tranclp", "rtranclp"
etc. Syntax: "^++", "^**"
Alex
Last updated: May 03 2024 at 12:27 UTC