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]
---------------------------------------------------------------------
*}
(* pabalagon manperjim raffergon2 aribatval benber josgomrom4 hugrubsan
cammonagu antramhur alfmarcua enrparalv marfruman1 gleherlop
chrgencar giafus1 pabbergue alikan juacanrod *)
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]
---------------------------------------------------------------------
*}
(* pabalagon manperjim raffergon2 aribatval benber josgomrom4 hugrubsan
cammonagu antramhur alfmarcua enrparalv marfruman1 gleherlop
chrgencar giafus1 pabbergue alikan juacanrod *)
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]
---------------------------------------------------------------------
*}
(* pabalagon manperjim raffergon2 aribatval benber josgomrom4 hugrubsan
gleherlop cammonagu alfmarcua enrparalv marfruman1 chrgencar giafus1
pabbergue alikan juacanrod antramhur *)
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))
---------------------------------------------------------------------
*}
(* pabalagon manperjim raffergon2 aribatval benber josgomrom4 hugrubsan
gleherlop cammonagu alfmarcua enrparalv marfruman1 chrgencar giafus1
pabbergue alikan juacanrod antramhur *)
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)
---------------------------------------------------------------------
*}
(* pabalagon manperjim raffergon2 josgomrom4 hugrubsan cammonagu
alfmarcua gleherlop enrparalv marfruman1 chrgencar pabbergue giafus1
alikan juacanrod aribatval antramhur *)
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i"
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 d @ [x]) @ rev (postOrden i)" by simp
also have "... = rev (postOrden i @ postOrden d @ [x])" by simp
finally show "?P (N x i d)" by simp
qed
(* benber *)
lemma "preOrden (espejo a) = rev (postOrden a)"
proof (induction a)
case (H v)
show ?case by simp
next
case IS: (N v l r)
have "preOrden (espejo (N v l r)) =
preOrden (N v (espejo r) (espejo l))" by simp
also have "... = v # (preOrden (espejo r)) @ (preOrden (espejo l))"
by simp
also have "... = v # rev (postOrden r) @ rev (postOrden l)"
using IS.IH by simp
also have "... = rev ((postOrden l) @ (postOrden r) @ [v])" by simp
also have "... = rev (postOrden (N v l r))" by simp
finally show ?case .
qed
(* cammonagu *)
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induction a) auto
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que
postOrden (espejo a) = rev (preOrden a)
---------------------------------------------------------------------
*}
(* pabalagon manperjim josgomrom4 hugrubsan cammonagu enrparalv
gleherlop chrgencar giafus1 pabbergue alikan aribatval *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i" and 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 (preOrden i @ preOrden d) @ rev [x]" by simp
also have "... = rev (x # preOrden i @ preOrden d)" by simp
finally show "?P (N x i d)" by simp
qed
(* raffergon2 alfmarcua marfruman1 juacanrod antramhur *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i"
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(preOrden d) @ rev (x # preOrden i)" by simp
also have "... = rev(x # preOrden i @ preOrden d)" by simp
finally show "?P (N x i d)" by simp
qed
(* benber cammonagu *)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induction a) auto
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que
inOrden (espejo a) = rev (inOrden a)
---------------------------------------------------------------------
*}
(* pabalagon manperjim josgomrom4 hugrubsan cammonagu enrparalv
gleherlop chrgencar giafus1 pabbergue alikan juacanrod aribatval *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i" and 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 "?P (N x i d)" by simp
qed
(* raffergon2 alfmarcua marfruman1 antramhur *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume H1: "?P i"
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(x # inOrden d) @ rev (inOrden i)" by simp
also have "... = rev(inOrden i @ x # inOrden d)" by simp
finally show "?P (N x i d)" by simp
qed
(* benber *)
theorem "inOrden (espejo a) = rev (inOrden a)"
proof (induction a)
case (H v)
show ?case by simp
next
case IS: (N v l r)
have "inOrden (espejo (N v l r)) =
inOrden (N v (espejo r) (espejo l))" by simp
also have "... = (inOrden (espejo r)) @ [v] @ (inOrden (espejo l))"
by simp
also have "... = (rev (inOrden r)) @ [v] @ (rev (inOrden l))"
using IS.IH by simp
also have "... = rev ((inOrden l) @ [v] @ (inOrden r))" by simp
also have"... = rev (inOrden (N v l r))" by simp
finally show ?case .
qed
(* cammonagu*)
lemma "inOrden (espejo a) = rev (inOrden a)"
by (induction a) auto
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
---------------------------------------------------------------------
*}
(* pabalagon manperjim raffergon2 aribatval benber josgomrom4 hugrubsan
cammonagu antramhur alfmarcua enrparalv marfruman1 gleherlop
chrgencar giafus1 pabbergue alikan juacanrod *)
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
---------------------------------------------------------------------
*}
(* pabalagon manperjim raffergon2 benber josgomrom4 gleherlop hugrubsan
cammonagu alfmarcua enrparalv marfruman1 chrgencar giafus1 pabbergue
alikan juacanrod aribatval antramhur *)
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
---------------------------------------------------------------------
*}
(* pabalagon manperjim raffergon2 benber josgomrom4 hugrubsan cammonagu
alfmarcua gleherlop enrparalv marfruman1 chrgencar giafus1 pabbergue
alikan juacanrod antramhur *)
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
---------------------------------------------------------------------
*}
(* pabalagon manperjim josgomrom4 hugrubsan cammonagu alfmarcua
enrparalv gleherlop chrgencar marfruman1 giafus1 pabbergue alikan
juacanrod antramhur *)
lemma inOrdenNotNil: "inOrden a ≠ []" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
have "?P (N x i d) = ((inOrden i @ [x] @ inOrden d) ≠ [])" by simp
also have "... = ((inOrden i ≠ []) ∨ ([x] ≠ []) ∨ (inOrden d ≠ []))"
by simp
also have "... = ([x] ≠ [])" by simp
finally show "?P (N x i d)" by simp
qed
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HI: "?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: inOrdenNotNil)
also have "... = extremo_derecha d" using HI by simp
also have "... = extremo_derecha (N x i d)" by simp
finally show "?P (N x i d)" .
qed
(* benber *)
theorem "last (inOrden a) = extremo_derecha a"
proof (induction a)
case (H v)
show ?case by simp
next
case IS: (N v l r)
have 1: "last (xs@ys) = last ys" if "ys ≠ []" for xs ys :: "'a list"
proof (induction xs)
case Nil
show ?case by simp
next
case IS: (Cons x xs)
have "last ((x#xs)@ys) = last (x#(xs@ys))" by simp
also have "... = last (xs @ ys)" using `ys ≠ []` by simp
also have "... = last ys" using IS.IH by simp
finally show ?case .
qed
have 2: "inOrden a ≠ []" for a :: "'a arbol"
by (induction a) auto
have "last (inOrden (N v l r)) =
last ( (inOrden l) @ [v] @ (inOrden r) )" by simp
also have "... = last (inOrden r)" using 1 2 by auto
also have "... = extremo_derecha r" using IS.IH by simp
also have "... = extremo_derecha (N v l r)" by simp
finally show ?case .
qed
text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
hd (inOrden a) = extremo_izquierda a
---------------------------------------------------------------------
*}
(* pabalagon manperjim josgomrom4 hugrubsan cammonagu alfmarcua
gleherlop enrparalv marfruman1 chrgencar giafus1 pabbergue alikan
juacanrod aribatval antramhur *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x::'a
have "hd (inOrden (H x)) = hd [x]" by simp
also have "... = x" by simp
also have "... = extremo_izquierda (H x)" by simp
finally show "?P (H x)" .
next
fix x i d
assume HI: "?P i"
have "hd (inOrden (N x i d)) = hd (inOrden i @ [x] @ inOrden d)"
by simp
also have "... = hd ((inOrden i @ [x]) @ inOrden d)" by simp
also have "... = hd (inOrden i)" by (simp add: inOrdenNotNil)
also have "... = extremo_izquierda i" using HI by simp
also have "... = extremo_izquierda (N x i d)" by simp
finally show "?P (N x i d)" .
qed
(* benber *)
theorem "hd (inOrden a) = extremo_izquierda a"
proof (induction a)
case (H v)
show ?case by simp
next
case IS: (N v l r)
moreover have "inOrden a ≠ []" for a :: "'a arbol"
by (induction a) auto
ultimately show ?case by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
hd (preOrden a) = last (postOrden a)
---------------------------------------------------------------------
*}
(* pabalagon manperjim josgomrom4 hugrubsan cammonagu alfmarcua
gleherlop marfruman1 chrgencar giafus1 pabbergue alikan juacanrod
aribatval antramhur *)
theorem hdPreOrden_lastPostOrden:
"hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x::'a
fix i d
have "hd (preOrden (N x i d)) = hd (x # preOrden i @ preOrden d)"
by simp
also have "... = x" by simp
also have "... = last [x]" by simp
also have "... = last (postOrden i @ postOrden d @ [x])" by simp
finally show "?P (N x i d)" by simp
qed
(* enrparalv *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x::'a
have "hd (preOrden (H x)) = hd [x]" by simp
also have "... = x" by simp
also have "... = last [x]" by simp
also have "... = last (postOrden (H x))" by simp
finally show "?P (H x)" by simp
next
fix x i d
have "hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d)"
by simp
also have "... = hd ([x] @ preOrden i)" by simp
also have "... = x" by simp
also have "... = last [x] " by simp
also have "... = last (postOrden i @ postOrden d @ [x]) " by simp
also have "... = last (postOrden (N x i d))" by simp
finally show "?P (N x i d)" by simp
oops
(* benber cammonagu *)
theorem "hd (preOrden a) = last (postOrden a)"
by (cases a) auto
text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
*}
(* pabalagon manperjim josgomrom4 hugrubsan cammonagu alfmarcua
gleherlop marfruman1 chrgencar giafus1 pabbergue alikan juacanrod
aribatval antramhur *)
theorem hdPreOrden_raiz: "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x::'a
fix i d
have "hd (preOrden (N x i d)) = hd (x # preOrden i @ preOrden d)"
by simp
also have "... = x" by simp
finally show "?P (N x i d)" by (simp only: raiz.simps(2))
qed
(* enrparalv *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x::'a
have "hd (preOrden (H x)) = hd [x]" by simp
also have "... = x " by simp
also have "... = raiz (H x)" by (simp only: raiz.simps(1))
finally show "?P (H x)" by simp
next
fix x i d
have "hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d)" by simp
also have "... = hd (([x] @ preOrden i) @ preOrden d)" by simp
also have "... = hd ([x] @ preOrden i)" by simp
also have "... = hd ([x])" by simp
also have "... = x" by simp
finally show "?P (N x i d)" by (simp only: raiz.simps(2))
oops
(* benber cammonagu*)
theorem "hd (preOrden a) = raiz a"
by (cases a) auto
text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
*}
(* pabalagon manperjim cammonagu alfmarcua marfruman1 gleherlop
chrgencar giafus1 pabbergue juacanrod hugrubsan alikan aribatval
antramhur *)
theorem "hd (inOrden a) = raiz a"
quickcheck
(*
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 *)
oops
(* benber josgomrom4 *)
(* El teorema no es cierto para arboles sobre numeros naturales *)
theorem "¬(∀ a :: nat arbol. hd (inOrden a) = raiz a)"
proof -
let ?a = "(N 0 (H 1) (H 2)) :: nat arbol"
have "hd (inOrden ?a) = 1" by simp
moreover have "raiz ?a = 0" by simp
ultimately have "hd (inOrden ?a) ≠ raiz ?a" by simp
hence "∃ a :: nat arbol. hd (inOrden a) ≠ raiz a" by (simp only: exI)
thus ?thesis by auto
qed
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
*}
(* pabalagon manperjim josgomrom4 cammonagu marfruman1 gleherlop
chrgencar giafus1 pabbergue juacanrod hugrubsan aribatval antramhur *)
theorem "last (postOrden a) = raiz a"
proof -
have "last (postOrden a) = hd (preOrden a)"
by (simp add: hdPreOrden_lastPostOrden)
also have "... = raiz a" by (simp add: hdPreOrden_raiz)
finally show "?thesis" .
qed
(* benber cammonagu*)
theorem "last (postOrden a) = raiz a"
by (cases a) auto
(* alfmarcua *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x::'a
fix i d
have "last (postOrden (N x i d)) =
last (postOrden i @ postOrden d @ [x])" by simp
also have "... = x" by simp
finally show "?P (N x i d)" by simp
qed
(* enrparalv *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x::'a
have "last (postOrden (H x)) = last [x]" by simp
also have "... = x" by simp
also have "... = raiz (H x)" by (simp only: raiz.simps(1))
finally show "?P (H x)" by simp
next
fix x i d
have "last (postOrden (N x i d)) =
last (postOrden i @ postOrden d @ [x])" by simp
also have "... = x" by simp
also have "... = raiz (N x i d)" by (simp only: raiz.simps(2))
finally show "?P (N x i d)" by simp
oops
end
