Rel 13 (sol)

chapter ‹R13: Recorridos de árboles›

theory R13_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)))
     = [a,d,c,f,h,g,e] 
  ---------------------------------------------------------------------›

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


― ‹La demostración en lenguaje natural es
Por inducción en la estructura de a, hay que probar:

+ Caso base: a es una hoja, es decir, a = H x
   En este caso,
      preOrden (espejo (H x))
   =  preOrden (H x)               (def. de espejo)
   =  [x]                          (def. de preOrden)
   Por otra parte,
      rev (postOrden (H x))
   =  rev [x]                      (def. de postOrden)
   =  [] @ [x]                     (def. de rev)
   =  [x]                          (def. de append)

   Por tanto,  preOrden (espejo (H x)) = rev (postOrden (H x))

+ Paso inductivo: a = (N x i d) y se verifica la hipótesis de 
  para los árboles i y d. Es decir,
  H1:  preOrden (espejo i) = rev (postOrden i)
  H2:  preOrden (espejo d) = rev (postOrden d)

  Hay que probar:  preOrden (espejo a) = rev (postOrden a)

  En efecto,
    preOrden (espejo (N x i d)) 
  = preOrden (N x (espejo d) (espejo i))             (def. espejo)
  = x # (preOrden (espejo d) @ preOrden (espejo i))  (def. preOrden)
  = x # (rev (postOrden d) @ rev (postOrden i))      (por H1 y H2)
  = x # rev ((postOrden i) @ (postOrden d))          (prop. de rev y append)
  = rev ((postOrden i) @ (postOrden d) @ [x])        (prop. de rev y append)
  = rev (postOrden (N x i d))                        (def. postOrden)

  Por tanto,  preOrden (espejo a) = rev (postOrden a)
›


― ‹La demostración automática es›
lemma  "preOrden (espejo a) = rev (postOrden a)"
  by (induct a) auto

― ‹La demostración estructurada es›
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 "… = x # (rev (postOrden d) @ rev (postOrden i))" 
      using HI1 HI2 by simp 
    also have "… = x # rev (postOrden i @ postOrden d)" by simp
    also have "… = rev ((postOrden i) @ (postOrden d) @ [x])" by simp
    also have "… = rev (postOrden (N x i d))" by simp
    finally show ?thesis .
  qed
qed

― ‹La demostración declarativa detallada es›
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix x :: 'a
  have "preOrden (espejo (H x)) = preOrden (H x)"
    by (simp only: espejo.simps(1))
  also have "… = [x]"
    by (simp only: preOrden.simps(1))
  also have "… = rev [x]"
    by (simp only: rev.simps
                   append.simps(1))
  also have "… = rev (postOrden (H x))"
    by (simp only: postOrden.simps(1))
  finally show "preOrden (espejo (H x)) = rev (postOrden (H x))" 
    by this
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 only: espejo.simps(2))
    also have "… = x # (preOrden (espejo d) @ preOrden (espejo i))" 
      by (simp only: preOrden.simps(2))
    also have "… = x # (rev (postOrden d) @ rev (postOrden i))" 
      by (simp only: HI1 HI2) 
    also have "… = x # rev (postOrden i @ postOrden d)" 
      by (simp only: rev_append)
    also have "… = rev ((postOrden i) @ (postOrden d) @ [x])"
      by (simp only: rev_append append.simps rev.simps)
    also have "… = rev (postOrden (N x i d))" 
      by (simp only: postOrden.simps(2))
    finally show ?thesis 
      by this
  qed
qed

― ‹La demostración aplicativa detallada es›
lemma  "preOrden (espejo a) = rev (postOrden a)" 
  apply (induct a)
   apply (simp only: espejo.simps(1)
                     postOrden.simps(1)
                     preOrden.simps(1)
                     rev.simps)
   apply (simp only: append.simps(1))
   apply (simp only: espejo.simps(2)
                     postOrden.simps(2)
                     preOrden.simps(2))
  apply  (simp only: rev_append 
                     append.simps 
                     rev.simps)
  done    

text ‹------------------------------------------------------------------ 
  Ejercicio 7. Demostrar que
     postOrden (espejo a) = rev (preOrden a)
  ---------------------------------------------------------------------›

― ‹La demostración automática es›
lemma "postOrden (espejo a) = rev (preOrden a)"
  by (induct a) auto

― ‹La demostración estructurada es›
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) @ [x]" 
       using HI1 HI2 by simp
    also have "… = rev (preOrden i @ preOrden d) @ [x]" by simp
    also have "… = rev ([x] @ preOrden i @ preOrden d)" by simp
    also have "… = rev (preOrden (N x i d))" by simp
    finally show ?thesis .
  qed
qed


(* Auxiliar *)
lemma rev1: "rev [x] = [x]"
proof-
  have "rev [x] = (rev []) @ [x]" by (simp only:rev.simps)
  also have "… = [] @ [x]" by (simp only: rev.simps)
  also have "… = [x]" by (simp only: append_Nil)
  finally show "rev [x] = [x]" by this
qed

― ‹La demostración declarativa detallada es›
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by (simp only: espejo.simps(1)
                                 postOrden.simps(1)
                                 preOrden.simps(1)
                                 rev.simps
                                 append.simps(1))
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 only:espejo.simps(2))
        also have "… = postOrden (espejo d) @ postOrden (espejo i) @ [x]" 
            by (simp only: postOrden.simps(2))
    also have "… = rev (preOrden d) @ rev (preOrden i) @ [x]" 
      by (simp only: HI1 HI2) 
    also have "… = rev (preOrden i @ preOrden d) @ [x]" 
      by (simp only: rev_append append_assoc)
    also have "… = rev (preOrden i @ preOrden d) @ rev [x]" 
      by (simp only: rev1)
      also have "… = rev ([x] @ preOrden i @ preOrden d)" 
       by (simp only: rev_append)
      also have "… = rev (preOrden (N x i d))" 
        by (simp only: append.simps preOrden.simps(2))
    finally show ?thesis by this
  qed
qed

― ‹La demostración aplicativa detallada es›
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
  apply (induct a)
  apply (simp only: espejo.simps(1)
                     postOrden.simps(1)
                     preOrden.simps(1)
                     rev.simps)
   apply (simp only: append.simps(1))
     apply (simp only: espejo.simps(2)
                     postOrden.simps(2)
                     preOrden.simps(2))
  apply  (simp only: rev_append 
                     append.simps 
                     rev.simps)
  apply (simp only: append.assoc)
  done
  

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar que
     inOrden (espejo a) = rev (inOrden a)
  --------------------------------------------------------------------- 
›

― ‹La demostración automática es›
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) auto

― ‹La demostración estructurada es›
theorem "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) @ [x] @ rev (inOrden i)" 
       using HI1 HI2 by simp
    also have "… = rev (inOrden i @ [x] @ inOrden d)" by simp
    also have "… = rev (inOrden (N x i d))" by simp
    finally show ?thesis .
  qed
qed

― ‹La demostración declarativa detallada es›
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by (simp only: espejo.simps(1)
                     inOrden.simps(1)
                     rev.simps
                     append_Nil)
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 only: espejo.simps(2))
    also have "… = inOrden (espejo d) @ [x] @ inOrden (espejo i)" 
      by (simp only: inOrden.simps(2))
    also have "… = rev (inOrden d) @ [x] @ rev (inOrden i)" 
      by (simp only: HI1 HI2)
    also have "… = rev (inOrden i @ [x] @ inOrden d)" 
      by (simp only: rev1 rev_append append_assoc)
    also have "… = rev (inOrden (N x i d))" 
      by (simp only: inOrden.simps(2))
    finally show ?thesis by this
  qed
qed

― ‹La demostración aplicativa detallada es›
theorem "inOrden (espejo a) = rev (inOrden a)"
  apply (induct a)
  apply (simp only: espejo.simps(1)
                     inOrden.simps(1)
                     rev.simps)
   apply (simp only: append_Nil)
   apply (simp only: espejo.simps(2)
                     inOrden.simps(2)
                     rev.simps)
  apply (simp only: rev_append 
                    append.assoc 
                    rev1)
  done

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
  --------------------------------------------------------------------- 
›

― ‹La demostración automática, basada en un lema, es›
lemma inOrdenNoVacio: "inOrden a ≠ []"
by (induct a) auto

theorem "last (inOrden a) = extremo_derecha a"
by (induct a) (auto simp add: inOrdenNoVacio)

― ‹La demostración estructurada es›
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 HI: "?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 HI by simp
    also have "… =  extremo_derecha (N x i d)" by simp
    finally show ?thesis .
  qed
qed


― ‹La demostración declarativa detallada es›
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by (simp only: inOrden.simps(1)
                    extremo_derecha.simps(1)
                    last.simps
                    if_P)
next
  fix x i d
  assume HI: "?P d"
  show "?P (N x i d)"
  proof -  
    have "last (inOrden (N x i d)) = 
          last (inOrden i @ [x] @ inOrden d)" 
      by (simp only: inOrden.simps)
    also have "… = last (inOrden d)" 
      by (simp add:inOrdenNoVacio)
    also have "… = extremo_derecha d" using HI by this
    also have "… =  extremo_derecha (N x i d)" 
      by (simp only: extremo_derecha.simps(2))
    finally show ?thesis .
  qed
qed


― ‹La demostración aplicativa detallada es›
theorem "last (inOrden a) = extremo_derecha a"
  apply (induct a)
  apply (simp only: inOrden.simps(1)
                    extremo_derecha.simps(1)
                    last.simps
                    if_P)
  apply (simp only: inOrden.simps(2)
                    extremo_derecha.simps(2))
  apply (simp only: last_append)
  apply (split if_split)
  apply (rule conjI)
   apply (rule impI)
   apply (simp only:append_Cons 
                    append_Nil) 
   apply (simp only: list.simps)
  apply (rule impI)
   apply (split if_split)
   apply (rule conjI)
   apply (rule impI)
   apply (simp only: inOrdenNoVacio)
  apply (rule impI)
  apply (simp only: refl)
  done


text ‹
  --------------------------------------------------------------------- 
  Ejercicio 13. Demostrar o refutar
     hd (inOrden a) = extremo_izquierda a
  --------------------------------------------------------------------- 
›

― ‹La demostración automática es›
theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a) (auto simp add: inOrdenNoVacio)

― ‹La demostración estructurada es›
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 HI: "?P i"
  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 HI by simp
    also have "… = extremo_izquierda (N x i d)" by simp
    finally show ?thesis .
  qed
qed



― ‹La demostración declarativa detallada es›
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by (simp only: extremo_izquierda.simps(1)
                      inOrden.simps(1)
                      list.sel)
next
  fix x i d
  assume HI: "?P i"
  show "?P (N x i d)"
  proof - 
    have "hd (inOrden (N x i d)) = 
          hd (inOrden i @ [x] @ inOrden d)" 
      by (simp only: inOrden.simps(2))
    also have "… = hd (inOrden i)" 
      by (simp add: inOrdenNoVacio)
    also have "… = extremo_izquierda i" using HI by this
    also have "… = extremo_izquierda (N x i d)" 
      by (simp only: extremo_izquierda.simps(2))
    finally show ?thesis by this
  qed
qed

― ‹La demostración aplicativa detallada es›
theorem "hd (inOrden a) = extremo_izquierda a" 
  apply (induct a)
  apply (simp only: extremo_izquierda.simps(1)
                    inOrden.simps(1))
   apply (rule list.sel)
   apply (simp only: extremo_izquierda.simps(2)
                    inOrden.simps(2))
  apply (simp only: hd_append)
  apply (split if_split)
  apply (rule conjI)
   apply (rule impI)
   apply (simp only: inOrdenNoVacio)
  apply (rule impI)
  apply (simp only:refl)
  done

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 14. Demostrar o refutar
     hd (preOrden a) = last (postOrden a)
  --------------------------------------------------------------------- 
›

― ‹La demostración automática es›
theorem "hd (preOrden a) = last (postOrden a)"
by (cases a) auto


― ‹La demostración estructurada es›
theorem "hd (preOrden a) = last (postOrden a)"(is "?P a")
proof (cases a)
  fix x
  assume "a = H x"
  then show "?P a" by simp 
next
  fix x i d
  assume H: "a = N x i d"
  show "?P a"
  proof - 
    have "hd (preOrden a) = hd (preOrden (N x i d))" using H by simp
    also have "… = 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
    also have "… = last (postOrden a)" using H by simp
    finally show ?thesis .
  qed
qed


― ‹La demostración declarativa detallada es›
theorem "hd (preOrden a) = last (postOrden a)"(is "?P a")
proof (cases a)
  fix x
  assume "a = H x"
  then show "?P a" by (simp only: preOrden.simps(1)
                                  postOrden.simps(1)
                                  last.simps
                                  if_P
                                  list.sel)
next
  fix x i d
  assume H: "a = N x i d"
  show "?P a"
  proof - 
    have "hd (preOrden a) = hd (preOrden (N x i d))" using H 
        by (rule arg_cong)
      also have "… = hd (x # (preOrden i @ preOrden d))" 
        by (simp only: preOrden.simps(2))
      also have "… = x" by (simp only: list.sel)
      also have "… = last ((postOrden i @ postOrden d) @ [x])"
        by (simp only: last_snoc)
    also have "… = last (postOrden i @ postOrden d @ [x])"
      by (simp only: append_assoc)
    also have "… = last (postOrden (N x i d))" 
      by (simp only: postOrden.simps(2))
    also have "… = last (postOrden a)" by (simp only:H)
    finally show ?thesis by this
  qed
qed

― ‹La demostración aplicativa detallada es›
theorem "hd (preOrden a) = last (postOrden a)"(is "?P a")
  apply (cases a)
  apply (simp only: preOrden.simps(1)
                    postOrden.simps(1)
                    last.simps
                    if_P)
   apply (rule list.sel)
    apply (simp only: preOrden.simps(2)
                    postOrden.simps(2))
  apply (simp only: append_assoc[THEN sym])
  apply (simp only: last_snoc)
  apply (simp only: list.sel)
  done
                       
text ‹
  --------------------------------------------------------------------- 
  Ejercicio 15. Demostrar o refutar
     hd (preOrden a) = raiz a
  --------------------------------------------------------------------- 
›

― ‹La demostración automática es›
theorem "hd (preOrden a) = raiz a"
by (cases a) auto

― ‹La demostración estructurada es›
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (cases a)
  fix x
  assume "a = H x"
  then show "?P a" by simp
next
  fix x i d
  assume H: "a = N x i d"
  show "?P a"
  proof -
    have "hd (preOrden a) = hd (preOrden (N x i d))" using H by simp
    also have "… = hd (x#(preOrden i @ preOrden d))" by simp
    also have "… = x" by simp
    also have "… = raiz (N x i d)" by simp
    also have "… = raiz a" using H by simp
    finally show ?thesis .
  qed
qed

― ‹La demostración declarativa detallada es›
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (cases a)
  fix x
  assume "a = H x"
  then show "?P a" by  (simp only: preOrden.simps(1)
                                   raiz.simps(1)
                                    list.sel)
next
  fix x i d
  assume H: "a = N x i d"
  then show "?P a" by  (simp only: preOrden.simps(2)
                                   raiz.simps(2)
                                   list.sel)
qed

― ‹La demostración aplicativa detallada es›
theorem "hd (preOrden a) = raiz a"
  apply (cases a)
  apply (simp only: preOrden.simps(1)
                    raiz.simps(1)
                    list.sel)
   apply (simp only: preOrden.simps(2)
                    raiz.simps(2)
                    list.sel)
  done

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
  --------------------------------------------------------------------- 
›

― ‹La demostración automática es›
theorem "last (postOrden a) = raiz a"
by (cases a) auto

― ‹La demostración estructurada es›
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (cases a)
  fix x
  assume "a = H x"
  then show "?P a" by simp
next
  fix x i d
  assume H: "a = N x i d"
  show "?P a"
  proof -
    have "last (postOrden a) = last (postOrden (N x i d))" using H by simp
    also have "… = last (postOrden i @ postOrden d @ [x])" by simp
    also have "… = x" by simp
    also have "… = raiz a" using H by simp
    finally show ?thesis .
  qed
qed

― ‹La demostración declarativa detallada es›
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (cases a)
  fix x
  assume "a = H x"
  then show "?P a" by (simp only: postOrden.simps(1)
                                  raiz.simps(1)
                                  last.simps  
                                  if_P)
next
  fix x i d
  assume H: "a = N x i d"
  show "?P a"
  proof -
    have "last (postOrden a) = last (postOrden (N x i d))" 
      using H by (rule arg_cong)
    also have "… = last (postOrden i @ postOrden d @ [x])" 
      by (simp only: postOrden.simps(2))
    also have "… = last ((postOrden i @ postOrden d) @ [x])" 
      by (simp only: append_assoc)
    also have "… = x" by (simp only: last_snoc)
    also have "… = raiz a" using H by (simp only: raiz.simps(2))
    finally show ?thesis by this
  qed
qed


― ‹La demostración aplicativa detallada es›
theorem "last (postOrden a) = raiz a" 
  apply (cases a)
  apply (simp only: postOrden.simps(1)
                    raiz.simps(1))
   apply (simp only: last.simps  
                     if_P)
   apply (simp only: postOrden.simps(2)
                    raiz.simps(2))
  apply (simp only: append_assoc[THEN sym])
  apply (simp only: last_snoc)
  done
  

end