如何在 Isabelle/HOL 中使用“THE”语法？答案

【问题标题】：How to use the "THE" syntax in Isabelle/HOL?如何在 Isabelle/HOL 中使用“THE”语法？
【发布时间】：2021-01-11 22:49:32
【问题描述】：

我正在尝试学习如何在 Isabelle/HOL (2020) 中使用 THE 语法。在教程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”语法的含义和用法，希望这里有例子吗？

【问题讨论】：

标签： isabelle

【解决方案1】：

你需要更多的括号。

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

SOME (resp. THE) 是 Hilbert 的 epsilon 运算符的（一个变体），它返回一个尊重某个属性的 (the) 元素。如果不存在（不存在或多于一个），则返回未指定的元素。

SOME 和 THE 不可执行。它们对初学者很少有用。

【讨论】：