Ver el código de «Tema 5: Razonamiento sobre árboles y bosques» - Razonamiento automático (2018-19)

<source lang="isabelle">
chapter {* Tema 5: Razonamiento sobre árboles *}

theory T5_Razonamiento_sobre_arboles
imports Main HOL.Parity
begin

text {*
  En este tema se estudia razonamiento sobre otras estructuras
  recursivas como árboles binarios, árboles generales y bosques.
  
  También se muestra cómo definir tipos de datos por recursión cruzada y
  la demostración de sus propiedades por inducción.
*}

text {*
  Se usarán nombres cortos. *}
  
declare [[names_short]]

section {* Razonamiento sobre árboles binarios *}

text {* 
  Ejemplo de definición de tipos recursivos:
  Definir un tipo de dato para los árboles binarios.
*}

datatype 'a arbolB = Hoja "'a" 
                   | Nodo "'a" "'a arbolB" "'a arbolB"

text {* 
  Ejemplo de definición sobre árboles binarios:
  Definir la función "espejo" que aplicada a un árbol devuelve su imagen
  especular.  
*}

fun espejo :: "'a arbolB ⇒ 'a arbolB" where
  "espejo (Hoja x)     = (Hoja x)"
| "espejo (Nodo x i d) = (Nodo x (espejo d) (espejo i))"

value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = 
      Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))"

text {* 
  Ejemplo de demostración sobre árboles binarios:
  Demostrar que la función "espejo" es involutiva; es decir, para
  cualquier árbol a, se tiene que 
     espejo (espejo a) = a.
*}

― ‹La demostración estructurada es›
lemma espejo_involutiva:
  fixes a :: "'b arbolB" 
  shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (Hoja x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "espejo (espejo (Nodo x i d)) = 
          espejo (Nodo x (espejo d) (espejo i))" by simp
    also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" 
      by simp
    also have "… = Nodo x i d" using h1 h2 by simp 
    finally show ?thesis .
 qed
qed

text {*
  Comentarios sobre la demostración anterior:
  · (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario
    cuyos elementos son de tipo b". 
  · (induct a) indica que el método de demostración es por inducción
    en el árbol binario a.
  · Se generan dos casos:
    1. ⋀a. espejo (espejo (Hoja a)) = Hoja a
    2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; 
                   espejo (espejo a3) = a3⟧
                  ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3
*}

― ‹La demostración automática es›
lemma espejo_involutiva_1: 
  "espejo (espejo a ) = a"
by (induct a) auto

text {* 
  Ejemplo. [Aplanamiento de árboles]
  Definir la función "aplana" que aplane los árboles recorriéndolos en
  orden infijo.  
*}

fun aplana :: "'a arbolB ⇒ 'a list" where
  "aplana (Hoja x)     = [x]"
| "aplana (Nodo x i d) = (aplana i) @ [x] @ (aplana d)"

value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = 
      [c, b, d, a, e]"

text {* 
  Ejemplo. [Aplanamiento de la imagen especular] Demostrar que
     aplana (espejo a) = rev (aplana a)
*}

― ‹La demostración estructurada es›
lemma 
  fixes a :: "'b arbolB"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (Hoja x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "aplana (espejo (Nodo x i d)) = 
          aplana (Nodo x (espejo d) (espejo i))" by simp
    also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" 
      by simp
    also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" 
      using h1 h2 by simp
    also have "… = rev ((aplana i) @ [x] @ (aplana d))" by simp
    also have "… = rev (aplana (Nodo x i d))" by simp
    finally show ?thesis .
 qed
qed

― ‹La demostración automática es›
lemma "aplana (espejo a) = rev (aplana a)"
by (induct a) auto

section {* Árboles y bosques. Recursión mutua e inducción *}

text {*
  Nota. [Ejemplo de definición de tipos mediante recursión cruzada]
  · Un árbol de tipo a es una hoja o un nodo de tipo a junto con un
    bosque de tipo a.
  · Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo
    un árbol de tipo a a un bosque de tipo a.
*}

datatype 'a arbol = Hoja | Nodo "'a" "'a bosque"
     and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"

text {*
  Regla de inducción correspondiente a la recursión cruzada:
  La regla de inducción sobre árboles y bosques es arbol_bosque.induct:
     ⟦P1 Hoja; 
      ⋀x b. P2 b ⟹ P1 (Nodo x b); 
      P2 Vacio;
      ⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ 
     ⟹ P1 a ∧ P2 b
*}

text {* 
  Ejemplos de definición por recursión cruzada:
  · aplana_arbol a) es la lista obtenida aplanando el árbol a.   
  · (aplana_bosque b) es la lista obtenida aplanando el bosque b.   
  · (map_arbol a h) es el árbol obtenido aplicando la función h a
    todos los nodos del árbol a.   
  · (map_bosque b h) es el bosque obtenido aplicando la función h a
    todos los nodos del bosque b. 
*}

fun aplana_arbol :: "'a arbol ⇒ 'a list" and 
    aplana_bosque :: "'a bosque ⇒ 'a list" where
  "aplana_arbol Hoja = []"
| "aplana_arbol (Nodo x b) = x # (aplana_bosque b)"
| "aplana_bosque Vacio = []"
| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"

fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and
    map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where
  "map_arbol  f Hoja        = Hoja"
| "map_arbol  f (Nodo x b)  = Nodo (f x) (map_bosque f b)"
| "map_bosque f Vacio       = Vacio"
| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"

text {*
  Ejemplo de demostración por inducción cruzada:
  Demostrar que:
  · aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
  · aplana_bosque (map_bosque f b) = map f (aplana_bosque b)
*}

― ‹La demostración detallada es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
  show "aplana_arbol (map_arbol f Hoja ) = map f (aplana_arbol Hoja)" 
    by simp
next
  fix x b
  assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_arbol (map_arbol f (Nodo x b)) = 
        aplana_arbol (Nodo (f x) (map_bosque f b))" by simp
  also have "… = (f x) # (aplana_bosque (map_bosque f b))" by simp
  also have "… = (f x) # (map f (aplana_bosque b))" using HI by simp
  also have "… = map f (aplana_arbol (Nodo x b))" by simp
  finally show "aplana_arbol (map_arbol f (Nodo x b))
                = map f (aplana_arbol (Nodo x b))" .
next
  show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" 
    by simp
next
  fix a b
  assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
     and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_bosque (map_bosque f (ConsB a b)) = 
        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp
  also have "… = aplana_arbol (map_arbol f a) @ 
                  aplana_bosque (map_bosque f b)" 
    by simp
  also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" 
    using HI1 HI2 by simp
  also have "… = map f (aplana_bosque (ConsB a b))" by simp
  finally show "aplana_bosque (map_bosque f (ConsB a b)) 
                = map f (aplana_bosque (ConsB a b))" by simp
qed

text {*
  Comentarios sobre la demostración anterior:
  · (induct_tac a and b) indica que el método de demostración es por
    inducción cruzada sobre a y b.
  · Se generan 4 casos:
    1. aplana_arbol (map_arbol arbol.Hoja h) = map h (aplana_arbol arbol.Hoja)
    2. ⋀a bosque.
          aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹
          aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =
          map h (aplana_arbol (arbol.Nodo a bosque))
    3. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
    4. ⋀arbol bosque.
          ⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);
           aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧
          ⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =
             map h (aplana_bosque (ConsB arbol bosque))
*}

― ‹La demostración automática es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
by (induct_tac a and b) auto

end
</source>