Wie verwende ich die THE-Syntax in Isabelle / HOL?
Ich versuche zu lernen, wie man die THE
Syntax in Isabelle / HOL (2020) verwendet. Im Tutorial main.pdf gibt es:
The basic logic: x = y, True, False, ¬ P, P ∧ Q, P ∨ Q, P −→ Q, ∀ x. P,
∃ x. P, ∃!x. P, THE x. P.
Ich kann verstehen, was die anderen bedeuten, aber nicht das letzte "THE x. P". Meine beste Vermutung ist "das (vielleicht einzigartige) x, das die Eigenschaft P erfüllt". Also habe ich versucht, ein Spielzeug-Lemma wie folgt zu formulieren:
lemma "0 = THE x::nat. (x ≥ 0 ∧ x ≤ 0)"
Dies bedeutet, dass das x, das sowohl ge als auch le 0 ist, 0 ist.
Aber ich bekomme einen Fehler in Isabelle / jEdit mit einem Highlight auf dem Wort "THE".
Ich habe versucht, mit den Schlüsselwörtern Isabelle und "THE" zu suchen, aber offensichtlich wird das Wort "THE" von Suchmaschinen ignoriert. Daher die Frage hier.
Kann jemand helfen, die Bedeutung und Verwendung der "THE" -Syntax zu erklären, hoffentlich anhand des Beispiels hier?
Antworten
Sie benötigen mehr Klammern.
lemma "0 = (THE x::nat. (x ≥ 0 ∧ x ≤ 0))"
(*the proof*)
using theI[of ‹λx::nat. (x ≥ 0 ∧ x ≤ 0)› 0]
by auto
SOME (bzw. THE) ist (eine Variante von) Hilberts epsilon-Operator, der ein (the) -Element zurückgibt, das eine bestimmte Eigenschaft respektiert. Wenn keine (keine oder mehr als eine) vorhanden ist, wird ein nicht angegebenes Element zurückgegeben.
EINIGE und DIE sind nicht ausführbar. Sie sind selten nützlich für Anfänger.