Isabelle 对二元谓词表示的关系有什么支持？答案

【问题标题】：What support does Isabelle have for relations represented by binary predicates?Isabelle 对二元谓词表示的关系有什么支持？
【发布时间】：2018-04-25 21:31:33
【问题描述】：

在 Isabelle 形式化中，我用二元谓词表示关系。我想让运算符使用这种表示来执行典型的关系运算，例如合成和反转。

文档“What's in Main”只提到了这样的运算符，用于表示成对的集合。 Relation 理论在一开始就说，“关系——作为成对的集合和二元谓词”。但是，我在这个理论中找不到对二元谓词表示的太多支持。我只找到了几个带有神秘pred_set_conv 属性的引理。

是否广泛支持由二元谓词表示的关系？特别是，是否定义了通用关系操作的运算符？这些东西记录在哪里？

【问题讨论】：

为什么不直接定义自己的合成和反转（以及其他需要的操作）？这似乎很容易。我知道，这可能就像重新发明轮子（如果已经存在合适的关系理论/库），但在这种情况下，“轮子”似乎是一个非常简单的轮子，并且您可以独立于外部库/理论。
或者您是否需要关于这些操作的复杂引理或定理，您宁愿从库/理论中重用而不是证明自己？
我不想使用我自己的定义，因为这会使代码不规范，因此不太容易理解。我不认为独立于外部理论很重要。事实上，我通常认为重新发明轮子会更糟。在这种特殊情况下，它甚至不依赖于某些第三方库，而是依赖于核心库，它应该是相当知名、稳定和持久的。

标签： isabelle

【解决方案1】：

对作为对集合的关系的支持比对二元谓词的支持稍好一些，但可用的东西很多。然而，许多关系操作是对函数和谓词的更一般操作的实例，或者它们确实是使用pred_set_conv 获得的。因此，它们可能很难找到。使用find_theorems 命令或面板来查找引理。以下是常用操作的简要总结：

组成：relcompp（中缀OO）
逆：conversep（符号_\<inverse>\<inverse>）
（自反）传递闭包：tranclp 和 rtranclp
交叉点：inf
工会：sup
包含：op <=（我发现引理 predicate2I 和 predicate2D 特别有用）
受限于域的函数图：BNF_Def.Grp
两个函数下的逆图像：BNF_Def.vimage2p
有充分根据和可访问性：wfP 和 accp

【讨论】：

非常感谢。这已经非常有用了。您能否详细说明pred_set_conv？通过搜索标准库源代码，我了解到将归纳谓词和归纳集联系起来是HOL的一些核心属性。但是，Isabelle/Isar 参考手册中没有记录。这个谓词是关于什么的？它记录在哪里？
交集和并集也有问题。 inf 和 sup 函数似乎不适用于二元谓词（类型为 'a ⇒ 'b ⇒ bool 的谓词），仅适用于一元谓词。 Isabelle 抱怨'b ⇒ bool 类型不是semilattice_inf。此外，在我的理论中，Isabelle 不接受 inf 和 sup 的符号 ⊓ 和 ⊔，尽管 HOL.Relation 中使用了这个符号。这是为什么呢？
我将\<converse> 更正为\<inverse>。然而，已经有两位同行评审拒绝了这一更正。原因？ “这次编辑偏离了帖子的初衷。即使是必须做出重大改变的编辑也应该努力维护帖子所有者的目标。”不用说，从他们的个人资料来看，这些评论者似乎对伊莎贝尔一无所知。我猜他们甚至不知道 \<…> 是符号的表示，而目前符号 \<converse> 根本不存在。
尊敬的其他审阅者，如果您知道如何找到它，请先查看 Isabelle 库源代码，并意识到conversep 的符号使用\<inverse>，而不是\<converse>。
我或多或少地解决了inf 和sup 的问题。二进制谓词的问题只发生在value 之后。在引理语句中，一切正常。符号 ⊓ 和 ⊔ 在导入 HOL-Library.Lattice_Syntax 时可用。奇怪的是在HOL.Relation这个语法被成功使用了，虽然这个理论没有导入HOL-Library.Lattice_Syntax。