Sol 12

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

(* 1ª demostración: sin patrones *) 
lemma "preOrden (espejo a) = rev (postOrden a)" 
proof (induct a) 
  fix x :: 'a
  show "preOrden (espejo (H x)) = rev (postOrden (H x))" by simp
next
  fix x :: 'a and i d :: "'a arbol"
  assume HI1: "preOrden (espejo i) = rev (postOrden i)"
  assume HI2: "preOrden (espejo d) = rev (postOrden d)"
  show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))"
  proof -
    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 "… = rev [x] @ rev (postOrden d) @ rev (postOrden i)" 
      using HI1 HI2 by simp 
    also have "… = rev ((postOrden i) @ (postOrden d) @ [x])" by simp
    finally show ?thesis by simp
  qed
qed

(* 2ª demostración: con patrones *) 
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 HI1: "?P i"
  assume HI2: "?P d"
  show "?P (N x i d)"
  proof -
    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 "… = rev [x] @ rev (postOrden d) @ rev (postOrden i)" 
      using HI1 HI2 by simp 
    also have "… = rev ((postOrden i) @ (postOrden d) @ [x])" 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

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