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
