Tema 11: Definiciones inductivas

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