isabelle - 在 Isabelle 中计算关系运算符时如何处理“引发异常匹配”？

Question

refl在 Isabelle (2020) 的 Main 中，我无法正确使用关系运算符。我假设refl如果关系是自反的，则返回 true，与refl_on上面的示例相同。但我仍在学习这些符号。

进一步来说：

value "refl_on {True,False} {(True,True),(False,False)}"

True按预期给出。我认为refl是相同的，但以下内容：

value "refl {(True,True),(False,False)}"

给出一个错误：

exception Match raised (line 39 of "generated code")

其他运营商，例如sym似乎没问题：

value "sym {(True,True)}"

在这里使用的正确方法是什么refl？

- 更新 -

似乎有一个类似的错误total：

value "total {(True,True),(False,False)}"

， 这使：

exception Match raised (line 39 of "generated code")

标签： isabelle

Answer 1

您不应该期望能够使用value. 该value命令是一个诊断命令，玩起来很有趣，有时也很有用，但 Isabelle/HOL 不是一种编程语言，如果没有额外的设置，您写下的大多数 HOL 术语都无法评估。

使评估成为可能的机制是代码生成器，它将 HOL 定义转换为可执行的 ML 代码，然后运行该代码并将结果转换回 HOL 术语。

在这种情况下，当然没有先验理由说明您不能评估该术语。当事情失败时，您可以使用export_code查看实际为您的术语生成的代码：

definition foo where "foo = refl {(True,True),(False,False)}"

export_code foo in SML

您可以查看代码生成器使用的“代码方程式”

definition foo where "foo = refl {(True,True),(False,False)}"

code_thms foo

可能有点难以阅读，但基本上问题在于，默认情况下，集合是通过列表实现的，或者作为set xs（列表的所有元素xs）或作为List.coset xs（不在列表中的所有元素xs）并且UNIV具有代码方程UNIV = List.coset []。（请注意，这refl只是 的缩写refl_on UNIV）。

不幸的是，Ball（'for all elements xof the set x，P(x)hold' 操作符）的实现不知道如何处理List.coset.

这里的一个快速解决方法是添加(UNIV :: bool set) = {True, False}一个code_unfold规则，以便代码生成器使用它。有了它，它就可以工作了！

lemma UNIV_bool [code_unfold]: "UNIV = {True, False}"
  by auto