Menu Close

LMF2019: Razonamiento sobre árboles y bosques en Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir y razonar en Isabelle/HOL tipos de datos recursivos como árboles binarios, árboles generales y bosques. En su definición se usa recursión cruzada y en la demostración de sus propiedades se usa inducción doble.

La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte: Razonamiento sobre árboles binarios

  • Segunda parte: Árboles y bosques: Recursión mutua e inducción

La teoría utilizada es la siguiente

chapter ‹Tema 8: Razonamiento sobre árboles›
 
theory T8_Razonamiento_sobre_arboles
imports Main 
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 arbolB.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 "?P (Nodo x i d)" 
      by this
  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" 
      using h1 h2
      by (simp only:) 
    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 aplicativa es›
lemma  
  "espejo (espejo a) = a"
  apply (induct a)
   apply simp
  apply simp
  done
 
― ‹La demostración aplicativa detallada es›
lemma  
  "espejo (espejo a) = a"
  apply (induct a)
   apply (simp only: espejo.simps(1))
  apply (simp only: espejo.simps(2))
  done
 
― ‹La demostración automática es›
lemma  
  "espejo (espejo a) = a"
  by (induct a) simp+ 
 
― ‹La demostración automática detallada es›
lemma  
  "espejo (espejo a) = a"
  by (induct a) (simp only: espejo.simps)+  
 
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 "?P (Nodo x i d)" 
      by this
  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))"
      (* find_theorems "rev (_ @ _)" *)
      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 aplicativa es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply simp
  apply simp
  done
 
― ‹La demostración aplicativa detallada es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: espejo.simps(1) aplana.simps(1))
   apply (simp only: rev_unit)
  apply (simp only: espejo.simps(2) aplana.simps(2))
  apply (simp only: rev_append)
  apply (simp only: rev_unit)
  apply (simp only: append_assoc)
  done
 
― ‹La demostración aplicativa detallada compacta es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: 
      espejo.simps(1) 
      aplana.simps(1)
      rev_unit
      espejo.simps(2) 
      aplana.simps(2)
      rev_append
      append_assoc)+
  done
 
― ‹La demostración aplicativa detallada más compacta es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: 
      espejo.simps
      aplana.simps
      rev_unit
      rev_append
      append_assoc)+
  done
 
― ‹La demostración automática es›
lemma "aplana (espejo a) = rev (aplana a)"
  by (induct a) simp_all
 
― ‹La demostración automática detallada es›
lemma "aplana (espejo a) = rev (aplana a)"
  by (induct a)
     (simp only: 
      espejo.simps
      aplana.simps
      rev_unit
      rev_append
      append_assoc)+
 
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))"
    using HI
    by (simp only:)
  also have "… = map f (aplana_arbol (Nodo x b))" 
    (* find_theorems "map _ (_ # _)" *)
    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)"
    (* find_theorems "map _ (_ @ _)" *)
    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 aplicativa es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply simp+
  done
 
― ‹La demostración aplicativa 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)"
  apply (induct_tac a and b)
    apply (simp only: map_arbol.simps aplana_arbol.simps)
    apply (simp only: list.map(2))
   apply (simp only: map_bosque.simps(1) aplana_bosque.simps(1))
   apply (simp only: list.map(1))
  apply (simp only: map_bosque.simps(2) aplana_bosque.simps(2))
  apply (simp only: map_append)
  done
 
― ‹La demostración aplicativa detallada compacta es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply (simp only: 
      map_arbol.simps 
      aplana_arbol.simps
      list.map(2)
      map_bosque.simps(1) 
      aplana_bosque.simps(1)
      list.map(1)
      map_bosque.simps(2) 
      aplana_bosque.simps(2)
      map_append)+
  done
 
― ‹La demostración aplicativa detallada más compacta es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply (simp only: 
      map_arbol.simps 
      map_bosque.simps
      aplana_arbol.simps
      aplana_bosque.simps
      list.map
      map_append)+
  done
 
― ‹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+
 
― ‹La demostración automática 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)"
  by (induct_tac a and b) 
     (simp only: 
      map_arbol.simps 
      map_bosque.simps
      aplana_arbol.simps
      aplana_bosque.simps
      list.map
      map_append)+
 
end
LMF2019