Relación 5

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 *)
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 *)
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 *)
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 *)
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 *)
lemma  "preOrden (espejo a) = rev (postOrden a)"
  by (induct a) auto

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

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar que
     postOrden (espejo a) = rev (preOrden a)
  --------------------------------------------------------------------- 
*}

(* luicedval *)
lemma "postOrden (espejo a) = rev (preOrden a)"
  by (induct a) auto

(*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 *)
theorem "inOrden (espejo a) = rev (inOrden a)"
  by (induct a) auto

(*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 *)
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 *)
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 *)
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

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


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

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 15. Demostrar o refutar
     hd (preOrden a) = raiz a
  --------------------------------------------------------------------- 
*}

 (*anddonram*)
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
 

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

 (*anddonram*)
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

end