Re: [isabelle] Relation of function absent from Main

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.


On 20 Feb 2021, at 18:12, Tobias Nipkow <nipkow at> wrote:

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.


On 19/02/2021 18:38, Christian Pardillo Laursen wrote:
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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.