Tema 7: El lenguaje de demostración Isar
De Demostración asistida por ordenador (2011-12)
Revisión del 20:33 2 feb 2012 de Jalonso (discusión | contribuciones)
header {* Tema 7: El lenguaje de demostración Isar *}
theory Tema_7
imports Main
begin
text {*
Este tema describe los elementos básicos del lenguaje de demostración
Isar (Intelligible semi-automated reasoning).
*}
section {* Panorama de la sintaxis (simplificada) de Isar *}
text {*
Representación de lemas (y teoremas)
· Un lema (o teorema) comienza con una etiqueta seguida por algunas
premisas y una conclusión.
· Las premisas se introducen con la palabra "assumes" y se separan
con "and".
· Cada premisa puede etiquetarse para referenciarse en la demostración.
· La conclusión se introduce con la palabra "shows".
Gramática (simplificada) de las demostraciones en Isar
<demostración> ::= proof <método> <declaración>* qed
| by <método>
<declaración> ::= fix <variable>+
| assume <proposición>+
| (from <hecho>+)? have <proposición>+ <demostración>
| (from <hecho>+)? show <proposición>+ <demostración>
<proposición> ::= (<etiqueta>:)? <cadena>
hecho ::= <etiqueta>
método ::= -
| this
| rule <hecho>
| simp
| blast
| auto
| induct <variable>
La declaración "show" demuestra la conclusión de la demostración
mientras que la declaración "have" demuestra un resultado intermedio.
*}
section {* Razonamiento proposicional *}
text {*
Regla de introducción de la conjunción:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
Nota: Se puede consultar mediante
thm conjI
Lema. [Ejemplo de introducción de conjunción con razonamiento progresivo]
P, Q ⊢ P ∧ (Q ∧ P)
Demostración. Estamos suponiendo
P (1)
y
Q (2)
De (2) y (1), por introducción de la conjunción, se tiene
Q ∧ P (3)
De (1) y (3), por introducción de la conjunción, se tiene
P ∧ (Q ∧ P)
*}
lemma conj2:
assumes 1: P and 2: "Q"
shows "P ∧ (Q ∧ P)"
proof -
from 2 1 have 3: "Q ∧ P" by (rule conjI)
from 1 3 show "P ∧ (Q ∧ P)" by (rule conjI)
qed
text {*
Razonamiento progresivo y regresivo en Isabelle:
· Isabelle soporta razonamiento progresivo. La anterior demostración
es una muestra.
· Isabelle soporta razonamiento regresivo. La siguiente demostración
es una muestra.
Lema. [Ejemplo de introducción de la conjunción con razonamiento regresivo]
P, Q ⊢ P ∧ (Q ∧ P)
Demostración. Estamos suponiendo
P (1)
y
Q (2)
Para demostrar el lema, por introducción de la conjunción, basta probar
P
y
Q ∧ P (3)
La condición 'P' se tiene por la hipótesis (1). Para demostrar
la condición (3), por introducción de la conjunción, basta probar
Q
y
P
La condición 'Q' se tiene por la hipótesis (2) y la condición 'P' se
tiene por la hipótesis (1).
*}
lemma
assumes 1: "P" and 2: "Q"
shows "P ∧ (Q ∧ P)"
proof (rule conjI)
from 1 show "P" by this
next
show "Q ∧ P"
proof (rule conjI)
from 2 show "Q" by this
next
from 1 show "P" by this
qed
qed
text {*
El método "this" demuestra el objetivo usando el hecho actual; es
decir, el de la cláusula "from".
Reglas de eliminación de la conjunción:
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
Regla de introducción de la implicación:
· impI: (P ⟹ Q) ⟹ P ⟶ Q
Lema. [Ejemplo de razonamiento híbrido]
Sean a y b dos números naturales. Si 0 < a y a < b, entonces a*a < b*b.
*}
lemma
fixes a b :: "nat"
shows "0 < a ∧ a < b ⟶ a * a < b * b"
proof (rule impI)
assume x: "0 < a ∧ a < b"
from x have za: "0 < a" by (rule conjunct1)
from x have ab: "a < b" by (rule conjunct2)
from za ab have aa: "a*a < a*b" by simp
from ab have bb: "a*b < b*b" by simp
from aa bb show "a*a < b*b" by arith
qed
text {*
Modus ponens:
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
Reglas de introducción de la disyunción:
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
Regla de eliminación de la disyunción:
. disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
Lema. [Razonamiento por casos]
A ∨ B, A ⟶ C, B ⟶ C ⊢ C
*}
lemma
assumes ab: "A ∨ B" and ac: "A ⟶ C" and bc: "B ⟶ C"
shows "C"
proof -
note ab
moreover {
assume a: "A"
from ac a have "C" by (rule mp) }
moreover {
assume b: "B"
from bc b have "C" by (rule mp) }
ultimately show "C" by (rule disjE)
qed
text {*
Resumen de reglas proposicionales:
· TrueI: True
· FalseE: False ⟹ P
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· conjE: ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· notE: ⟦¬P; P⟧ ⟹ R
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· impE: ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· iff: (P ⟶ Q) ⟶ (Q ⟶ P) ⟶ P = Q
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· iffE: ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R
· ccontr: (¬P ⟹ False) ⟹ P
· classical: (¬P ⟹ P) ⟹ P
· exlude_middle: ¬P ∨ P
· disjCI: (¬Q ⟹ P) ⟹ P ∨ Q
· impCE: ⟦P ⟶ Q; ¬P ⟹ R; Q ⟹ R⟧ ⟹ R
· iffCE: ⟦P = Q; ⟦P; Q⟧ ⟹ R; ⟦¬P; ¬Q⟧ ⟹ R⟧ ⟹ R
· notnotD: ¬¬P ⟹ P
· swap: ⟦¬P; ¬R ⟹ P⟧ ⟹ R
Referencia de reglas de inferencia: Más información sobre las reglas
de inferencia se encuentra en la sección 2.2 de "Isabelle's Logics:
HOL".
*}
section {* Atajos de Isar *}
text {*
Isar tiene muchos atajos, como los siguientes:
this | éste | el hecho probado en la declaración anterior
then | entonces | from this
hence | por lo tanto | then have
thus | de esta manera | then show
with hecho+ | con | from hecho+ and this
. | por ésto | by this
.. | trivialmente | by regla (Isabelle adivina la regla)
Razonamiento acumulativo:
Una sucesión de hechos que se van a usar como premisa en una declaración
puede agruparse usando "moreover" (además) y usarse en la declaración
usando "ultimately" (finalmente).
Lema. [Ejemplo de uso de atajos y razonamiento acumulativo]
A ∧ B ⊢ B ∧ A.
*}
lemma "A ∧ B ⟶ B ∧ A"
proof (rule impI)
assume ab: "A ∧ B"
hence "B" by (rule conjunct2)
moreover from ab have "A" ..
ultimately show "B ∧ A" by (rule conjI)
qed
section {* Cuantificadores universal y existencial *}
thm allE
text {*
Reglas del cuantificador universal:
· allI: (⋀x. P x) ⟹ ∀x. P x
· allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
En la regla allI la nueva variable se introduce mediante la palabra "fix".
Lema. [Ejemplo con cuantificadores universales]
∀x. P ⟶ Q x ⊢ P ⟶ (∀x. Q x)
*}
lemma
assumes a: "∀ x. P ⟶ Q x"
shows "P ⟶ (∀ x. Q x)"
proof (rule impI)
assume p: "P"
show "∀ x. Q x"
proof (rule allI)
fix y
from a have pq: "P ⟶ Q y" by (rule allE)
from pq p show "Q y" by (rule mp)
qed
qed
text {*
Reglas del cuantificador existencial:
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
En la regla exE la nueva variable se introduce mediante la declaración
"obtain ... where ... by (rule exE)"
Lema. [Ejemplo con cuantificador existencial y demostración progresiva]
∃x. P ∧ Q(x) ⊢ P ∧ (∃x. Q(x))
*}
lemma
assumes e: "∃ x. P ∧ Q(x)"
shows "P ∧ (∃ x. Q(x))"
proof -
from e obtain y where f: "P ∧ Q(y)" by (rule exE)
from f have p: "P" by (rule conjunct1)
from f have q: "Q(y)" by (rule conjunct2)
from q have eq: "∃ x. Q(x)" by (rule exI)
from p eq show "P ∧ (∃ x. Q(x))" by (rule conjI)
qed
text {*
Lema. [Ejemplo con cuantificador existencial y demostración automática]
∃x. P ∧ Q(x) ⊢ P ∧ (∃x. Q(x))
*}
lemma
assumes e: "∃ x. P ∧ Q(x)"
shows "P ∧ (∃ x. Q(x))"
proof -
from e obtain y where f: "P ∧ Q(y)" ..
from f have p: "P" ..
from f have q: "Q(y)" ..
from q have eq: "∃x. Q(x)" ..
from p eq show "P ∧ (∃x. Q(x))" ..
qed
text {*
Lema. [Ejemplo con cuantificador existencial y demostración regresiva]
∃x. P ∧ Q(x) ⊢ P ∧ (∃x. Q(x))"
*}
lemma
assumes e: "∃x. P ∧ Q(x)"
shows "P ∧ (∃x. Q(x))"
proof (rule conjI)
show "P"
proof -
from e obtain y where p: "P ∧ Q(y)" by (rule exE)
from p show "P" by (rule conjunct1)
qed
show "∃x. Q(x)"
proof -
from e obtain y where p: "P ∧ Q(y)" by (rule exE)
from p have q: "Q(y)" by (rule conjunct2)
from q show "∃x. Q(x)" by (rule exI)
qed
qed
text {*
Definición. [Ejemplo de definición existencial]
El número natural x divide al número natural y si existe un natural k
tal que k×x = y. Se representa por x | y.
*}
definition divide :: "nat ⇒ nat ⇒ bool" ("_ | _" [80,80] 80) where
"x | y ≡ ∃k. k*x = y"
text {*
Ejemplo de activación automática de regla de simplificación:
La definición de divide se añade a las reglas de simplificación.
*}
declare divide_def[simp]
text {*
Lema. [Transitividad de la divisibilidad]
Sean a, b y c números naturales. Si b es divisible por a y c es
divisible por b, entonces c es divisible por a.
*}
lemma divide_trans:
fixes a b c :: "nat"
assumes ab: "a | b" and bc: "b | c"
shows "a | c"
proof simp
from ab obtain m where m: "m*a = b" by auto
from bc obtain n where n: "n*b = c" by auto
from m n have "m*n*a = c" by auto
thus "∃k. k*a = c" by (rule exI)
qed
text {*
Método auto: En el lema anterior es la primera vez que se usa el
método automático "auto".
Lema. [CNS de divisibilidad]
Sean a y b dos números naturales. Entonces a es divisible por b syss
el resto de dividir a entre b es cero.
*}
lemma CNS_divisibilidad:
"(a | b) = (b mod a = 0)"
by auto
section {* Razonamiento ecuacional *}
text {*
Elementos para el razonamiento ecuacional:
El razonamiento ecuacional se realiza de manera más concisa usando la
combinación de "also" (además) y "finally" (finalmente).
Lema. [Ejemplo de razonamiento ecuacional]
Si a=b, b=c y c=d, entonces a=d.
*}
lemma
assumes 1: "a = b" and 2: "b = c" and 3: "c = d"
shows "a = d"
proof -
have "a = b" by (rule 1)
also have "… = c" by (rule 2)
also have "… = d" by (rule 3)
finally show "a = d" .
qed
text {*
El lema anterior puede demostrarse automáticamente con la maza
("sledgehammer").
*}
lemma
assumes 1: "a = b" and 2: "b = c" and 3: "c = d"
shows "a = d"
proof -
show "a=d" by (metis 1 2 3)
qed
end