¿Cómo utilizar la sintaxis “THE” en Isabelle / HOL?

Jan 12 2021

Estoy tratando de aprender a usar la THEsintaxis 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

3 MathiasFleury Jan 12 2021 at 13:09

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.