How to use the "THE" syntax in Isabelle/HOL?

I am trying to learn how to use the THE syntax in Isabelle/HOL (2020). In the tutorial main.pdf, there is:

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

I can understand what the others mean, but not the last one "THE x. P". My best guess is "the (maybe unique) x that satisfy property P". So I tried to state a toy lemma as follows:

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

, which means that the x that is both ge and le 0 is 0.

But I get an error in Isabelle/jEdit with a highlight on the "THE" word.

I tried to search with the keywords Isabelle and "THE", but obviously the word "THE" is ignored by search engines. Hence the question here.

Can someone help explain the meaning and use of the "THE" syntax, hopefully with the example here?

Solution

You need more parentheses.

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) is (a variant of) Hilbert's epsilon operator that returns a (the) element that respects a certain property. If none (none or more than one) exist, an underspecified element is returned.

SOME and THE are not executable. They are rarely useful for beginners.