[isabelle] Relation of function absent from Main

To: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
Subject: [isabelle] Relation of function absent from Main
From: Christian Pardillo Laursen <cp735 at cam.ac.uk>
Date: Fri, 19 Feb 2021 17:38:50 +0000
Accept-language: en-GB, en-US
Authentication-results: lists.cam.ac.uk; dkim=none (message not signed) header.d=none; lists.cam.ac.uk; dmarc=none action=none header.from=cam.ac.uk;
Thread-index: AQHXBuInsWpj246j+kSyXMhXnUcjdQ==
Thread-topic: Relation of function absent from Main

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

Follow-Ups:
- Re: [isabelle] Relation of function absent from Main
  - From: Tobias Nipkow

Previous by Date: [isabelle] 2nd CfP ThEdu'21
Next by Date: [isabelle] 14th Conference on Intelligent Computer Mathematics (CICM 2021), Invited Speakers Update & Second call for papers, Conference Date: July 26-31, 2021
Previous by Thread: [isabelle] 2nd CfP ThEdu'21
Next by Thread: Re: [isabelle] Relation of function absent from Main
Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
Cl-isabelle-users list archive Table of Contents
More information about the Cl-isabelle-users mailing list

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