isabelle - 在 Isabelle 中计算关系运算符时如何处理 "exception Match raised"？

Question

我无法正确使用关系运算符 refl在伊莎贝尔 (2020) 的主要内容中。我假设 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")

Answer 1

您不应该期望能够使用 value 评估所有内容。 . value command 是一个诊断命令，玩起来很有趣，偶尔会有用，但 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 的实现(“对于集合 x 的所有元素 x， P(x) 持有”运算符)不知道如何处理 List.coset .
这里的一个快速解决方法是添加 (UNIV :: bool set) = {True, False}作为 code_unfold规则，以便代码生成器使用它。有了它，它就起作用了!

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