Email Gateway (Feb 20 2021 at 10:57): Email Gateway (Feb 20 2021 at 10:57):From: Christian Pardillo Laursen <cp735@cam.ac.uk>
Hello,
I have been using the following function extensively:
definition rel_of :: "('a ⇒ 'a) ⇒ 'a rel" where "rel_of f = {(x,y) . f x = y}"
This seems to be absent from the Isabelle libraries, despite being obvious. Am I missing something, or is it perhaps a bad idea to convert between functions and relations?
Best regards,
Christian Pardillo Laursen
Email Gateway (Feb 20 2021 at 17:12):From: Tobias Nipkow <nipkow@in.tum.de>
It doesn't sound like a bad idea, and I seem to remember that I once toyed with
adding it, but the fact that nobody ever added it indicates that it may not be
worth it, i.e. that you can work with the set comprehension just as easily. But
that is not clear.
Tobias
smime.p7s
Email Gateway (Feb 20 2021 at 21:57):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Tobias, hi Christian,
There is already the more general Gr (graph of a function) notion and its counterpart that returns a predicate in Main:
definition "Gr A f = {(a, f a) | a. a ∈ A}"
definition "Grp A f = (λa b. b = f a ∧ a ∈ A)”
These constants were originally used internally by the datatype package and are therefore only accessible by their long names (BNF_Def.Gr). Still, they were “found” by users and now there are already a couple of occurrences in the AFP. If they are deemed useful, one can reconsider their internal status and potentially find better “public" names for them.
Dmitriy
Last updated: Jul 15 2022 at 23:21 UTC