¿Cómo utilizar la sintaxis “THE” en Isabelle / HOL?
Estoy tratando de aprender a usar la THE
sintaxis en Isabelle / HOL (2020). En el tutorial main.pdf, hay:
The basic logic: x = y, True, False, ¬ P, P ∧ Q, P ∨ Q, P −→ Q, ∀ x. P,
∃ x. P, ∃!x. P, THE x. P.
Puedo entender lo que significan los demás, pero no el último "EL x. P". Mi mejor suposición es "la (quizás única) x que satisfaga la propiedad P". Así que traté de enunciar un lema de juguete de la siguiente manera:
lemma "0 = THE x::nat. (x ≥ 0 ∧ x ≤ 0)"
, lo que significa que la x que es tanto ge como le 0 es 0.
Pero obtengo un error en Isabelle / jEdit con un resaltado en la palabra "THE".
Traté de buscar con las palabras clave Isabelle y "THE", pero obviamente los motores de búsqueda ignoran la palabra "THE". De ahí la pregunta aquí.
¿Puede alguien ayudarme a explicar el significado y el uso de la sintaxis "THE", con suerte con el ejemplo aquí?
Respuestas
Necesitas más paréntesis.
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) es (una variante del) operador épsilon de Hilbert que devuelve un (the) elemento que respeta una determinada propiedad. Si no existe ninguno (ninguno o más de uno), se devuelve un elemento subespecificado.
SOME y THE no son ejecutables. Rara vez son útiles para principiantes.