Razonamiento sobre árboles y bosques

chapter ‹Tema 8: Razonamiento sobre árboles›

theory T8_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.›

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 ‹Regla de inducción correspondiente a los árboles binarios:
  La regla de inducción sobre árboles binarios es arbol.induct:
  ⟦ ⋀x. P (Hoja x);
    ⋀x i d. ⟦P i; P d⟧ ⟹ P (Nodo x i d)⟧ 
  ⟹ P a
›

thm arbolB.induct

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 declarativa es›
lemma 
  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

― ‹La demostración declarativa detallada es›
lemma 
  fixes a :: "'b arbolB" 
  shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (Hoja x)"  
    by (simp only: espejo.simps(1)) 
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 only: espejo.simps(2))
    also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" 
      by (simp only: espejo.simps(2))
    also have "… = Nodo x i d" 
      by (simp only: h1 h2) 
    finally show ?thesis 
      by this
  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 (espejo a) = a"
  by (induct a) simp_all  

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 declarativa 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

― ‹Lema auxiliar para la demostración declarativa detallada›
lemma rev_unit: "rev [x] = [x]"
proof -
  have "rev [x] = rev [] @ [x]" 
    by (simp only: rev.simps(2))
  also have "… = [] @ [x]"
    by (simp only: rev.simps(1))
  also have "… = [x]"
    by (simp only: append.simps(1))
  finally show ?thesis
    by this
qed

― ‹La demostración estructurada y detallada es›
lemma 
  fixes a :: "'b arbolB"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x :: 'b
  have "aplana (espejo (Hoja x)) = aplana (Hoja x)"
    by (simp only: espejo.simps(1))
  also have "… = [x]"
    by (simp only: aplana.simps(1))
  also have "… = rev [x]"
    by (simp only: rev_unit)
  also have "… = rev (aplana (Hoja x))"
    by (simp only: aplana.simps(1))
  finally show "?P (Hoja x)" 
    by this 
next
  fix x :: 'b
  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 only: espejo.simps(2))
    also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" 
      by (simp only: aplana.simps(2))
    also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" 
      by (simp only: h1 h2)
    also have "… = rev ((aplana i) @ [x] @ (aplana d))" 
      by (simp only: rev_append rev_unit append_assoc)
    also have "… = rev (aplana (Nodo x i d))" 
      by (simp only: aplana.simps(2))
    finally show ?thesis 
      by this
  qed
qed

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

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 = 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:
     ⟦⋀x b. P2 b ⟹ P1 (Nodo x b); 
      P2 Vacio;
      ⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ 
     ⟹ P1 a ∧ P2 b›

thm arbol_bosque.induct

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 f a) es el árbol obtenido aplicando la función f a
    todos los nodos del árbol a.   
  · (map_bosque f b) es el bosque obtenido aplicando la función f a
    todos los nodos del bosque b. ›

fun aplana_arbol :: "'a arbol ⇒ 'a list" and 
    aplana_bosque :: "'a bosque ⇒ 'a list" where
  "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 (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)›

declare [[names_short]] 

― ‹La demostración declarativa 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)
  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))" 
    by this
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 this
qed

― ‹La demostración declarativa 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)
  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 only: map_arbol.simps(1))
  also have "… = (f x) # (aplana_bosque (map_bosque f b))" 
    by (simp only: aplana_arbol.simps(1))
  also have "… = (f x) # (map f (aplana_bosque b))" 
    by (simp only: HI)
  also have "… = map f (aplana_arbol (Nodo x b))" 
    by (simp only: list.map aplana_arbol.simps(1))
  finally show "aplana_arbol (map_arbol f (Nodo x b)) =
                map f (aplana_arbol (Nodo x b))" 
    by this
next
  show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" 
    by (simp only: aplana_bosque.simps(1)
                   map_bosque.simps(1)
                   list.map)
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 only: map_bosque.simps(2))
  also have "… = aplana_arbol (map_arbol f a) @ 
                  aplana_bosque (map_bosque f b)" 
    by (simp only: aplana_bosque.simps(2))
  also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" 
    by (simp only: HI1 HI2)
  also have "… = map f (aplana_arbol a @ aplana_bosque b)"
    by (simp only: map_append)
  also have "… = map f (aplana_bosque (ConsB a b))" 
    by (simp only: aplana_bosque.simps(2))
  finally show "aplana_bosque (map_bosque f (ConsB a b)) =
                map f (aplana_bosque (ConsB a b))" 
    by this
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 3 casos:
    1. ⋀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))
    2. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
    3. ⋀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) simp_all

end