Como usar a sintaxe “THE” no Isabelle / HOL?
Estou tentando aprender a usar a THE
sintaxe 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
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.