chapter ‹Tema 9: Definiciones inductivas›
theory T9_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))
›
thm par.cero
thm par.paso
thm par.simps
subsection ‹Uso de las reglas de introducción›
text ‹
Lema: Los números de la forma 2*k son pares.
›
― ‹La demostración aplicativa es›
lemma dobles_son_pares [intro!]:
"2*k ∈ par"
apply (induct k)
(* 1. 2 * 0 ∈ par
2. ⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par *)
apply simp_all
(* *)
done
― ‹La demostración automática es›
lemma dobles_son_pares_2:
"2*k ∈ par"
by (induct k) auto
― ‹La demostración estructurada es›
lemma dobles_son_pares_3:
"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"
using dobles_son_pares_3 by blast
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
›
thm par.induct
text ‹Lema: Los números pares son divisibles por 2.›
― ‹Demostración aplicativa›
lemma par_imp_even:
"n ∈ par ⟹ even n"
apply (induction rule: par.induct)
(* 1. even 0
2. ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
apply (simp only: dvd_def)
(* 1. ∃k. 0 = 2 * k
2. ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
apply (rule_tac x=0 in exI)
(* 1. 0 = 2 * 0
2. ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
apply simp
(* ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
apply (simp only: dvd_def)
(* ⋀n. ⟦n ∈ par; ∃k. n = 2 * k⟧ ⟹ ∃k. Suc (Suc n) = 2 * k *)
apply (erule exE)
(* ⋀n k. ⟦n ∈ par; n = 2 * k⟧ ⟹ ∃k. Suc (Suc n) = 2 * k*)
apply (rule_tac x="k+1" in exI)
(* ⋀n k. ⟦n ∈ par; n = 2 * k⟧ ⟹ Suc (Suc n) = 2 * (k + 1) *)
apply simp
(* *)
done
― ‹2ª demostración aplicativa›
lemma par_imp_even_2:
"n ∈ par ⟹ even n"
apply (induction rule: par.induct)
(* 1. even 0
2. ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
apply simp_all
(* *)
done
― ‹Demostración automática›
lemma par_imp_even_3:
"n ∈ par ⟹ even n"
by (induction rule: par.induct) simp_all
― ‹Demostración declarativa›
lemma par_imp_even_4:
"n ∈ par ⟹ even n"
proof (induction rule: par.induct)
show "even 0"
by simp
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"
by (rule exE)
then have "Suc (Suc n) = 2*(k+1)"
by simp
then have "∃k. Suc (Suc n) = 2*k"
by (rule exI)
then show "even (Suc (Suc n))"
by (simp add: dvd_def)
qed
― ‹2ª demostración declarativa›
lemma par_imp_even_5:
"n ∈ par ⟹ even n"
proof (induction rule: par.induct)
show "even 0" by simp
next
fix n::nat
assume H1: "n ∈ par" and
H2: "even n"
then show "even (Suc (Suc n))"
by simp
qed
text ‹Lema: Un número n es par syss es divisible por 2.›
theorem par_iff_even: "(n ∈ par) = (even n)"
using even_imp_par par_imp_even_5 by blast
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)
(* 1. n ∈ par
2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par *)
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 aplicativa es›
lemma par_imp_par_menos:
"n ∈ par ⟹ n - 2 ∈ par"
apply (induction rule: par.induct)
(* 1. 0 - 2 ∈ par
2. ⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par *)
apply auto
(* *)
done
― ‹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 aplicativa es›
lemma
"Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (drule par_imp_par_menos_2)
(* Suc (Suc n) - 2 ∈ par ⟹ n ∈ par *)
apply simp
(* *)
done
― ‹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)
― ‹La demostración declarativa 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
text ‹Lemma. Un número natural n es par syss n+2 es par.›
lemma [iff]: "((Suc (Suc n)) ∈ par) = (n ∈ par)"
using Suc_Suc_par_imp_par by blast
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)
›
thm Pares_Impares.induct
text ‹Ejemplo de demostración usando el esquema anterior.›
― ‹Demostración aplicativa›
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
apply (induction rule: Pares_Impares.induct)
(* 1. even 0
2. ⋀n. ⟦n ∈ Impares; even (Suc n)⟧ ⟹ even (Suc n)
3. ⋀n. ⟦n ∈ Pares; even n⟧ ⟹ even (Suc (Suc n))*)
apply auto
(* *)
done
― ‹Demostración automática›
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
by (induction rule: Pares_Impares.induct) auto
― ‹La demostración declarativa es›
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"
by (rule exE)
then have "Suc (Suc n) = 2*(k+1)"
by auto
then have "∃k. Suc (Suc n) = 2*k"
by (rule exI)
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
