Come utilizzare la sintassi "THE" in Isabelle / HOL?

Question

Sto cercando di imparare a usare la THEsintassi in Isabelle / HOL (2020). Nel tutorial main.pdf, c'è:

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

Posso capire cosa significano gli altri, ma non l'ultimo "THE x. P". La mia ipotesi migliore è "la (forse unica) x che soddisfa la proprietà P". Quindi ho provato a dichiarare un lemma giocattolo come segue:

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

, il che significa che la x che è sia ge che le 0 è 0.

Ma ottengo un errore in Isabelle / jEdit con un'evidenziazione sulla parola "THE".

Ho provato a cercare con le parole chiave Isabelle e "THE", ma ovviamente la parola "THE" viene ignorata dai motori di ricerca. Da qui la domanda qui.

Qualcuno può aiutare a spiegare il significato e l'uso della sintassi "THE", si spera con l'esempio qui?

Answer 1

Hai bisogno di più parentesi.

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

ALCUNI (rispettivamente THE) è (una variante di) l'operatore epsilon di Hilbert che restituisce un (l'elemento) che rispetta una certa proprietà. Se nessuno (nessuno o più di uno) esiste, viene restituito un elemento sottospecificato.

ALCUNI e THE non sono eseguibili. Raramente sono utili per i principianti.