header {* Tema 10: Conjuntos definidos inductivamente *}
theory T10_Conjuntos_definidos_inductivamente
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.
· Lema: Si n es divisible por 2, entonces es par.
*}
lemma dvd_imp_par: "2 dvd n ⟹ n ∈ par"
by (auto simp add: dvd_def)
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_dvd:
"n ∈ par ⟹ 2 dvd 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: "2 dvd n"
have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
then obtain k where "n = 2*k" ..
hence "Suc (Suc n) = 2*(k+1)" by auto
hence "∃k. Suc (Suc n) = 2*k" ..
thus "2 dvd Suc (Suc n)" by (simp add: dvd_def)
qed
-- "2ª demostración (con arith)"
lemma par_imp_dvd_2:
"n ∈ par ⟹ 2 dvd 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: "2 dvd n"
thus "2 dvd Suc (Suc n)" by (auto simp add: dvd_def, arith)
qed
-- "3ª demostración (automática)"
lemma par_imp_dvd_3:
"n ∈ par ⟹ 2 dvd 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_dvd: "(n ∈ par) = (2 dvd n)"
by (blast intro: dvd_imp_par par_imp_dvd)
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)
thus "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 ⟶ 2 dvd m) ∧ (n ∈ Impares ⟶ 2 dvd (Suc n))"
proof (induction rule:Pares_Impares.induct)
show "2 dvd (0::nat)" by simp
next
fix n :: "nat"
assume H1: "n ∈ Impares" and
H2: "2 dvd Suc n"
show "2 dvd Suc n" using H2 by simp
next
fix n :: "nat"
assume H1: "n ∈ Pares" and
H2: "2 dvd n"
have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
then obtain k where "n = 2*k" ..
hence "Suc (Suc n) = 2*(k+1)" by auto
hence "∃k. Suc (Suc n) = 2*k" ..
thus "2 dvd 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.
*}
section {* La clausura reflexiva transitiva *}
text {*
· Las definiciones inductivas aceptan parámetros; por tanto, permite
expresar funciones que construyen conjuntos.
· La relaciones binarias son conjuntos de pares; por tanto, se pueden
definir inductivamente.
*}
text {*
· La clausura reflexiva y transitiva de una relación r es la menor
relación reflexiva y transitiva que contiene a r.
· Se representa por r*.
· Se puede definir inductivamente:
· (x,x) ∈ r*
· Si (x,y) ∈ r e (y,z) ∈ r*, entonces (x,z) ∈ r*
· La definición inductiva se puede expresar en Isabelle/HOL como
sigue:
*}
inductive_set
crt :: "('a × 'a) set ⇒ ('a × 'a) set" ("_*" [1000] 999)
for r :: "('a × 'a) set"
where
crt_refl [iff]: "(x,x) ∈ r*"
| crt_paso: "⟦ (x,y) ∈ r; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"
text {*
Notas:
· La sintaxis concreta permite escribir r* en lugar de (crt r).
· La definición consta de dos reglas.
· A la regla reflexiva se le añade el atributo iff para aumentar la
automatización.
· A la regla del paso no se le añade ningún atributo, porque r* ocurre
en la izquierda.
· En el resto de esta sección se demuestra que esta definición
coincide con la menor relación reflexiva y transitiva que contiene a
r.
*}
text {*
Lema. La relación r* contiene a r.
*}
lemma [intro]: "(x,y) ∈ r ⟹ (x,y) ∈ r*"
by (blast intro: crt_paso)
text {*
Notas:
· La ventaja del lema es que se puede declarar como regla de
introducción, porque r* ocurre sólo en la derecha.
· Con la declaración, algunas demostraciones que usan crt_paso se
hacen de manera automática.
*}
text {*
El esquema de inducción de la clausura reflexiva transitiva es
· crt.induct:
⟦(x1, x2) ∈ r*;
⋀x. P x x;
⋀x y z. ⟦(x,y) ∈ r; (y,z) ∈ r*; P y z⟧ ⟹ P x z⟧
⟹ P x1 x2
*}
text {*
Lema. La relación r* es transitiva.
*}
lemma crt_trans: "⟦ (x,y) ∈ r*; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"
proof (induction rule:crt.induct)
oops
text {*
· El caso base que genera es
⋀x. (y, z) ∈ r* ⟹ (x, z) ∈ r*
que no se puede demostrar.
· El problema está que que en la conclusión no aparece la y. Se puede
reformular como sigue:
*}
lemma crt_trans [rule_format]:
"(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
proof (induction rule:crt.induct)
show "⋀x. (x,z) ∈ r* ⟶ (x,z) ∈ r*" by simp
next
fix x y u
assume H1: "(x,y) ∈ r" and
H2: "(y,u) ∈ r*" and
H3: "(u,z) ∈ r* ⟶ (y,z) ∈ r*"
show "(u,z) ∈ r* ⟶ (x,z) ∈ r*"
proof
assume "(u,z) ∈ r*"
with H3 have "(y,z) ∈ r*" ..
with H1 show "(x,z) ∈ r*" by (rule crt_paso)
qed
qed
text {*
Notas:
· La reformulación anterior es un caso particular de la siguiente
heurística:
"Para probar una fórmula por inducción sobre (x1,...,xn) ∈ R,
poner todas las premisas conteniendo cualquiera de lax xi en la
conclusión usando ⟶".
· El atributo "rule_format" transforma ⟶ en ⟹.
*}
text {*
(crt2 r) es la menor relación reflexiva y transitiva que contiene a r.
*}
inductive_set
crt2 :: "('a × 'a)set ⇒ ('a × 'a)set"
for r :: "('a × 'a)set"
where
"(x,y) ∈ r ⟹ (x,y) ∈ crt2 r"
| "(x,x) ∈ crt2 r"
| "⟦ (x,y) ∈ crt2 r; (y,z) ∈ crt2 r ⟧ ⟹ (x,z) ∈ crt2 r"
text {*
Lema. La relación (crt2 r) está contenida en r*.
*}
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
proof (induction rule: crt2.induct)
fix x y
assume "(x,y) ∈ r"
thus "(x,y) ∈ r*" by blast
next
fix x
show "(x,x) ∈ r*" by blast
next
fix x y z
assume H1: "(x,y) ∈ crt2 r" and
H2: "(x,y) ∈ r*" and
H3: "(y,z) ∈ crt2 r" and
H4: "(y,z) ∈ r*"
show "(x,z) ∈ r*" using H2 H4 by (blast intro: crt_trans)
qed
text {*
Lema. La relación r* está contenida en (crt2 r).
*}
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
proof (induction rule:crt.induct)
fix x
show "(x,x) ∈ crt2 r" by (rule crt2.intros(2))
next
fix x y z
assume H1: "(x,y) ∈ r" and
H2: "(y,z) ∈ r*" and
H3: "(y,z) ∈ crt2 r"
have "(x,y) ∈ crt2 r" using H1 by (rule crt2.intros(1))
thus "(x,z) ∈ crt2 r" using H3 by (rule crt2.intros(3))
qed
text {*
Ejercicio: Demostrar que si (x,y) ∈ r* e (y,z) ∈ r, entonces
(x,z) ∈ r*
*}
lemma crt_paso2 [rule_format]:
"(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) : r*"
proof (induction rule: crt.induct)
fix x
show "(x,z) ∈ r ⟶ (x,z) ∈ r*"
proof
assume "(x,z) ∈ r"
thus "(x,z) ∈ r*" by blast
qed
next
fix x y u
assume H1: "(x,y) ∈ r" and
H2: "(y,u) ∈ r*" and
H3: "(u,z) ∈ r ⟶ (y,z) ∈ r*"
show "(u,z) ∈ r ⟶ (x,z) ∈ r*"
proof
assume "(u,z) ∈ r"
with H3 have "(y,z) ∈ r*" ..
with H1 show "(x,z) ∈ r*" by (rule crt_paso)
qed
qed
section {* Definiciones inductivas avanzadas *}
subsection {* Cuantificadores universales en las reglas de introducción
(términos básicos) *}
text {*
Como caso de estudio se presenta la teoría de los términos básicos
(i.e. sin variables).
*}
text {*
· Un término básico se obtiene aplicando una función a una lista de
términos básicos.
· Las constantes se representan mediante funciones 0-arias.
· terminoB es el tipo de los términos básicos.
*}
datatype 'f terminoB = Aplica 'f "'f terminoB list"
text {*
op_entera es el tipo de las operaciones enteras y está formado por las
constantes enteras, el opuesto y la suma.
*}
datatype op_entera = Numero int | Opuesto | Suma
text {*
El tipo "op_entera terminoB" está formado por los términos básicos con
operaciones enteras.
*}
text {*
El conjunto de los téminos básicos sobre un conjunto de símbolos de
función F se define inductivamente:
si f ∈ F y t1,...,tn son términos básicos sobre F, entonces
f(t1,...,tn) es un término básico sobre F.
*}
inductive_set terminosB :: "'f set ⇒ 'f terminoB set"
for F :: "'f set"
where
paso [intro!]: "⟦∀t ∈ set args. t ∈ terminosB F; f ∈ F⟧
⟹ (Aplica f args) ∈ terminosB F"
text {*
Ejemplo de demostración sobre el conjunto de los términos básicos:
Lema: terminosB es monótona; es decir, si F ⊆ G, entonces
terminosB F ⊆ terminosB G.
*}
lemma terminosB_mono:
assumes "F ⊆ G"
shows "terminosB F ⊆ terminosB G"
proof -
have "⋀x. x ∈ terminosB F ⟹ x ∈ terminosB G"
proof (rule terminosB.induct)
fix x ys f
assume H1: "∀t ∈ set ys. t ∈ terminosB F ∧ t ∈ terminosB G" and
H2: "f ∈ F"
have "∀t ∈ set ys. t ∈ terminosB G" using H1 by simp
thus "(Aplica f ys) ∈ terminosB G" using assms H2 by blast
qed
thus ?thesis ..
qed
text {*
· La aridad de un símbolo de función es el número de argumentos a los
que se puede aplicar.
· Un término está bien formado si la longitud de la lista de
argumentos de cada símbolo de función es igual a su aridad.
*}
inductive_set
terminoB_bien_formado :: "('f ⇒ nat) ⇒ 'f terminoB set"
for aridad :: "'f ⇒ nat"
where
paso [intro!]: "⟦∀t ∈ set args. t ∈ terminoB_bien_formado aridad;
length args = aridad f⟧
⟹ (Aplica f args) ∈ terminoB_bien_formado aridad"
subsection {* Definición alternativa mediante una función monótona *}
text {*
En la siguiente definición se usa
· "lists A" que es el conjunto de las listas cuyos elementos
pertenecen conjunto A. Está definido en la teoría Lists por
inductive_set
lists :: "'a set => 'a list set"
for A :: "'a set"
where
"[] ∈ lists A"
| "⟦ a ∈ A; l ∈ lists A ⟧ ⟹ a # l ∈ lists A"
· Para demostrar la terminación, se usa el lema
lists_mono: A ⊆ B ⟹ lists A ⊆ lists B
*}
inductive_set
terminoB_bien_formado' :: "('f ⇒ nat) ⇒ 'f terminoB set"
for aridad :: "'f ⇒ nat"
where
paso [intro!]: "⟦args ∈ lists (terminoB_bien_formado' aridad);
length args = aridad f⟧
⟹ (Aplica f args) ∈ terminoB_bien_formado' aridad"
monos lists_mono
text {*
El uso de lists_mono no es necesario. Se incluye para mostrar la
sintaxis de la declaración de "monos".
*}
subsection {* Demostración de equivalencia *}
lemma
"terminoB_bien_formado aridad ⊆ terminoB_bien_formado' aridad"
proof -
have "⋀x. x ∈ terminoB_bien_formado aridad ⟹
x ∈ terminoB_bien_formado' aridad"
proof (erule terminoB_bien_formado.induct)
fix x ys f
assume H1: "∀t ∈ set ys. t ∈ terminoB_bien_formado aridad ∧
t ∈ terminoB_bien_formado' aridad" and
H2: "length ys = aridad f"
thus "Aplica f ys ∈ terminoB_bien_formado' aridad" by auto
qed
thus ?thesis ..
qed
lemma
"terminoB_bien_formado' aridad ⊆ terminoB_bien_formado aridad"
proof -
have "⋀x. x ∈ terminoB_bien_formado' aridad ⟹
x ∈ terminoB_bien_formado aridad"
proof (erule terminoB_bien_formado'.induct)
fix x ys f
assume H1: "ys ∈ lists (terminoB_bien_formado' aridad ∩
{a. a ∈ terminoB_bien_formado aridad})" and
H2: "length ys = aridad f"
have "ys ∈ lists (terminoB_bien_formado' aridad) ∩
lists (terminoB_bien_formado aridad)"
using H1 by (simp add: lists_Int_eq)
hence "ys ∈ lists (terminoB_bien_formado aridad)" by simp
thus "Aplica f ys ∈ terminoB_bien_formado aridad" using H2 by auto
qed
thus ?thesis ..
qed
-- "La demostración anterior se puede simplificar:"
lemma
"terminoB_bien_formado' aridad ⊆ terminoB_bien_formado aridad"
proof -
have "⋀x. x ∈ terminoB_bien_formado' aridad ⟹
x ∈ terminoB_bien_formado aridad"
proof (erule terminoB_bien_formado'.induct)
fix x ys f
assume "ys ∈ lists (terminoB_bien_formado' aridad ∩
{a. a ∈ terminoB_bien_formado aridad})"
"length ys = aridad f"
thus "Aplica f ys ∈ terminoB_bien_formado aridad" by auto
qed
thus ?thesis ..
qed
end
