Sol 12
De Lógica matemática y fundamentos (2018-19)
<source lang = "isabelle"> chapter {* R12: Recorridos de árboles *}
theory R12_sol 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]
---------------------------------------------------------------------
- }
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]
---------------------------------------------------------------------
- }
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]
---------------------------------------------------------------------
- }
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))
---------------------------------------------------------------------
- }
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)
---------------------------------------------------------------------
- }
lemma "preOrden (espejo a) = rev (postOrden a)" by (induct a) simp_all
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a") proof (induct a)
fix x show "?P (H x)" by simp
next
fix a1 a2 a3 assume HI1: "?P a2" assume HI2: "?P a3" show "?P (N a1 a2 a3)" proof - have "preOrden (espejo (N a1 a2 a3)) = preOrden (N a1 (espejo a3) (espejo a2))" by simp also have "… = [a1] @ preOrden (espejo a3) @ preOrden (espejo a2)" by simp also have "… = rev [a1] @ rev (postOrden a3) @ rev (postOrden a2)" using HI1 HI2 by simp also have "… = rev ((postOrden a2) @ (postOrden a3) @ [a1])" by simp finally show ?thesis by simp qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que
postOrden (espejo a) = rev (preOrden a)
---------------------------------------------------------------------
- }
lemma "postOrden (espejo a) = rev (preOrden a)" by (induct a) simp_all
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 HI1: "?P i" assume HI2: "?P d" show "?P (N x i d)" proof - 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) @ rev [x]" using HI1 HI2 by simp also have "... = rev ([x] @ preOrden i @ preOrden d)" by simp finally show ?thesis by simp qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que
inOrden (espejo a) = rev (inOrden a)
---------------------------------------------------------------------
- }
lemma "inOrden (espejo a) = rev (inOrden a)" by (induct a) simp_all
lemma "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 HI1: "?P i" assume HI2: "?P d" show "?P (N x i d)" proof - 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) @ rev [x] @ rev (inOrden i)" using HI1 HI2 by simp also have "... = rev (inOrden i @ [x] @ inOrden d)" by simp finally show ?thesis by simp qed
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
---------------------------------------------------------------------
- }
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
---------------------------------------------------------------------
- }
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
"extremo_izquierda (H a) = a"
| "extremo_izquierda (N f x y) = (extremo_izquierda x)"
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
---------------------------------------------------------------------
- }
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
---------------------------------------------------------------------
- }
lemma inOrdenNoVacio: "inOrden a ≠ []"
apply (induct a) apply simp_all done
theorem ultimoInOrden:
"last (inOrden a) = extremo_derecha a" apply (induct a) apply simp apply (simp add: inOrdenNoVacio) done
theorem "last (inOrden a) = extremo_derecha a" by (induct a) (simp_all add: inOrdenNoVacio)
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 HI1: "?P i" assume HI2: "?P d" show "?P (N x i d)" proof - have "last (inOrden (N x i d)) = last ((inOrden i)@[x]@(inOrden d))" by simp also have "... = last (inOrden d)" by (simp add: inOrdenNoVacio) also have "... = extremo_derecha d" using HI2 by simp also have "... = extremo_derecha (N x i d)" by simp finally show ?thesis by simp qed
qed
thm inOrden.simps(2)
text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
hd (inOrden a) = extremo_izquierda a
---------------------------------------------------------------------
- }
theorem "hd (inOrden a) = extremo_izquierda a"
apply (induct a) apply simp apply (simp add: inOrdenNoVacio) done
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a") proof (induct a)
fix x show "?P (H x)" by simp
next
fix x i d assume HI1: "?P i" assume HI2: "?P d" show "?P (N x i d)" proof - 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 HI1 by simp also have "... = extremo_izquierda (N x i d)" by simp finally show ?thesis by simp qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
hd (preOrden a) = last (postOrden a)
---------------------------------------------------------------------
- }
theorem "hd (preOrden a) = last (postOrden a)" by (induct a) simp_all
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 assume HI1: "?P i" assume HI2: "?P d" show "?P (N x i d)" proof - have "hd (preOrden (N x i d)) = hd (x#((preOrden i)@(preOrden d)))" by simp also have "... = 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 ?thesis by simp qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
- }
theorem "hd (preOrden a) = raiz a" by (induct a) simp_all
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 assume HI1: "?P i" assume HI2: "?P d" show "?P (N x i d)" proof - have "hd (preOrden (N x i d)) = hd (x#((preOrden i)@(preOrden d)))" by simp also have "... = x" by simp also have "... = raiz (N x i d)" by simp finally show ?thesis by simp qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
- }
theorem "hd (inOrden a) = raiz a" quickcheck oops
text {*
Quickcheck found a counterexample: a = N a1 (H a2) (H a1) Evaluated terms: hd (inOrden a) = a2 raiz a = a1
- }
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
- }
lemma "last (postOrden a) = raiz a" by (induct a) simp_all
lemma "last (postOrden a) = raiz a" (is "?P a") proof (induct a)
fix x show "?P (H x)" by simp
next
fix x i d assume HI1: "?P i" assume HI2: "?P d" show "?P (N x i d)" proof - have "last (postOrden (N x i d)) = last ((postOrden i)@(postOrden d)@[x])" by simp also have "... = last [x]" by simp also have "... = x" by simp also have "... = raiz (N x i d)" by simp finally show ?thesis by simp qed
qed
end
</isabelle>