Rel 6

header {* R6: Recorridos de árboles *}

theory R6
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)auto



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) auto



lemma "postOrden (espejo a) = rev (preOrden 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 "postOrden(espejo (N a1 a2 a3)) = postOrden (N a1 (espejo a3) (espejo a2))" by simp
  also have "... = (postOrden(espejo a3))@(postOrden(espejo a2)@[a1])" by simp
  also have "... = (rev(preOrden a3))@(rev(preOrden a2))@[a1]" using HI1 HI2 by simp
  also have "... = rev(preOrden (N a1 a2 a3))" by simp
  finally show ?thesis by simp
  qed
qed

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar que
     inOrden (espejo a) = rev (inOrden a)
  --------------------------------------------------------------------- 
*}

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
  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 "inOrden(espejo (N a1 a2 a3)) = inOrden (N a1 (espejo a3) (espejo a2))" by simp
  also have "... = (inOrden(espejo a3))@[a1]@(inOrden(espejo a2))" by simp
  also have "... = (rev(inOrden a3))@[a1]@(rev(inOrden a2))" using HI1 HI2 by simp
  also have "... = rev(inOrden (N a1 a2 a3))" 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 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
  --------------------------------------------------------------------- 
*}

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
  --------------------------------------------------------------------- 
*}

theorem "last (inOrden a) = extremo_derecha a"
oops

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 13. Demostrar o refutar
     hd (inOrden a) = extremo_izquierda a
  --------------------------------------------------------------------- 
*}

theorem "hd (inOrden a) = extremo_izquierda a"
oops

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 14. Demostrar o refutar
     hd (preOrden a) = last (postOrden a)
  --------------------------------------------------------------------- 
*}

theorem "hd (preOrden a) = last (postOrden a)"
by(induct a)auto




theorem "hd (preOrden a) = last (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 "hd(preOrden (N a1 a2 a3)) = hd([a1]@(preOrden a2)@(preOrden a3))" by simp
  also have "... = a1" by simp
  also have "... = last((postOrden a3)@(postOrden a2)@[a1])"by simp
  also have "... = last(postOrden (N a1 a2 a3))" 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)auto



theorem "hd (preOrden a) = raiz 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 "hd(preOrden (N a1 a2 a3)) = hd([a1]@(preOrden a2)@(preOrden a3))" by simp
  also have "... = a1" by simp
  also have "... = raiz(N a1 a2 a3)" 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{* Contraejemplo:
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
  --------------------------------------------------------------------- 
*}

theorem "last (postOrden a) = raiz a"
by(induct a)auto




theorem "last (postOrden a) = raiz 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 "last(postOrden (N a1 a2 a3)) = last((postOrden a2)@(postOrden a3)@[a1])" by simp
  also have "... = a1" by simp
  also have "... = raiz(N a1 a2 a3)" by simp
  finally show ?thesis by simp
  qed
qed


end