我想证明伊莎贝尔中类似的引理
\n\nlemma assumes "y = (THE x. P x)" shows "P (THE x. P x)"\n我想这个假设意味着THE x. P x存在并且是明确定义的。所以这个引理也应该是正确的
lemma assumes "y = (THE x. P x)" shows "\xe2\x88\x83! x. P x"\n我不知道如何证明这一点，因为我已经查看了当我在 Isabelle 的查询框中输入“name: the”时出现的所有定理，但它们似乎没有用。我找不到THE两者的定义，也不知道如何定义它，尽管我对它的含义有一个直观的想法。我尝试过类似的事情，尽管我确信这是错误的
"(\xe2\x88\x83!x. P x) \xe2\x9f\xb9 THE x. P x = (SOME x. P x)"\n甚至可能没用，因为我也不知道如何定义SOME！
不幸的是，这个假设并不意味着\ THE x. P xxe2\x80\x98exists\xe2\x80\x99 ，至少在某种意义上你不会感到满意。由于 HOL 是一个全逻辑，因此逻辑中不存在 \xe2\x80\x98well-definitionness\xe2\x80\x99 的概念。
THE x. P x如果您在没有x满足 的唯一值时写入P，那么仍然THE x. P x 是HOL 中 \xe2\x80\x98exists\xe2\x80\x99 的值，但您无法证明任何有意义的值（很像常量undefined），而且肯定不是其中之一P成立。对于 也是如此SOME，与 基本相同，THE区别在于对于，财产THE必须有唯一的SOME见证人，并且不需要唯一性。
显示某事的典型方法SOME x. P x是，您首先显示证人存在（即\xe2\x88\x83x. P x），然后将其插入到规则中someI_ex，然后告诉您P (SOME x. P x)确实成立。
与 相同THE，只是您必须证明只有一个证人 \xe2\x80\x93 这就是其含义\xe2\x88\x83!（参见定理Ex1_def）。显示这种独特的存在可以通过例如规则ex_ex1I或来完成ex1I。然后您可以将该事实插入theI'并the1_equality获得您想要的结果。
顺便说一下，常量 forSOME被称为Eps（如 \xe2\x80\x98Hilbert 的 \xce\xb5 运算符\xe2\x80\x99 中所示），其他的是The和Ex1。如果您输入 eg term Eps，您可以按住 Ctrl 键单击Eps，它会将您带到其定义（或者，在 的情况下，Eps更The确切地说是它们的公理化）。
还有一个LEAST自然数组合器，SOME它LeastI_ex与Least_le。
另一个旁注：这种想法，仅仅因为你可以写下一个术语，它不一定是直观意义上的 \xe2\x80\x98well-define\xe2\x80\x99 在 Isabelle 中很常见：你可以除以零，你可以写下不可微函数的导数、不可测集的测度、不可积函数的积分等。然后你会得到某种虚拟值（例如 0 表示除以零或完全除以其他值）荒谬的喜欢THE x. False）一样荒谬，但大多数讨论导数、积分等实际属性的定理确实明确要求该事物实际上是明确定义的。