Как использовать синтаксис «THE» в Isabelle / HOL?

Question

Я пытаюсь научиться использовать THEсинтаксис в Isabelle / HOL (2020). В учебнике main.pdf есть:

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

Я могу понять, что означают другие, но не последний "THE x. P". Мое лучшее предположение - это «(возможно, уникальный) x, удовлетворяющий свойству P». Поэтому я попытался сформулировать игрушечную лемму следующим образом:

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

, что означает, что x, который является как ge, так и le 0, равен 0.

Но я получаю сообщение об ошибке в Isabelle / jEdit с выделением слова "THE".

Я попытался выполнить поиск по ключевым словам Изабель и "THE", но, очевидно, слово "THE" игнорируется поисковыми системами. Отсюда вопрос.

Может ли кто-нибудь помочь объяснить значение и использование синтаксиса "THE", надеюсь, с помощью приведенного здесь примера?

Answer 1

Вам нужно больше скобок.

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

НЕКОТОРЫЕ (соответственно THE) - это (вариант) эпсилон-оператора Гильберта, который возвращает () элемент, который учитывает определенное свойство. Если ни одного (ни одного или более одного) не существует, возвращается недоопределенный элемент.

НЕКОТОРЫЕ и НЕ исполняемые. Они редко бывают полезны новичкам.