En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.
La clase se ha basado en la siguiente teoría Isabelle
chapter {* Tema 11: Definiciones inductivas *}
theory T11_Definiciones_inductivas
imports Main
begin
section {* El conjunto de los números pares *}
text {*
· El conjunto de los números pares se define inductivamente como el
menor conjunto que contiene al 0 y es cerrado por la operación (+2).
· El conjunto de los números pares también puede definirse como los
naturales divisible por 2.
· Veremos cómo se escriben las dos definiciones en Isabelle/HOL y cómo
se demuestra su equivalencia.
*}
subsection {* Definición inductiva del conjunto de los pares *}
inductive_set par :: "nat set" where
cero [intro!]: "0 ∈ par"
| paso [intro!]: "n ∈ par ⟹ (Suc (Suc n)) ∈ par"
text {*
· Una definición inductiva está formada con reglas de introducción.
· La definición inductiva genera varios teoremas:
· par.cero: 0 ∈ par
· par.paso: n ∈ par ⟹ Suc (Suc n) ∈ par
· par.simps: (a ∈ par) = (a = 0 ∨ (∃n. a = Suc (Suc n) ∧ n ∈ par))
*}
subsection {* Uso de las reglas de introducción *}
text {*
Lema: Los números de la forma 2*k son pares.
*}
― ‹La demostración automática es›
lemma dobles_son_pares [intro!]:
"2*k ∈ par"
by (induct k) auto
― ‹La demostración estructurada es›
lemma dobles_son_pares_2:
"2*k ∈ par"
proof (induct k)
show "2 * 0 ∈ par" by auto
next
show "⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par" by auto
qed
text {*
· Nota: Nuestro objetivo es demostrar la equivalencia de la definición
anterior y la definición mediante divisibilidad (even).
· Lema: Si n es divisible por 2, entonces es par.
*}
lemma even_imp_par: "even n ⟹ n ∈ par"
by auto
subsection {* Regla de inducción *}
text {*
Entre las reglas generadas por la definión de par está la de
inducción:
· par.induct: ⟦ x ∈ par;
P 0;
⋀n. ⟦n ∈ par; P n⟧ ⟹ P (Suc (Suc n))⟧
⟹ P x
*}
text {*
Lema: Los números pares son divisibles por 2.
*}
― ‹1ª demostración (detallada)›
lemma par_imp_even:
"n ∈ par ⟹ even n"
proof (induction rule: par.induct)
show "2 dvd (0::nat)" by (simp_all add: dvd_def)
next
fix n::nat
assume H1: "n ∈ par" and
H2: "even n"
have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
then obtain k where "n = 2*k" ..
then have "Suc (Suc n) = 2*(k+1)" by auto
then have "∃k. Suc (Suc n) = 2*k" ..
then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
― ‹2ª demostración (con arith)›
lemma par_imp_even_2:
"n ∈ par ⟹ even n"
proof (induction rule: par.induct)
show "even (0::nat)" by (simp_all add: dvd_def)
next
fix n::nat
assume H1: "n ∈ par" and
H2: "even n"
then show "even (Suc (Suc n))" by (auto simp add: dvd_def, arith)
qed
― ‹3ª demostración (automática)›
lemma par_imp_even_3:
"n ∈ par ⟹ even n"
by (induction rule:par.induct) (auto simp add: dvd_def, arith)
text {*
Lema: Un número n es par syss es divisible por 2.
*}
theorem par_iff_even: "(n ∈ par) = (even n)"
by (blast intro: even_imp_par par_imp_even)
subsection{* Generalización y regla de inducción *}
text {*
· Antes de aplicar inducción se debe de generalizar la fórmula a
probar.
· Vamos a ilustrar el principio anterior en el caso de los conjuntos
inductivamente definidos, con el siguiente ejemplo: si n+2 es par,
entonces n también lo es.
· El siguiente intento falla:
*}
lemma "Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (erule par.induct)
oops
text {*
En el intento anterior, los subobjetivos generados son
1. n ∈ par
2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par
que no se pueden demostrar.
Se ha perdido la información sobre Suc (Suc n).
*}
text {*
Reformulación del lema: Si n es par, entonces n-2 también lo es.
*}
― ‹La demostración automática es›
lemma par_imp_par_menos_2:
"n ∈ par ⟹ n - 2 ∈ par"
by (induction rule:par.induct) auto
― ‹La demostración estructurada es›
lemma "n ∈ par ⟹ n - 2 ∈ par"
proof (induction rule:par.induct)
show "0 - 2 ∈ par" by auto
next
show "⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par" by auto
qed
text {*
Con el lema anterior se puede demostrar el original.
*}
― ‹La demostración estructurada es›
lemma
assumes "Suc (Suc n) ∈ par"
shows "n ∈ par"
proof -
have "Suc (Suc n) - 2 ∈ par" using assms by (rule par_imp_par_menos_2)
then show "n ∈ par" by simp
qed
― ‹La demostración aplicativa es›
lemma
"Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (drule par_imp_par_menos_2)
apply simp
done
(* Comentar el uso de drule *)
― ‹La demostración automática es›
lemma Suc_Suc_par_imp_par:
"Suc (Suc n) ∈ par ⟹ n ∈ par"
by (drule par_imp_par_menos_2, simp)
text {*
Lemma. Un número natural n es par syss n+2 es par.
*}
lemma [iff]: "((Suc (Suc n)) ∈ par) = (n ∈ par)"
by (blast dest: Suc_Suc_par_imp_par)
text {*
Se usa el atributo "iff" porque sirve como regla de simplificación.
*}
subsection {* Definiciones mutuamente inductivas *}
text {*
Definición cruzada de los conjuntos inductivos de los pares y de los
impares:
*}
inductive_set
Pares :: "nat set" and
Impares :: "nat set"
where
ceroP: "0 ∈ Pares"
| ParesI: "n ∈ Impares ⟹ Suc n ∈ Pares"
| ImparesI: "n ∈ Pares ⟹ Suc n ∈ Impares"
text {*
El esquema de inducción generado por la definición anterior es
· Pares_Impares.induct:
⟦P1 0;
⋀n. ⟦n ∈ Impares; P2 n⟧ ⟹ P1 (Suc n);
⋀n. ⟦n ∈ Pares; P1 n⟧ ⟹ P2 (Suc n)⟧
⟹ (x1 ∈ Pares ⟶ P1 x1) ∧ (x2 ∈ Impares ⟶ P2 x2)
*}
text {*
Ejemplo de demostración usando el esquema anterior.
*}
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
proof (induction rule:Pares_Impares.induct)
show "even (0::nat)" by simp
next
fix n :: "nat"
assume H1: "n ∈ Impares" and
H2: "even (Suc n)"
show "even (Suc n)" using H2 by simp
next
fix n :: "nat"
assume H1: "n ∈ Pares" and
H2: "even n"
have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
then obtain k where "n = 2*k" ..
then have "Suc (Suc n) = 2*(k+1)" by auto
then have "∃k. Suc (Suc n) = 2*k" ..
then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
subsection {* Definición inductiva de predicados *}
text {*
Definición inductiva del predicado es_par tal que (es_par n) se
verifica si n es par.
*}
inductive es_par :: "nat ⇒ bool" where
"es_par 0"
| "es_par n ⟹ es_par (Suc(Suc n))"
text {*
Heurística para elegir entre definir conjuntos o predicados:
· si se va a combinar con operaciones conjuntistas, definir conjunto;
· en caso contrario, definir predicado.
*}
end |
chapter {* Tema 11: Definiciones inductivas *}
theory T11_Definiciones_inductivas
imports Main
begin
section {* El conjunto de los números pares *}
text {*
· El conjunto de los números pares se define inductivamente como el
menor conjunto que contiene al 0 y es cerrado por la operación (+2).
· El conjunto de los números pares también puede definirse como los
naturales divisible por 2.
· Veremos cómo se escriben las dos definiciones en Isabelle/HOL y cómo
se demuestra su equivalencia.
*}
subsection {* Definición inductiva del conjunto de los pares *}
inductive_set par :: "nat set" where
cero [intro!]: "0 ∈ par"
| paso [intro!]: "n ∈ par ⟹ (Suc (Suc n)) ∈ par"
text {*
· Una definición inductiva está formada con reglas de introducción.
· La definición inductiva genera varios teoremas:
· par.cero: 0 ∈ par
· par.paso: n ∈ par ⟹ Suc (Suc n) ∈ par
· par.simps: (a ∈ par) = (a = 0 ∨ (∃n. a = Suc (Suc n) ∧ n ∈ par))
*}
subsection {* Uso de las reglas de introducción *}
text {*
Lema: Los números de la forma 2*k son pares.
*}
― ‹La demostración automática es›
lemma dobles_son_pares [intro!]:
"2*k ∈ par"
by (induct k) auto
― ‹La demostración estructurada es›
lemma dobles_son_pares_2:
"2*k ∈ par"
proof (induct k)
show "2 * 0 ∈ par" by auto
next
show "⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par" by auto
qed
text {*
· Nota: Nuestro objetivo es demostrar la equivalencia de la definición
anterior y la definición mediante divisibilidad (even).
· Lema: Si n es divisible por 2, entonces es par.
*}
lemma even_imp_par: "even n ⟹ n ∈ par"
by auto
subsection {* Regla de inducción *}
text {*
Entre las reglas generadas por la definión de par está la de
inducción:
· par.induct: ⟦ x ∈ par;
P 0;
⋀n. ⟦n ∈ par; P n⟧ ⟹ P (Suc (Suc n))⟧
⟹ P x
*}
text {*
Lema: Los números pares son divisibles por 2.
*}
― ‹1ª demostración (detallada)›
lemma par_imp_even:
"n ∈ par ⟹ even n"
proof (induction rule: par.induct)
show "2 dvd (0::nat)" by (simp_all add: dvd_def)
next
fix n::nat
assume H1: "n ∈ par" and
H2: "even n"
have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
then obtain k where "n = 2*k" ..
then have "Suc (Suc n) = 2*(k+1)" by auto
then have "∃k. Suc (Suc n) = 2*k" ..
then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
― ‹2ª demostración (con arith)›
lemma par_imp_even_2:
"n ∈ par ⟹ even n"
proof (induction rule: par.induct)
show "even (0::nat)" by (simp_all add: dvd_def)
next
fix n::nat
assume H1: "n ∈ par" and
H2: "even n"
then show "even (Suc (Suc n))" by (auto simp add: dvd_def, arith)
qed
― ‹3ª demostración (automática)›
lemma par_imp_even_3:
"n ∈ par ⟹ even n"
by (induction rule:par.induct) (auto simp add: dvd_def, arith)
text {*
Lema: Un número n es par syss es divisible por 2.
*}
theorem par_iff_even: "(n ∈ par) = (even n)"
by (blast intro: even_imp_par par_imp_even)
subsection{* Generalización y regla de inducción *}
text {*
· Antes de aplicar inducción se debe de generalizar la fórmula a
probar.
· Vamos a ilustrar el principio anterior en el caso de los conjuntos
inductivamente definidos, con el siguiente ejemplo: si n+2 es par,
entonces n también lo es.
· El siguiente intento falla:
*}
lemma "Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (erule par.induct)
oops
text {*
En el intento anterior, los subobjetivos generados son
1. n ∈ par
2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par
que no se pueden demostrar.
Se ha perdido la información sobre Suc (Suc n).
*}
text {*
Reformulación del lema: Si n es par, entonces n-2 también lo es.
*}
― ‹La demostración automática es›
lemma par_imp_par_menos_2:
"n ∈ par ⟹ n - 2 ∈ par"
by (induction rule:par.induct) auto
― ‹La demostración estructurada es›
lemma "n ∈ par ⟹ n - 2 ∈ par"
proof (induction rule:par.induct)
show "0 - 2 ∈ par" by auto
next
show "⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par" by auto
qed
text {*
Con el lema anterior se puede demostrar el original.
*}
― ‹La demostración estructurada es›
lemma
assumes "Suc (Suc n) ∈ par"
shows "n ∈ par"
proof -
have "Suc (Suc n) - 2 ∈ par" using assms by (rule par_imp_par_menos_2)
then show "n ∈ par" by simp
qed
― ‹La demostración aplicativa es›
lemma
"Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (drule par_imp_par_menos_2)
apply simp
done
(* Comentar el uso de drule *)
― ‹La demostración automática es›
lemma Suc_Suc_par_imp_par:
"Suc (Suc n) ∈ par ⟹ n ∈ par"
by (drule par_imp_par_menos_2, simp)
text {*
Lemma. Un número natural n es par syss n+2 es par.
*}
lemma [iff]: "((Suc (Suc n)) ∈ par) = (n ∈ par)"
by (blast dest: Suc_Suc_par_imp_par)
text {*
Se usa el atributo "iff" porque sirve como regla de simplificación.
*}
subsection {* Definiciones mutuamente inductivas *}
text {*
Definición cruzada de los conjuntos inductivos de los pares y de los
impares:
*}
inductive_set
Pares :: "nat set" and
Impares :: "nat set"
where
ceroP: "0 ∈ Pares"
| ParesI: "n ∈ Impares ⟹ Suc n ∈ Pares"
| ImparesI: "n ∈ Pares ⟹ Suc n ∈ Impares"
text {*
El esquema de inducción generado por la definición anterior es
· Pares_Impares.induct:
⟦P1 0;
⋀n. ⟦n ∈ Impares; P2 n⟧ ⟹ P1 (Suc n);
⋀n. ⟦n ∈ Pares; P1 n⟧ ⟹ P2 (Suc n)⟧
⟹ (x1 ∈ Pares ⟶ P1 x1) ∧ (x2 ∈ Impares ⟶ P2 x2)
*}
text {*
Ejemplo de demostración usando el esquema anterior.
*}
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
proof (induction rule:Pares_Impares.induct)
show "even (0::nat)" by simp
next
fix n :: "nat"
assume H1: "n ∈ Impares" and
H2: "even (Suc n)"
show "even (Suc n)" using H2 by simp
next
fix n :: "nat"
assume H1: "n ∈ Pares" and
H2: "even n"
have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
then obtain k where "n = 2*k" ..
then have "Suc (Suc n) = 2*(k+1)" by auto
then have "∃k. Suc (Suc n) = 2*k" ..
then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
subsection {* Definición inductiva de predicados *}
text {*
Definición inductiva del predicado es_par tal que (es_par n) se
verifica si n es par.
*}
inductive es_par :: "nat ⇒ bool" where
"es_par 0"
| "es_par n ⟹ es_par (Suc(Suc n))"
text {*
Heurística para elegir entre definir conjuntos o predicados:
· si se va a combinar con operaciones conjuntistas, definir conjunto;
· en caso contrario, definir predicado.
*}
end
Como ejercicio se propuso la relación 8 sobre gramáticas libres de contexto.