Relación 7

header {* R7: Recorridos de árboles *}

theory R7_2
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] 
  --------------------------------------------------------------------- 
*}

-- "diecabmen1 maresccas4 domlloriv pabflomar juaruipav jaisalmen zoiruicha"

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]" 

-- "irealetei marescpla"
fun preOrden2 :: "'a arbol ⇒ 'a list" where
  "preOrden2 (H a) = [a]"
 |"preOrden2 (N dato a1 a2) = dato#(preOrden2 a1 @ preOrden2 a2)"

-- "pabflomar: ¿Realmente se nota el usar el # en lugar de la @?"

value "preOrden2 (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]
  --------------------------------------------------------------------- 
*}

-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav jaisalmen zoiruicha"

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]"



--"marescpla"
fun inOrden2 :: "'a arbol ⇒ 'a list" where
  "inOrden2 (H a)=[a]"|
  "inOrden2 (N a x y) = inOrden2 x @ a # inOrden2 y"
 
value "inOrden2 (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))
  --------------------------------------------------------------------- 
*}

-- "diecabmen1 maresccas4 domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"

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

-- "irealetei: Es igual que la anterior pero  los paréntesis no hacen falta"
fun espejo2 :: "'a arbol ⇒ 'a arbol" where
  "espejo2 (H dato) = (H dato)"
| "espejo2 (N dato a1 a2) = N dato (espejo2 a2) (espejo2 a1)"

value "espejo2 (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)
  --------------------------------------------------------------------- 
*}
 
-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4 pabflomar"

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

-- "irealetei"
lemma  "preOrden (espejo a) = rev (postOrden a)"
proof (induct a)
  fix a::"'a"
  show "preOrden (espejo (H a)) = rev (postOrden (H a))" by simp
next
  fix data::"'a"
  fix a1::"'a arbol"
  assume HI1:" preOrden (espejo a1) = rev (postOrden a1)"
  fix a2::"'a arbol"
  assume HI2:" preOrden (espejo a2) = rev (postOrden a2)"
  show "preOrden (espejo (N data a1 a2)) = rev (postOrden (N data a1 a2))"
  proof -
    have "preOrden (espejo (N data a1 a2))=preOrden (N data (espejo a2) (espejo a1))" by simp
    also have "... = data # (preOrden(espejo a2) @ preOrden(espejo a1))" by simp
    also have "... = data # (rev (postOrden a2) @ rev (postOrden a1))" using HI1 HI2 by simp
    also have "... = data # (rev (postOrden a1 @ postOrden a2))" by simp
    also have "... = rev (postOrden a1 @ postOrden a2 @ [data])" by simp
    also have "... = rev (postOrden (N data a1 a2))" by simp
    finally show ?thesis by simp
  qed
qed

--"marescpla"
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix a:: "'a arbol"
  fix x:: "'a"
 show "?P (H x)" by simp
  next
  fix a:: "'a"
  fix x:: "'a arbol"
  fix y :: "'a arbol"
  fix t :: "'a arbol"
 assume HI : "?P x"
 assume HII : "?P y"
  have "preOrden (espejo (N a x y))= preOrden (N a (espejo y) (espejo x))" by (simp only: espejo.simps(2))
  also have "... = a # (preOrden (espejo y) @ preOrden (espejo x))" by (simp only: preOrden2.simps(2))
  also have "... = a # (rev (postOrden y) @ rev (postOrden x))" using HI HII by simp
  also have "... = rev (postOrden x @ postOrden y @ [a])" by simp
  finally show "preOrden (espejo (N a x y))= rev (postOrden (N a x y))" by simp
 qed

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

-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4"

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

--"irealetei"
lemma  "postOrden (espejo a) = rev (preOrden a)"
proof (induct a)
  fix a::"'a"
  show "postOrden (espejo (H a)) = rev (preOrden (H a))" by simp
next
  fix data::"'a"
  fix a1::"'a arbol"
  assume HI1:" postOrden (espejo a1) = rev (preOrden a1)"
  fix a2::"'a arbol"
  assume HI2:" postOrden (espejo a2) = rev (preOrden a2)"
  show "postOrden (espejo (N data a1 a2)) = rev (preOrden (N data a1 a2))"
  proof -
    have "postOrden (espejo (N data a1 a2))=postOrden (N data (espejo a2) (espejo a1))" by simp
    also have "... = postOrden(espejo a2) @ postOrden(espejo a1) @ [data]" by simp
    also have "... = rev (preOrden a2) @ rev (preOrden a1) @ [data]" using HI1 HI2 by simp
    also have "... = rev (preOrden a1 @ preOrden a2)@[data]" by simp
    also have "... = rev (preOrden a1 @ preOrden a2)@ rev ([data])" by simp
    also have "... = rev ([data] @ preOrden a1 @ preOrden a2)" by simp
    also have "... = rev (preOrden (N data a1 a2))" by simp
    finally show ?thesis by simp
  qed
qed

--"marescpla"
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
  fix a:: "'a arbol"
  fix x:: "'a"
 show "?P (H x)" by simp
  next
  fix a:: "'a"
  fix x:: "'a arbol"
  fix y :: "'a arbol"
  fix t :: "'a arbol"
 assume HI : "?P x"
 assume HII : "?P y"
  have "postOrden (espejo (N a x y))= postOrden (N a (espejo y) (espejo x))" by (simp only: espejo.simps(2))
  also have "... = (postOrden (espejo y) @ postOrden (espejo x)) @ [a]" by (simp only: postOrden.simps(2))
  also have "... = (rev (preOrden y) @ rev (preOrden x)) @ [a]" using HI HII by simp
  also have "... = rev (a # preOrden x @ preOrden y)" by simp
  finally show "postOrden (espejo (N a x y))= rev (preOrden (N a x y))" by simp
 qed
 

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

-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav jaisalmen zoiruicha"

theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) auto

-- "diecabmen1 maresccas4"

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) @ rev [a1] @ rev (inOrden a2)" using HI1 HI2 by simp
    also have "… = rev (inOrden a2 @ [a1] @ inOrden a3)" by simp
    finally show ?thesis by simp
  qed
qed

-- "irealetei"
lemma  "inOrden (espejo a) = rev (inOrden a)"
proof (induct a)
  fix a::"'a"
  show "inOrden (espejo (H a)) = rev (inOrden (H a))" by simp
next
  fix data::"'a"
  fix a1::"'a arbol"
  assume HI1:" inOrden (espejo a1) = rev (inOrden a1)"
  fix a2::"'a arbol"
  assume HI2:" inOrden (espejo a2) = rev (inOrden a2)"
  show "inOrden (espejo (N data a1 a2)) = rev (inOrden (N data a1 a2))"
  proof -
    have "inOrden (espejo (N data a1 a2))=inOrden (N data (espejo a2) (espejo a1))" by simp
    also have "... = inOrden(espejo a2) @ [data] @ inOrden(espejo a1)" by simp
    also have "... = rev (inOrden a2)@ [data] @ rev (inOrden a1)" using HI1 HI2 by simp
    also have "... = rev (inOrden a2)@ rev([data]) @ rev (inOrden a1)" by simp
    also have "... = rev ([data] @ (inOrden a2)) @ rev(inOrden a1)" by simp
    also have "... = rev ( inOrden a1 @ [data] @ inOrden a2)" by simp
    also have "... = rev (inOrden (N data a1 a2))" by simp
    finally show ?thesis by simp
  qed
qed

--"marescpla"
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix a:: "'a arbol"
  fix x:: "'a"
 show "?P (H x)" by simp
  next
  fix a:: "'a"
  fix x:: "'a arbol"
  fix y :: "'a arbol"
  fix t :: "'a arbol"
 assume HI : "?P x"
 assume HII : "?P y"
  have "inOrden (espejo (N a x y))= inOrden (N a (espejo y) (espejo x))" by (simp only: espejo.simps(2))
  also have "... = (inOrden (espejo y) @ a #  inOrden (espejo x))" by (simp only: inOrden.simps(2))
  also have "... = (rev (inOrden y) @ a # rev (inOrden x))" using HI HII by simp
  also have "... = rev (inOrden x @ a # inOrden y)" by simp
  finally show "inOrden (espejo (N a x y))= rev (inOrden (N a x y))" 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
  --------------------------------------------------------------------- 
*}

-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4 domlloriv juaruipav"

lemma inOrdenNN: "inOrden a ≠ []"
by (induct a) auto

theorem "last (inOrden a) = extremo_derecha 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 (inOrden (N a1 a2 a3)) = last (a1 # inOrden a3)" by simp
    also have "… = last (inOrden a3)"  by (simp add: inOrdenNN)
    also have "… = extremo_derecha a3" using HI2 by simp
    finally show ?thesis by simp
  qed
qed

--"irealetei jaisalmen zoiruicha"
lemma inOrdenNoPuedeSerVacio: "inOrden a ≠ []"
by (induct a) auto

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

theorem "last (inOrden a) = extremo_derecha a"
proof (induct a)
  fix data::"'a"
  show "last (inOrden (H data)) = extremo_derecha (H data)" by simp
next 
  fix data::"'a" 
  fix a2::"'a arbol"
  fix a1
  assume HI:" last (inOrden a2) = extremo_derecha a2"
  show "last (inOrden (N data a1 a2)) = extremo_derecha (N data a1 a2)"
  proof -
    have "last (inOrden (N data a1 a2))= last ((inOrden a1)@[data] @ (inOrden a2))" by simp
    also have "...= last (inOrden a2)" by (simp add:inOrdenNoPuedeSerVacio)
    also have "...=extremo_derecha a2" using HI by simp
    also have "...=extremo_derecha (N data a1 a2)" by simp
    finally show ?thesis by simp
  qed
qed


--"marescpla"

lemma inOrdenDistintoVacio:
 "inOrden a ≠ []" (is "?P a")
proof (induct a)
  fix a :: "'a arbol"
  fix x :: "'a"
 show "?P (H x)" by simp
  next
  fix a1:: "'a"
  fix a2:: "'a arbol"
  fix a3:: "'a arbol"
 assume HI: "?P a2"  
    have "inOrden (N a1 a2 a3)= inOrden a2 @ a1 # inOrden a3" by (simp only: inOrden.simps(2))
 also have "… ≠ []" using HI by simp
 finally show "inOrden (N a1 a2 a3) ≠ []" by simp
 qed
 
    
 
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induction a)
  fix x :: "'a"
    show "?P (H x)" by simp
  next
  fix a :: "'a"
  fix x :: "'a arbol"
  fix y :: "'a arbol"
  assume HII : "?P y"
    have "last (inOrden (N a x y)) = last (inOrden x @ a # inOrden y)" by (simp only: inOrden.simps(2))
    also have "... = last (a # inOrden y)" by (simp add: inOrdenDistintoVacio)
    also have "... = last (inOrden y)" by (simp add: inOrdenDistintoVacio)
    also have "... = extremo_derecha y" using HII by simp
  finally show "last (inOrden (N a x y)) = extremo_derecha (N a x y)" by simp
qed

 



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

-- "diecabmen1 maresccas4 irealetei domlloriv juaruipav"

theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a) (auto simp add: inOrdenNN)

-- "diecabmen1 maresccas4 "

theorem "hd (inOrden a) = extremo_izquierda 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 (inOrden (N a1 a2 a3)) = hd  (inOrden a2 @ a1 # inOrden a3)" by simp
    also have "… = hd (inOrden a2)"  by (simp add: inOrdenNN)
    also have "… = extremo_izquierda a2" using HI1 by simp
    finally show ?thesis by simp
  qed
qed

-- "irealetei"
theorem "hd (inOrden a) = extremo_izquierda a"
proof (induct a)
  fix data::"'a"
  show "hd (inOrden (H data)) = extremo_izquierda (H data)" by simp
next 
  fix data::"'a" 
  fix a1::"'a arbol"
  fix a2
  assume HI:" hd (inOrden a1) = extremo_izquierda a1"
  show "hd (inOrden (N data a1 a2)) = extremo_izquierda (N data a1 a2)"
  proof -
    have "hd (inOrden (N data a1 a2))= hd ((inOrden a1)@[data] @ (inOrden a2))" by simp
    also have "...= hd (inOrden a1)" by (simp add:inOrdenNoPuedeSerVacio)
    also have "...=extremo_izquierda a1" using HI by simp
    also have "...=extremo_izquierda (N data a1 a2)" by simp
    finally show ?thesis by simp
  qed
qed


--"marescpla"

theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
  fix a:: "'a arbol"
  fix x:: "'a"
    show "?P (H x)" by simp
    next
  fix a :: "'a"
  fix x :: "'a arbol"
  fix y :: "'a arbol"
  assume HI: "?P x"
    have "hd (inOrden (N a x y))= hd (inOrden x @ a # inOrden y)" by (simp only: inOrden.simps(2))
    also have "...=hd (inOrden x)" by ( simp add: inOrdenDistintoVacio)
    also have "...= extremo_izquierda x" using HI by simp
    finally show "hd (inOrden (N a x y)) = extremo_izquierda (N a x y)" by simp
  qed

-- "jaisalmen zoiruicha"
theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a) (auto simp add: inOrdenNoPuedeSerVacio

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

-- "diecabmen1 maresccas4 domlloriv juaruipav jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4"

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)" by simp
    also have "… = a1" by simp
    finally show ?thesis by simp
  qed
qed

-- "irealetei: Se puede hacer con cases"
theorem "hd (preOrden a) = last (postOrden a)"
by (cases a) auto

theorem "hd (preOrden a) = last (postOrden a)"
proof (cases a)
  fix data
  assume "a = H data"
  then show "hd (preOrden a) = last (postOrden a)" by simp
next
  fix data::"'a"
  fix a1::"'a arbol"
  fix a2::"'a arbol"
  assume A:"a = N data a1 a2"
  then
    have "hd (preOrden (N data a1 a2)) = hd (data #(preOrden a1 @ preOrden a2))" by simp
    also have "... = data" by simp
    also have "... = last (postOrden a1 @ postOrden a2 @ [data])" by simp
    also have "... = last (postOrden (N data a1 a1))" by simp
    finally show ?thesis using A by simp
qed


--"marescpla"

theorem T1: "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (cases a)
  fix a:: "'a arbol"
  fix x:: "'a"
  assume H1 : "a = (H x)"
  then have "hd (preOrden a)= hd (preOrden (H x))" by simp
  also have "... = last (postOrden (H x))" by simp
  finally show "?P a" using H1 by simp
    next
  fix t :: "'a"
  fix x :: "'a arbol"
  fix y :: "'a arbol"
  assume H2: "a = (N t x y)"
    then have "hd (preOrden a)= hd (preOrden (N t x y))" by simp
    have "hd (preOrden (N t x y))= hd (t # preOrden x @ preOrden y)" by (simp only: preOrden2.simps(2))
    also have "...= t " by (simp only: hd.simps(1))
    finally show "hd (preOrden a)= last (postOrden a)" using H2 by simp
qed
 

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

-- "diecabmen1 maresccas4 domlloriv juaruipav zoiruicha jaisalmen"

theorem "hd (preOrden a) = raiz a"
by (induct a) auto

-- "diecabmen1 maresccas4"

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)" by simp
    also have "… = a1" by simp
    finally show ?thesis by simp
  qed
qed

-- "irealetei"

theorem "hd (preOrden a) = raiz a"
by (cases a) auto

theorem "hd (preOrden a) = raiz a"
proof (cases a)
  fix data
  assume "a = H data"
  then show "hd (preOrden a) = raiz a" by simp
next
  fix data::"'a"
  fix a1::"'a arbol"
  fix a2::"'a arbol"
  assume A:"a = N data a1 a2"
  then
    have "hd (preOrden (N data a1 a2)) = hd (data #(preOrden a1 @ preOrden a2))" by simp
    also have "... = data" by simp
    also have "... = raiz (N data a1 a2)" by simp
    finally show ?thesis using A by simp
qed

--"marescpla"

theorem T2: "hd (preOrden a) = raiz a" (is "?P a")
proof (cases a)
  fix a ::"'a arbol"
  fix x::"'a"
assume " a = (H x)"
  then show "?P a" by simp
next
  fix a ::"'a arbol"
  fix t::"'a"
  fix x ::"'a arbol"
  fix y ::"'a arbol"
assume H: " a = (N t x y)"
  then have "hd (preOrden a) = hd (t # preOrden x @ preOrden y)" by simp
  also have "...= t" by simp
  finally show "?P a" using H by simp
qed


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

-- "diecabmen1 maresccas4 irealetei domlloriv juaruipav marescpla jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4 domlloriv juaruipav jaisalmen zoiruicha"

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

-- "diecabmen1 maresccas4"

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

--"irealetei"

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

theorem "last (postOrden a) = raiz a"
proof (cases a)
 fix data
  assume "a = H data"
  then show "last (postOrden a) = raiz a" by simp
next
  fix data::"'a"
  fix a1::"'a arbol"
  fix a2::"'a arbol"
  assume A:"a = N data a1 a2"
  then
    have "last (postOrden (N data a1 a2)) = last (preOrden a1 @ preOrden a2 @ [data])" by simp
    also have "... = data" by simp
    also have "... = raiz (N data a1 a2)" by simp
    finally show ?thesis using A by simp
qed

--"marescpla"

theorem "last (postOrden a) = raiz a" (is "?P a")
proof-
have "last (postOrden a) = hd (preOrden a)" by (simp add:T1)
also have "... = raiz a" by (simp add: T2)
finally show "?P a" by simp
qed

end