Jak używać składni „THE” w Isabelle / HOL?

Jan 12 2021

Próbuję nauczyć się korzystać ze THEskł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

3 MathiasFleury Jan 12 2021 at 13:09

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.