如何在 Isabelle 中对“布尔值”进行归纳定义

Question

在 Isabelle 中，我想定义接受谓词 'a => bool 的运算符，并根据“谓词的归纳结构”修改它们。例如，有人可能想要在这些谓词上计算 Disjunctive Normal Form (DNF)，例如D (λ x. P x --> Q x) = (λ x. ¬ P x \/ Q x).

这里的问题是bool 不是归纳数据类型。我想到了两种可能的解决方案：

1. 创建一个归纳数据类型，允许我在它们上定义我的运算符。为这个数据类型提供谓词 (P::'a => bool) 语义，然后用它来证明我要检查的引理。
2. 证明每个可能的归纳情况的定理。然后展示一个使用上述所有规则的一般案例。

作为第三种选择，我（希望）希望更有经验的 Isabelle 用户可以用一个绕过这个“归纳问题”的秘密函数/typedef 来启发我的方法。所以这里的问题是：

还有其他更简单的选择吗？如果是，是哪些？如果没有，我的任何方法是否看起来有缺陷或注定失败？

警告：我举了一个例子，DNF，但是，运算符不一定保留谓词的真值的一般情况对我来说更感兴趣，例如D 可以这样做：D (λ x. P x /\ Q x) = (λ x. P x \/ Q x)。

Answer 1

HOL 函数无法查看其参数的句法表示。原因是替换公理，即逻辑上相等的项可以在任何上下文中替换。否则，可以定义一个满足D (λ x. P x) = True 和D (λ x. P x & True) = False 的函数D，从而得到False 的证明。

对于像转换为 DNF 这样的函数，其在 HOL 中的语义不依赖于参数的语法，仍然可以定义这样的转换。对于 DNF 转换，语义操作是恒等式，即，

definition DNF :: "('a => bool) => ('a => bool)" where "D = id"

然后，您可以派生实际执行转换的重写规则。例如，

lemma DNF_imp: "DNF (λx. P x --> Q x) = DNF (λx. ~ P x | Q x)"

如果您使用这样一组专用规则调用 Isabelle 的简化器，您将有效地转换为 DNF（尽管您永远无法在 HOL 中正式表示您的规则集适用于所有情况）。

很多时候，像DNF_imp 这样的规则不足以实现这样的功能。在这种情况下，您可以在 Isabelle/ML 中编写一个 simproc，它在 DNF _ 术语上触发并执行转换。由于您正在跳出逻辑，因此 simproc 可以查看参数的 HOL 语法，并在逻辑上相等的条件下表现出不同的行为。

相反，如果您确实想在逻辑中表达和推理转换函数D，则无法像您建议的数据类型那样引入要处理的语法。