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