Isabelle/HOL中的undefined

Question

我试图在 Isabelle/HOL 中证明这个引理。但是 nitpick 找到了反例，既对这个引理也对其否定。

lemma "(0::nat) ≠ undefined"

这怎么可能呢？我查了一下 undefined 的定义，发现它是一个公理：

axiomatization undefined :: 'a

但这还是经典逻辑，对吧？所以要么 "(0::nat) = undefined" 成立，要么 "(0::nat) ≠ undefined" 成立。

背景：

我有一个类型为：

type_synonym myfun = "nat ⇒ nat"

的函数，并在 locale 中对其值域和定义域施加约束。当我试图取一个特定的函数并展示它满足所有条件时，我遇到了问题，因为其中一些条件仅对非 undefined 值成立。

提前感谢你的帮助 :)

- DianaPrince

Answer 1

通过公理化，每种类型都有一个指定值是 undefined。这不是某个生活在该类型正常范围之外的单独值，即 undefined :: nat 是自然数，但你不知道它是哪个自然数，而且实际上你将无法证明任何与 undefined 相关的非平凡属性。在这个上下文中，平凡属性是适用于该类型的所有值的属性。

因此，在 Isabelle/HOL 中，语句 undefined ≠ (0 :: nat) 不能被证明，它的否定也不能（除了错误和不一致性）。

特别地，对于 undefined :: bool，我们知道 undefined = True ∨ undefined = False，但同样，你将无法证明 undefined = True 或 undefined = False。

然而，对于单位类型（仅由值 () :: unit 组成的单元素类型），你可以证明 undefined = ()，因为这是一个平凡属性。

至于你原来的问题，听起来好像你需要更改你的应用程序中未定义性的建模方式。由于你没有提供任何关于你正在做什么的细节，所以无法就该怎么做给出具体建议。但是试图证明任何关于 undefined 的东西都是行不通的。

- Manuel Eberl

---

非常感谢，这对我帮助很大。现在我已经将值映射为0而不是未定义。抱歉，我的意思是 (0::nat) = undefined 或者 (0::nat) ≠ undefined 应该成立。我已经编辑了上面的问题。 - DianaPrince

是的，选择一个合适的虚拟值（比如0）而不是undefined通常可以让你的生活更轻松。我会更新我的答案，删除涉及该笔误的部分。 - Manuel Eberl

你可以轻松证明 lemma "undefined = (0::nat) ∨ undefined ≠ (0::nat)" by blast。 - ammbauer