在 Isabelle 中证明关于 THE 的直觉陈述
Proving intuitive statements about THE in Isabelle
我想证明 Isabelle 中类似这个引理的东西
lemma assumes "y = (THE x. P x)" shows "P (THE x. P x)"
我想这个假设意味着 THE x. P x 存在并且定义明确。所以这个引理也应该是真的
lemma assumes "y = (THE x. P x)" shows "∃! x. P x"
我不确定如何证明这一点，因为我已经查看了当我在 Isabelle 的查询框中键入 "name: the" 时出现的所有定理，但它们似乎没有用。我也找不到 THE 的定义，而且我不确定如何定义它，尽管我对它的含义有一个直观的认识。我尝试过这样的事情，尽管我确定这是错误的
"(∃!x. P x) ⟹ THE x. P x = (SOME x. P x)"
甚至可能没用，因为我也不知道如何定义 SOME！
不幸的是，这个假设并不暗示THE x. P x“存在”，至少在某种意义上你不会感到满意。由于 HOL 是一个完整的逻辑，因此逻辑中没有“明确定义”的概念。
如果在没有满足P的唯一x时写THE x. P x，那么THE x. P x仍然是 HOL 中“存在”的值，但您无法证明任何有意义的值（很像 undefined 常量），而且肯定不是 P 成立的值。 SOME也是一样，和THE基本一样，不同的是THE需要有一个unique witness 属性 和 SOME 不需要唯一性。
显示有关 SOME x. P x 的典型方法是首先显示证人存在（即 ∃x. P x），然后将其插入 someI_ex 之类的规则中，然后告诉你 P (SOME x. P x) 确实成立。
对于 THE 也是一样的，除了你必须证明确实有 一个 证人——这就是 ∃! 的意思（参见定理 Ex1_def)。可以显示这种独特的存在，例如使用规则 ex_ex1I 或 ex1I。然后您可以将该事实代入 theI' 和 the1_equality 以获得您想要的结果。
顺便说一句，SOME 的常量称为 Eps（如“希尔伯特的 ε 运算符”），其他的是 The 和 Ex1。如果您输入例如term Eps，您可以按住 Ctrl 并单击 Eps，它会将您带到它的定义（或者，在 Eps 和 The 的情况下，而不是它们的公理化）。
还有一个用于自然数的 LEAST 组合子，它与 SOME 非常相似，有时非常有用（它被称为“最小”，引理是 LeastI_ex 和 Least_le).
另一个旁注：这种认为仅仅因为你可以写下一个术语，它不一定在直觉意义上“定义明确”的想法在 Isabelle 中很常见：你可以除以零，你可以写下不可微分函数的导数、不可测集的测度、不可积函数的积分等。然后你会得到某种虚拟值（例如 0 表示被零除或完全荒谬的东西，比如 THE x. False)，但大多数讨论导数、积分等实际性质的定理确实明确要求该事物实际上是明确定义的。
我想证明 Isabelle 中类似这个引理的东西
lemma assumes "y = (THE x. P x)" shows "P (THE x. P x)"
我想这个假设意味着 THE x. P x 存在并且定义明确。所以这个引理也应该是真的
lemma assumes "y = (THE x. P x)" shows "∃! x. P x"
我不确定如何证明这一点，因为我已经查看了当我在 Isabelle 的查询框中键入 "name: the" 时出现的所有定理，但它们似乎没有用。我也找不到 THE 的定义，而且我不确定如何定义它，尽管我对它的含义有一个直观的认识。我尝试过这样的事情，尽管我确定这是错误的
"(∃!x. P x) ⟹ THE x. P x = (SOME x. P x)"
甚至可能没用，因为我也不知道如何定义 SOME！
不幸的是，这个假设并不暗示THE x. P x“存在”，至少在某种意义上你不会感到满意。由于 HOL 是一个完整的逻辑，因此逻辑中没有“明确定义”的概念。
如果在没有满足P的唯一x时写THE x. P x，那么THE x. P x仍然是 HOL 中“存在”的值，但您无法证明任何有意义的值（很像 undefined 常量），而且肯定不是 P 成立的值。 SOME也是一样，和THE基本一样，不同的是THE需要有一个unique witness 属性 和 SOME 不需要唯一性。
显示有关 SOME x. P x 的典型方法是首先显示证人存在（即 ∃x. P x），然后将其插入 someI_ex 之类的规则中，然后告诉你 P (SOME x. P x) 确实成立。
对于 THE 也是一样的，除了你必须证明确实有 一个 证人——这就是 ∃! 的意思（参见定理 Ex1_def)。可以显示这种独特的存在，例如使用规则 ex_ex1I 或 ex1I。然后您可以将该事实代入 theI' 和 the1_equality 以获得您想要的结果。
顺便说一句，SOME 的常量称为 Eps（如“希尔伯特的 ε 运算符”），其他的是 The 和 Ex1。如果您输入例如term Eps，您可以按住 Ctrl 并单击 Eps，它会将您带到它的定义（或者，在 Eps 和 The 的情况下，而不是它们的公理化）。
还有一个用于自然数的 LEAST 组合子，它与 SOME 非常相似，有时非常有用（它被称为“最小”，引理是 LeastI_ex 和 Least_le).
另一个旁注：这种认为仅仅因为你可以写下一个术语，它不一定在直觉意义上“定义明确”的想法在 Isabelle 中很常见：你可以除以零，你可以写下不可微分函数的导数、不可测集的测度、不可积函数的积分等。然后你会得到某种虚拟值（例如 0 表示被零除或完全荒谬的东西，比如 THE x. False)，但大多数讨论导数、积分等实际性质的定理确实明确要求该事物实际上是明确定义的。