如何使用Isabelle/HOL中的" the“语法？

Question

我正在尝试学习如何在Isabelle/HOL (2020)中使用THE语法。在tutorial main.pdf中，有：

The basic logic: x = y, True, False, ¬ P, P ∧ Q, P ∨ Q, P −→ Q, ∀ x. P,
∃ x. P, ∃!x. P, THE x. P.

我能理解其他人的意思，但不能理解最后一个"THE x.p“。我最好的猜测是“满足属性P的(可能是唯一的)x”。所以我试着把一个玩具引理说成：

lemma "0 = THE x::nat. (x ≥ 0 ∧ x ≤ 0)"

，这意味着既是ge又是le 0的x是0。

但是我在Isabelle/jEdit中得到了一个错误，突出显示了" the“这个单词。

我试着用关键字Isabelle和" the“搜索，但很明显" the”这个词被搜索引擎忽略了。因此这里就有了这个问题。

有没有人能帮我解释一下" the“语法的含义和用法，最好是这里的例子？

Answer 1

你需要更多的括号。

lemma "0 = (THE x::nat. (x ≥ 0 ∧ x ≤ 0))"
  (*the proof*)
  using theI[of ‹λx::nat. (x ≥ 0 ∧ x ≤ 0)› 0]
  by auto

一些(分别为)是希尔伯特的epsilon运算符的(变体)，它返回符合特定属性的()元素。如果不存在(不存在或存在多个)，则返回未指定的元素。

有些和是不可执行的。对于初学者来说，它们很少有用。