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
|