Isabelle / HOLで「THE」構文を使用するにはどうすればよいですか？

Question

THEIsabelle / HOL（2020）の構文の使い方を学ぼうとしています。チュートリアル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.

他の意味は理解できますが、最後の「THEx.P」は理解できません。私の最善の推測は、「プロパティPを満たす（おそらく一意の）x」です。だから私はおもちゃの補題を次のように述べようとしました：

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

、これは、geとle0の両方である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

SOME（またはTHE）は、特定のプロパティを尊重する（the）要素を返すHilbertのイプシロン演算子（の変形）です。存在しない（存在しない、または複数）場合、指定不足の要素が返されます。

SOMEとTHEは実行可能ではありません。初心者にはめったに役に立ちません。