Como usar a sintaxe “THE” no Isabelle / HOL?

Jan 12 2021

Estou tentando aprender a usar a THEsintaxe em Isabelle / HOL (2020). No tutorial main.pdf, existe:

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

Eu posso entender o que os outros querem dizer, mas não o último "THE x. P". Meu melhor palpite é "o (talvez único) x que satisfaça a propriedade P". Então, tentei apresentar um lema do brinquedo da seguinte maneira:

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

, o que significa que x que é ge e le 0 é 0.

Mas recebo um erro no Isabelle / jEdit com destaque na palavra "THE".

Tentei pesquisar com as palavras-chave Isabelle e "THE", mas obviamente a palavra "THE" é ignorada pelos motores de pesquisa. Daí a questão aqui.

Alguém pode ajudar a explicar o significado e o uso da sintaxe "THE", espero que com o exemplo aqui?

Respostas

3 MathiasFleury Jan 12 2021 at 13:09

Você precisa de mais parênteses.

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

SOME (resp. THE) é (uma variante do) operador épsilon de Hilbert que retorna um (o) elemento que respeita uma determinada propriedade. Se nenhum (nenhum ou mais de um) existir, um elemento não especificado será retornado.

SOME e THE não são executáveis. Eles raramente são úteis para iniciantes.