chapter {* R5: Recorridos de árboles *}
theory R5_Recorridos_de_arboles
imports Main
begin
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que tiene información en los nodos y en las hojas.
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
a d f h
se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
---------------------------------------------------------------------
*}
datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"
value "N e (N c (H a) (H d)) (N g (H f) (H h))"
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
preOrden :: "'a arbol ⇒ 'a list"
tal que (preOrden a) es el recorrido pre orden del árbol a. Por
ejemplo,
preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]
---------------------------------------------------------------------
*}
(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden (H x) = [x]"
| "preOrden (N x i d) = x # preOrden i @ preOrden d"
value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]"
text {*
---------------------------------------------------------------------
Ejercicio 3. Definir la función
postOrden :: "'a arbol ⇒ 'a list"
tal que (postOrden a) es el recorrido post orden del árbol a. Por
ejemplo,
postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]
---------------------------------------------------------------------
*}
(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
fun postOrden :: "'a arbol ⇒ 'a list" where
"postOrden (H x) = [x]"
| "postOrden (N x i d) = postOrden i @ postOrden d @ [x]"
value "postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,d,c,f,h,g,e]"
text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
inOrden :: "'a arbol ⇒ 'a list"
tal que (inOrden a) es el recorrido in orden del árbol a. Por
ejemplo,
inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]
---------------------------------------------------------------------
*}
(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
fun inOrden :: "'a arbol ⇒ 'a list" where
"inOrden (H x) = [x]"
| "inOrden (N x i d) = inOrden i @ x # inOrden d"
value "inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]"
text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
espejo :: "'a arbol ⇒ 'a arbol"
tal que (espejo a) es la imagen especular del árbol a. Por ejemplo,
espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))
---------------------------------------------------------------------
*}
(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
fun espejo :: "'a arbol ⇒ 'a arbol" where
"espejo (H x) = (H x)"
| "espejo (N x i d) = (N x (espejo d) (espejo i))"
value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))"
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que
preOrden (espejo a) = rev (postOrden a)
---------------------------------------------------------------------
*}
(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod jospermon1*)
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induct a) auto
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. preOrden (espejo (H x)) = rev (postOrden (H x))" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "preOrden (espejo (N x i d)) = preOrden (N x (espejo d) (espejo i))" by simp
also have "... = x # preOrden (espejo d) @ preOrden (espejo i)" by simp
also have "... = x # rev (postOrden d) @ rev (postOrden i)" using H1 H2 by simp
also have "... = rev((postOrden i) @ (postOrden d) @ [x])" by simp
finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" by simp
qed
(*anddonram*)
lemma
fixes a :: "'b arbol"
shows "preOrden (espejo a) = rev (postOrden a)"
proof (induct a)
(*Si no pones el tipo da un warning. ¿Por qué?*)
fix x::'b
show " preOrden (espejo (H x)) = rev (postOrden (H x))" by simp
next
fix x1a
(*Si no pones el tipo da un error. ¿Por qué?*)
fix a1:: "'b arbol"
assume H1:" preOrden (espejo a1) = rev (postOrden a1)"
fix a2:: "'b arbol"
assume H2:" preOrden (espejo a2) = rev (postOrden a2)"
have "preOrden (espejo (N x1a a1 a2)) = preOrden (N x1a (espejo a2) (espejo a1)) "
by simp
also have "... = [x1a] @ (preOrden (espejo a2)) @ (preOrden (espejo a1)) " by simp
also have "... = [x1a] @ rev (postOrden a2) @ rev (postOrden a1) " using H1 H2 by simp
also have "... = rev( (postOrden a1) @ (postOrden a2) @ [x1a]) " by simp
finally show "preOrden (espejo (N x1a a1 a2)) = rev (postOrden (N x1a a1 a2)) "
by simp
qed
(* cesgongut *)
(* creo que es lo mismo que luicedval et al. *)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (N x i d)"
proof -
have "preOrden (espejo (N x i d)) =
preOrden (N x (espejo d) (espejo i))" by simp
also have "… = rev (postOrden (N x i d))" using h1 h2 by simp
finally show ?thesis .
qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que
postOrden (espejo a) = rev (preOrden a)
---------------------------------------------------------------------
*}
(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1 *)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a) auto
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. postOrden (espejo (H x)) = rev (preOrden (H x))" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "postOrden (espejo (N x i d)) = postOrden (N x (espejo d) (espejo i))" by simp
also have "... = postOrden (espejo d) @ postOrden (espejo i) @ [x]" by simp
also have "... = rev (preOrden d) @ rev (preOrden i) @ [x]" using H1 H2 by simp
also have "... = rev(x # (preOrden i) @ (preOrden d))" by simp
finally show "postOrden (espejo (N x i d)) = rev (preOrden (N x i d))" by simp
qed
(*anddonram*)
lemma
fixes a :: "'b arbol"
shows "postOrden (espejo a) = rev (preOrden a)"
proof (induct a)
fix x::'b
show "postOrden (espejo (H x)) = rev (preOrden (H x))" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:"postOrden (espejo a1) = rev (preOrden a1)"
fix a2:: "'b arbol"
assume H2:"postOrden (espejo a2) = rev (preOrden a2)"
have "postOrden (espejo (N x1a a1 a2)) = postOrden (N x1a (espejo a2) (espejo a1)) "
by simp
also have "... = (postOrden (espejo a2)) @ (postOrden (espejo a1)) @ [x1a] " by simp
also have "... = rev (preOrden a2) @ rev (preOrden a1) @ [x1a]" using H1 H2 by simp
also have "... = rev([x1a] @ (preOrden a1) @ (preOrden a2) ) " by simp
finally show "postOrden (espejo (N x1a a1 a2)) = rev (preOrden (N x1a a1 a2))"
by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que
inOrden (espejo a) = rev (inOrden a)
---------------------------------------------------------------------
*}
(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) auto
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. inOrden (espejo (H x)) = rev (inOrden (H x))" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "inOrden (espejo (N x i d)) = inOrden (N x (espejo d) (espejo i))" by simp
also have "... = inOrden (espejo d) @ x # (inOrden (espejo i)) " by simp
also have "... = rev (inOrden d) @ x # rev (inOrden i) " using H1 H2 by simp
also have "... = rev( (inOrden i) @ x # (inOrden d)) " by simp
finally show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" by simp
qed
(*anddonram*)
theorem
fixes a :: "'b arbol"
shows "inOrden (espejo a) = rev (inOrden a)"
proof (induct a)
fix x::'b
show "inOrden (espejo (H x)) = rev (inOrden (H x))" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:" inOrden (espejo a1) = rev (inOrden a1)"
fix a2:: "'b arbol"
assume H2:" inOrden (espejo a2) = rev (inOrden a2)"
have "inOrden (espejo (N x1a a1 a2)) = inOrden (N x1a (espejo a2) (espejo a1)) "
by simp
also have "... = (inOrden (espejo a2)) @ [x1a]@ (inOrden (espejo a1)) " by simp
also have "... = rev (inOrden a2) @ [x1a] @ rev (inOrden a1) " using H1 H2 by simp
also have "... = rev((inOrden a1) @ [x1a] @ (inOrden a2) ) " by simp
finally show " inOrden (espejo (N x1a a1 a2)) = rev (inOrden (N x1a a1 a2))"
by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 9. Definir la función
raiz :: "'a arbol ⇒ 'a"
tal que (raiz a) es la raiz del árbol a. Por ejemplo,
raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e
---------------------------------------------------------------------
*}
(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
fun raiz :: "'a arbol ⇒ 'a" where
"raiz (H x) = x"
| "raiz (N x i d) = x"
value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e"
text {*
---------------------------------------------------------------------
Ejercicio 10. Definir la función
extremo_izquierda :: "'a arbol ⇒ 'a"
tal que (extremo_izquierda a) es el nodo más a la izquierda del árbol
a. Por ejemplo,
extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a
---------------------------------------------------------------------
*}
(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
"extremo_izquierda (H x) = x"
| "extremo_izquierda (N x i d) = extremo_izquierda i"
value "extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a"
text {*
---------------------------------------------------------------------
Ejercicio 11. Definir la función
extremo_derecha :: "'a arbol ⇒ 'a"
tal que (extremo_derecha a) es el nodo más a la derecha del árbol
a. Por ejemplo,
extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h
---------------------------------------------------------------------
*}
(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
fun extremo_derecha :: "'a arbol ⇒ 'a" where
"extremo_derecha (H x) = x"
| "extremo_derecha (N x i d) = extremo_derecha d"
value "extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h"
text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar
last (inOrden a) = extremo_derecha a
---------------------------------------------------------------------
*}
(*anddonram*)
lemma inOrdenNoVacio: "inOrden a ≠ []" by (cases a) auto
theorem
fixes a :: "'b arbol"
shows "last (inOrden a) = extremo_derecha a"
proof (induct a)
fix x::'b
show "last (inOrden (H x)) = extremo_derecha (H x)" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:"last (inOrden a1) = extremo_derecha a1"
fix a2:: "'b arbol"
assume H2:"last (inOrden a2) = extremo_derecha a2"
have "last (inOrden (N x1a a1 a2)) = last( (inOrden a1) @ [x1a] @ (inOrden a2)) "
by simp
also have "... = last( [x1a] @ inOrden a2) " by simp
also have "... = last (inOrden a2) " by (simp add:inOrdenNoVacio)
also have "... = extremo_derecha a2 " using H2 by simp
finally show "last (inOrden (N x1a a1 a2)) = extremo_derecha (N x1a a1 a2)"
by simp
qed
(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
lemma inOrdenNoVacio: "inOrden a ≠ []" by (cases a) auto
(* Créditos Andrés, no sabía como hacerlo *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i
fix d assume H1: "?P d"
have "last (inOrden (N x i d)) = last (inOrden i @ x # inOrden d)" by simp
also have "... = last (x # inOrden d)" by simp
also have "... = last (inOrden d)" by (simp add:inOrdenNoVacio)
also have "... = extremo_derecha d" using H1 by simp
finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
hd (inOrden a) = extremo_izquierda a
---------------------------------------------------------------------
*}
(*anddonram*)
theorem
fixes a :: "'b arbol"
shows "hd (inOrden a) = extremo_izquierda a"
proof (induct a)
fix x::'b
show "hd (inOrden (H x)) = extremo_izquierda (H x)" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:" hd (inOrden a1) = extremo_izquierda a1"
fix a2:: "'b arbol"
assume H2:" hd (inOrden a2) = extremo_izquierda a2"
have "hd (inOrden (N x1a a1 a2)) = hd ( (inOrden a1) @ [x1a] @ (inOrden a2)) "
by simp
also have "... = hd (inOrden a1) " by (simp add:inOrdenNoVacio)
also have "... = extremo_izquierda a1 " using H1 by simp
finally show " hd (inOrden (N x1a a1 a2)) = extremo_izquierda (N x1a a1 a2)"
by simp
qed
(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d
have "hd (inOrden (N x i d)) = hd (inOrden i @ x # inOrden d)" by simp
also have "... = hd (inOrden i)" by (simp add:inOrdenNoVacio)
also have "... = extremo_izquierda i" using H1 by simp
finally show "hd (inOrden (N x i d)) = extremo_izquierda (N x i d)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
hd (preOrden a) = last (postOrden a)
---------------------------------------------------------------------
*}
(*anddonram*)
theorem
fixes a :: "'b arbol"
shows "hd (preOrden a) = last (postOrden a)"
proof (induct a)
fix x::'b
show "hd (preOrden (H x)) = last (postOrden (H x))" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:"hd (preOrden a1) = last (postOrden a1)"
fix a2:: "'b arbol"
assume H2:"hd (preOrden a2) = last (postOrden a2)"
have "hd (preOrden (N x1a a1 a2)) = hd ( [x1a] @ (preOrden a1) @ (preOrden a2)) "
by simp
also have "... = x1a " by simp
also have "... = last ((preOrden a1) @ (preOrden a2)@ [x1a])" by simp
finally show "hd (preOrden (N x1a a1 a2)) = last (postOrden (N x1a a1 a2))"
by simp
qed
(* luicedval rafcabgon rafferrod*)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "hd (preOrden (N x i d)) = hd (x # preOrden i @ preOrden d)" by simp
also have "... = x" by simp
also have "... = last (postOrden d @ postOrden i @ [x])" by simp
finally show "hd (preOrden (N x i d)) = last (postOrden (N x i d))" by simp
qed
(* edupalhid *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
show "?P (N x i d)" by simp
qed
(* cesgongut *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
show "?P (N x i d)"
proof -
have "hd (preOrden (N x i d)) = hd (x # preOrden d @ preOrden i)" by simp
also have "... = x" by simp
next
have "last (postOrden (N x i d)) =
last (postOrden d @ postOrden i @ [x])" by simp
also have "... = x" by simp
finally show ?thesis by simp
qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
*}
(*anddonram diwu2 *)
theorem "hd (preOrden a) = raiz a"
proof (induct a)
fix x::'b
show "hd (preOrden (H x)) = raiz (H x)" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:" hd (preOrden a1) = raiz a1"
fix a2:: "'b arbol"
assume H2:" hd (preOrden a2) = raiz a2"
have "hd (preOrden (N x1a a1 a2)) = hd ( [x1a] @ (preOrden a1) @ (preOrden a2)) "
by simp
also have "... = x1a " by simp
finally show "hd (preOrden (N x1a a1 a2)) = raiz (N x1a a1 a2)"
by simp
qed
(* luicedval rafcabgon macmerflo rafferrod cesgongut jospermon1*)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "hd (preOrden (N x i d)) = hd (x # preOrden i @ preOrden d)" by simp
also have "... = x" by simp
finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp
qed
(* edupalhid *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
show "?P (N x i d)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
*}
(*anddonram luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
theorem "hd (inOrden a) = raiz a"
quickcheck
oops
(*
Quickcheck found a counterexample:
a = N a⇩1 (H a⇩2) (H a⇩1)
Evaluated terms:
hd (inOrden a) = a⇩2
raiz a = a⇩1
*)
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
*}
(*anddonram*)
theorem "last (postOrden a) = raiz a"
proof (induct a)
fix x::'b
show "last (postOrden (H x)) = raiz (H x)" by simp
next
fix x1a
fix a1:: "'b arbol"
assume H1:"last (postOrden a1) = raiz a1 "
fix a2:: "'b arbol"
assume H2:"last (postOrden a2) = raiz a2"
have " last (postOrden (N x1a a1 a2)) = last ( (preOrden a1) @ (preOrden a2)@[x1a] ) "
by simp
also have "... = x1a " by simp
finally show " last (postOrden (N x1a a1 a2)) = raiz (N x1a a1 a2)"
by simp
qed
(* luicedval oscgonesc diwu2 rafcabgon macmerflo rafferrod cesgongut jospermon1*)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x::"'b arbol"
show "⋀x. ?P (H x)" by simp
next
fix x
fix i assume H1: "?P i"
fix d assume H2: "?P d"
have "last (postOrden (N x i d)) = last (postOrden i @ postOrden d @ [x])" by simp
also have "... = last (postOrden d @ [x])" by simp
also have "... = x" by simp
finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp
qed
(* edupalhid *)
theorem "last (postOrden a) = raiz a"
apply (induct a)
apply simp
apply simp
done
end
(* edupalhid *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
fix x i d
show "?P (N x i d)" by simp
qed
