Relación 7
De Razonamiento automático (2014-15)
Revisión del 09:50 2 dic 2014 de Juacorvic (discusión | contribuciones)
header {* R7: Recorridos de árboles *}
theory R7
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]
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar,juacorvic"
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden (H x) = [x]"
|"preOrden (N x yy zz) = x#(preOrden yy @ preOrden zz)"
value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]" -- "True"
value "preOrden (N e (N c (N a1 (H a2) (H a3)) (H d)) (N g (H f) (H h)))
= [e, c, a1, a2, a3, d, g, f, h]" -- "True"
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)))
= [a,d,c,f,h,g,e]
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar,juacorvic"
fun postOrden :: "'a arbol ⇒ 'a list" where
"postOrden (H x) = [x]"
|"postOrden (N x yy zz)= postOrden yy @ postOrden zz @ [x]"
value "postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,d,c,f,h,g,e]" -- "True"
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]
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar,juacorvic"
fun inOrden :: "'a arbol ⇒ 'a list" where
"inOrden (H x) = [x]"
|"inOrden (N x yy zz) = inOrden yy @ [x] @ inOrden zz"
value "inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]" -- "True"
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))
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
fun espejo :: "'a arbol ⇒ 'a arbol" where
"espejo (H x) = (H x)"
|"espejo (N x yy zz) = (N x (espejo zz) (espejo yy))"
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))" -- "True"
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que
preOrden (espejo a) = rev (postOrden a)
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induct a, simp_all)
--"jeshorcob,davoremar"
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x yy zz
assume h1: "?P yy"
assume h2: "?P zz"
have "preOrden (espejo (N x yy zz))
= preOrden (N x (espejo zz) (espejo yy))" by simp
also have "... = x#(preOrden(espejo zz)@preOrden(espejo yy))" by simp
also have "... = x#rev(postOrden zz)@rev(postOrden yy)"
using h1 h2 by simp
also have "... = rev((postOrden yy)@(postOrden zz)@[x])" by simp
finally show "?P (N x yy zz)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que
postOrden (espejo a) = rev (preOrden a)
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a, simp_all)
--"jeshorcob,davoremar"
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x y z
assume h1: "?P y"
assume h2: "?P z"
have "postOrden (espejo (N x y z)) =
postOrden (N x (espejo z) (espejo y))" by simp
also have "... = postOrden(espejo z)@postOrden(espejo y)@[x]" by simp
also have "... = rev(preOrden z)@rev(preOrden y)@[x]"
using h1 h2 by simp
also have "... = rev(x#(preOrden y)@(preOrden z))" by simp
finally show "?P (N x y z)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que
inOrden (espejo a) = rev (inOrden a)
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a, simp_all)
--"jeshorcob,davoremar"
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x y z
assume h1: "?P y"
assume h2: "?P z"
have "inOrden(espejo (N x y z)) =
inOrden(N x (espejo z) (espejo y))" by simp
also have "... = inOrden(espejo z)@[x]@inOrden(espejo y)" by simp
also have "... = rev(inOrden z)@[x]@rev(inOrden y)" using h1 h2 by simp
also have "... = rev(inOrden y @ [x] @ inOrden z)" by simp
finally show "?P (N x y z)" 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
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
fun raiz :: "'a arbol ⇒ 'a" where
"raiz (H x) = x"
|"raiz (N x _ _ ) = x"
value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e" -- "True"
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
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
"extremo_izquierda (H x) = x"
|"extremo_izquierda (N _ yy _) = extremo_izquierda yy"
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
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
fun extremo_derecha :: "'a arbol ⇒ 'a" where
"extremo_derecha (H x) = x"
|"extremo_derecha (N _ _ zz) = extremo_derecha zz"
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
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
(*jeshorcob: al intentar hacer la prueba automática, el sistema se
pregunta por el caso en el que la lista sea vacía. Debemos indicar que
esto no puede ocurrir y para ello añadimos un lema auxiliar.*)
lemma a1: "inOrden a ≠ []"
by (induct a, simp_all)
--"jeshorcob,davoremar"
theorem "last (inOrden a) = extremo_derecha a"
by (induct a, simp_all add: a1)
--"jeshorcob,davoremar"
lemma "inOrden a ≠ []"
proof (induct a)
fix x::"'a" show "inOrden (H x) ≠ []" by simp
next
fix x::"'a" and y z::"'a arbol"
assume h1: "inOrden y ≠ []"
assume h2: "inOrden z ≠ []"
show "inOrden (N x y z) ≠ []" using h1 h2 by simp
qed
--"jeshorcob,davoremar"
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x y z
assume h2: "?P z"
have "last(inOrden(N x y z))=last(inOrden y @[x]@ inOrden z)" by simp
also have "... = last(inOrden z)" by (simp add: a1)
also have "... = extremo_derecha z" using h2 by simp
finally show "?P (N x y z)" by simp
qed
--"Pedrosrei"
theorem "last (inOrden a) = extremo_derecha a"
apply (induct a, simp_all) apply (metis append_is_Nil_conv arbol.exhaust
inOrden.simps(1) inOrden.simps(2) list.distinct(1)) done
text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
hd (inOrden a) = extremo_izquierda a
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
(*jeshorcob: aquí necesitamos el mismo lema por un motivo similar*)
theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a, simp_all add: a1)
--"jeshorcob,davoremar"
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x y z
assume h1: "?P y"
have "hd(inOrden(N x y z))=hd(inOrden y @[x]@ inOrden z)" by simp
also have "... = hd(inOrden y)" by (simp add: a1)
also have "... = extremo_izquierda y" using h1 by simp
finally show "?P (N x y z)" by simp
qed
--"Pedrosrei"
theorem "hd (inOrden a) = extremo_izquierda a"
apply (induct a, simp_all) apply (metis Nil_is_append_conv
extremo_izquierda.cases hd_append inOrden.simps(1) inOrden.simps(2)
list.distinct(1)) done
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
hd (preOrden a) = last (postOrden a)
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
theorem "hd (preOrden a) = last (postOrden a)"
by (induct a, simp_all)
--"jeshorcob,davoremar"
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x::"'a" and y z
have "hd(preOrden(N x y z)) = hd(x#(preOrden y @ preOrden z))" by simp
also have "... = x" by simp
also have "... = last(postOrden y @ postOrden z @[x])" by simp
finally show "?P (N x y z)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
theorem "hd (preOrden a) = raiz a"
by (induct a, simp_all)
--"jeshorcob,davoremar"
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x::"'a" and y z
have "hd(preOrden(N x y z)) = hd(x#(preOrden y @ preOrden z))" by simp
also have "... = x" by simp
finally show "?P (N x y z)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
theorem "hd (inOrden a) = raiz a"
quickcheck
oops
(*Encuentra el contrajemplo:
a = N a⇩1 (H a⇩2) (H a⇩1)
ya que evaluando se ve que son distindos:
hd (inOrden a) = a⇩2
raiz a = a⇩1
*)
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar"
theorem "last (postOrden a) = raiz a"
by (induct a, simp_all)
--"jeshorcob,davoremar"
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x::"'a" and y z
have "last(postOrden(N x y z)) =
last(postOrden y @ postOrden z @ [x])" by simp
also have "... = x" by simp
finally show "?P (N x y z)" by simp
qed
end