Ver el código de «Tema 10: Conjuntos definidos inductivamente» - Razonamiento automático (2014-15)

<source lang="isar">
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
</source>