Re: [isabelle] Relation of function absent from Main

Tobias Nipkow <nipkow at in.tum.de> · Sat, 20 Feb 2021 18:12:09 +0100

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

On 19/02/2021 18:38, Christian Pardillo Laursen wrote:

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

smime.p7s