Jak używać składni „THE” w Isabelle / HOL?
Próbuję nauczyć się korzystać ze THE
składni w Isabelle / HOL (2020). W poradniku main.pdf znajduje się:
The basic logic: x = y, True, False, ¬ P, P ∧ Q, P ∨ Q, P −→ Q, ∀ x. P,
∃ x. P, ∃!x. P, THE x. P.
Rozumiem, co inni mają na myśli, ale nie ostatni „THE x. P”. Moim najlepszym przypuszczeniem jest „(być może unikalne) x spełniające właściwość P”. Więc spróbowałem sformułować lemat z zabawką w następujący sposób:
lemma "0 = THE x::nat. (x ≥ 0 ∧ x ≤ 0)"
, co oznacza, że x, który jest jednocześnie ge i le 0, wynosi 0.
Ale pojawia się błąd w Isabelle / jEdit z podświetleniem słowa „THE”.
Próbowałem wyszukiwać za pomocą słów kluczowych Isabelle i „THE”, ale oczywiście słowo „THE” jest ignorowane przez wyszukiwarki. Stąd pytanie.
Czy ktoś może pomóc wyjaśnić znaczenie i użycie składni „THE”, miejmy nadzieję, na przykładzie tutaj?
Odpowiedzi
Potrzebujesz więcej nawiasów.
lemma "0 = (THE x::nat. (x ≥ 0 ∧ x ≤ 0))"
(*the proof*)
using theI[of ‹λx::nat. (x ≥ 0 ∧ x ≤ 0)› 0]
by auto
SOME (odpowiednio THE) jest (wariantem) operatora epsilon Hilberta, który zwraca element (czyli), który szanuje pewną właściwość. Jeśli żaden (żaden lub więcej niż jeden) nie istnieje, zwracany jest niedookreślony element.
NIEKTÓRE i NIE są wykonywalne. Rzadko są przydatne dla początkujących.