未定义于Isabelle/HOL中

Question

我在伊莎贝尔/霍尔试图证明这个引理。

lemma "(0::nat) ≠ undefined"

但是nitpick找到了反例来证明这一点和它的否定

lemma "(0::nat) = undefined"

这怎麽可能？我查看了未定义的定义是如何定义的，这是一个公理：

axiomatization undefined :: 'a

但这仍然是经典逻辑，对吧？因此，无论是"(0::nat) = undefined"还是"(0::nat) ≠ undefined"都应该是真的。

背景：

我有一个类型的函数：

type_synonym myfun = "nat ⇒ nat"

我在区域设置中对它的图像和域施加限制。当我尝试接受一个特定的函数并显示它满足了区域设置中的所有条件时，我遇到了问题，因为有些条件只适用于未定义的值。

(预先谢谢:)

Answer 1

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

因此，undefined ≠ (0 :: nat)语句在Isabelle/HOL中是不可证明的，它的否定(bug和不一致除外)也是不可证明的。

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

但是，对于单元类型(仅由值() :: unit组成的单元素类型)，可以证明undefined = ()，因为这是一个微不足道的属性。

至于您最初的问题，听起来好像您必须改变您在应用程序中建模不确定的方式。因为你没有给出任何细节，你正在做什么，这是不可能给出任何具体的建议，以做什么。但是试图证明关于undefined的任何东西都是行不通的。