在Isabelle/HOL中，可以找到以下公理化
axiomatization The :: "('a ⇒ bool) ⇒ 'a"
axiomatization undefined :: 'a
有什么原因不能使用吗
definition "undefined ≡ The (λx. False)"
还是这只是一件历史文物？似乎目前的方式导致了"；不同的"；不败的概念。当我按照的思路定义一些东西时，我偶然发现了这一点
definition "of_interest y ≡ (THE x. foobar x y)"
并想证明(事后看来愚蠢的(理智检查
lemma "(∄x. foobar x y) ⟹ of_interest y = undefined"
这在当前状态下显然不起作用，但应该通过上面对未定义的定义。
通过使用axiomatization机制，您可以清楚地声明，您不能对undefined :: 'a进行任何假设，但它是'a类型的任意但未知的值。相反，通过使用您的定义，您现在对undefined有了更多的了解，即它是The将λx. False映射到的值(Eps (λx. True)和类似的定义也是如此(。例如，使用您的定义，您可以证明The (λx. False) = undefined，而使用axiomatization无法证明。