Relación 6

chapter {* R6: Recorridos de árboles *}

theory R6_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   3
  se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
  --------------------------------------------------------------------- 
*}

(* ivamenjim marpoldia1 manmorjim1 bowma migtermor wilmorort 
   juacabsou serrodcal pabrodmac ferrenseg rubgonmar paupeddeg 
   crigomgom danrodcha jeamacpov marcarmor13 josgarsan fraortmoy 
   dancorgar fracorjim1 anaprarod antsancab1 *)

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

(* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor 
   wilmorort lucnovdos serrodcal pabrodmac jeamacpov paupeddeg
   marcarmor13 josgarsan dancorgar anaprarod antsancab1 *)

fun preOrden :: "'a arbol ⇒ 'a list" where
  "preOrden (H t)     = [t]"
| "preOrden (N t i d) = [t] @ (preOrden i) @ (preOrden d)"

(* danrodcha crigomgom manmorjim1 bowma juacabsou ferrenseg 
   rubgonmar paupeddeg fracorjim1 *)
fun preOrden1 :: "'a arbol ⇒ 'a list" where
  "preOrden1 (H x)     = [x]"
| "preOrden1 (N x i d) = x # preOrden1 i @ preOrden1 d"

value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))  
      = [e,c,a,d,g,f,h]" 
value "preOrden1 (N e (N c (H a) (H d)) (N g (H f) (H h)))  
      = [e,c,a,d,g,f,h]" 

(* danrodcha *)
lemma "preOrden a = preOrden1 a"
by (induct a) simp_all

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

(* ivamenjim  danrodcha crigomgom marpoldia1 manmorjim1
    pablucoto bowma fraortmoy migtermor wilmorort lucnovdos
    juacabsou serrodcal pabrodmac  ferrenseg jeamacpov 
    rubgonmar paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod antsancab1 *)

fun postOrden :: "'a arbol ⇒ 'a list" where
  "postOrden (H t)     = [t]"
| "postOrden (N t i d) = (postOrden i) @ (postOrden d) @ [t]"

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

(* ivamenjim crigomgom marpoldia1 pablucoto bowma fraortmoy 
   migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac 
   ferrenseg jeamacpov rubgonmar paupeddeg marcarmor13 josgarsan
   dancorgar anaprarod antsancab1 *)
fun inOrden :: "'a arbol ⇒ 'a list" where
  "inOrden (H t)     = [t]"
| "inOrden (N t i d) = (inOrden i) @ [t] @ (inOrden d)"

(* danrodcha manmorjim1 fracorjim1 *)
fun inOrden1 :: "'a arbol ⇒ 'a list" where
  "inOrden1 (H t)     = [t]"
| "inOrden1 (N t i d) = inOrden1 i @ t#inOrden1 d"

value "inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
       = [a,c,d,e,f,g,h]"
value "inOrden1 (N e (N c (H a) (H d)) (N g (H f) (H h)))
       = [a,c,d,e,f,g,h]"

(* manmorjim1 *)
lemma "inOrden t = inOrden1 t"
apply (induct t)
apply auto
done

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

(* ivamenjim danrodcha crigomgom marpoldia1 manmorjim1 
   pablucoto bowma fraortmoy migtermor wilmorort lucnovdos 
   juacabsou serrodcal pabrodmac ferrenseg jeamacpov rubgonmar 
   paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod antsancab1 *)
fun espejo :: "'a arbol ⇒ 'a arbol" where
  "espejo (H t)     = H t"
| "espejo (N t i d) = N t (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)
  --------------------------------------------------------------------- 
*}

(* ivamenjim migtermor wilmorort juacabsou serrodcal dancorgar josgarsan
*) 
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  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 h1 h2 by simp 
  finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" 
    by simp
qed

(* danrodcha paupeddeg anaprarod *)
lemma  "preOrden (espejo a) = rev (postOrden a)"
by (induct a) simp_all


(* danrodcha crigomgom fracorjim1 *)
lemma  "preOrden1 (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 HIi: "?P i"
  assume HId: "?P d"
  have "preOrden1 (espejo (N x i d)) = 
        preOrden1 (N x (espejo d) (espejo i))"
    by (simp only: espejo.simps(2))
  also have "… = x#preOrden1 (espejo d) @ preOrden1 (espejo i)"
    by (simp only: preOrden1.simps(2))
  also have"… = x#rev (postOrden d) @ rev (postOrden i)" 
    using HIi HId by simp
  also have "… = rev (postOrden (N x i d))" by simp
  finally show "?P (N x i d)" by simp
qed

(* danrodcha fraortmoy anaprarod *)
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 HIi: "?P i"
  assume HId: "?P d"
  show "?P (N x i d)" using HIi HId by simp
qed

(* bowma *)
lemma  "preOrden (espejo a) = rev (postOrden a)"
apply (induct a)
apply simp_all
done

(* pablucoto marpoldia1 jeamacpov paupeddeg marcarmor13 anaprarod *)
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 h1: "?P i"
  assume h2: "?P d"
  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 h1 h2 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 "?P (N x i d)" by simp  
qed

(* bowma *)
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?p a")
proof (induct a)
  fix t
  show "?p (H t)" by simp
  (* Aquí si le diga "preOrden (espejo (H t)) = rev (postOrden (H t))",
     isabelle dice: 
  proof (prove)
  goal (1 subgoal):
  1. preOrden (espejo (H t)) = rev (postOrden (H t)) 
  Introduced fixed type variable(s): 'b in "t__" 
  No entiendo porqué *)
next 
  fix t i d
  assume H1: "?p i"
  assume H2: "?p d"
  have "preOrden (espejo (N t i d)) = 
        preOrden (N t (espejo d) (espejo i))" by simp
  also have "... = [t] @ (preOrden (espejo d)) @ (preOrden (espejo i))" 
    by simp
  also have "... = [t] @ rev (postOrden d) @ rev (postOrden i)" 
    using H1 H2 by simp
  finally show "?p (N t i d)" by simp
qed 

(* Comentario sobre tipo inducido. *)

(* fraortmoy lucnovdos pabrodmac*)
lemma  "preOrden (espejo a) = rev (postOrden a)"
by (induct a) auto

(*pabrodmac*)
lemma
  fixes a ::"'b arbol" 
  shows "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?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]@rev(postOrden d)@rev(postOrden i)" 
      using h1 h2 by simp
    also have "… = rev(postOrden (N x i d))" by simp
    finally show ?thesis .
 qed
qed

(* ferrenseg rubgonmar *)
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x l r
  assume H1: "?P l"
  assume H2: "?P r"
  show "?P (N x l r)"
  proof -
    have "preOrden (espejo (N x l r)) = 
          preOrden (N x (espejo r) (espejo l))" by simp
    also have "… = x # (preOrden (espejo r) @ preOrden (espejo l))" by simp
    also have "… = x # (rev (postOrden r) @ rev (postOrden l))" 
       using H1 H2 by simp 
    also have "… = x # rev (postOrden l @ postOrden r)" by simp
    also have "… = rev ((postOrden l) @ (postOrden r) @ [x])" by simp
    also have "… = rev (postOrden (N x l r))" by simp
    finally show ?thesis .
  qed
qed

(* antsancab1 *)
(* Le he puesto el nombre para utilizarlo en la siguiente demostración *)
lemma  pre_es_rev_post: "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x
  fix i assume H1: "?P i"
  fix d assume H2: "?P d"
  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 H1 H2 by simp
  finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" by simp
qed

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

(* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal
   dancorgar josgarsan antsancab1 *) 
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  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 h1 h2 by simp 
  finally show "postOrden (espejo (N x i d)) = rev (preOrden (N x i d))" 
    by simp
    (* "?p (N x i d)" más corto *)
qed

(* danrodcha fraortmoy anaprarod *)
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 HIi: "?P i"
  assume HId: "?P d"
  show "?P (N x i d)" using HIi HId by simp
qed

(* pablucoto marpoldia1 jeamacpov paupeddeg rubgonmar anaprarod *)
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 H1: "?P i"
  assume H2: "?P d"
  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 H1 H2 by simp
  also have "... = rev (preOrden d) @ rev (x # preOrden i)"  by simp
  also have "... = rev (x # preOrden i @ preOrden d)" by simp
  also have "... = rev (preOrden (N x i d)) " by simp
  finally show "?P (N x i d)" by simp
 qed

(* fraortmoy lucnovdos pabrodmac paupeddeg marcarmor13 *)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a) auto

(* anaprarod *)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a) simp_all

(*pabrodmac*)
lemma
  fixes a ::"'b arbol" 
  shows "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?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 "… = rev (preOrden d) @ rev (preOrden i) @ [x]" 
      using h1 h2 by simp
    also have "… = rev (preOrden (N x i d))" by simp
    finally show ?thesis.
 qed
qed

(* ferrenseg *)
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x l r
  assume H1: "?P l"
  assume H2: "?P r"
  show "?P (N x l r)"
  proof -
    have "postOrden (espejo (N x l r)) = 
          postOrden (N x (espejo r) (espejo l))" by simp
    also have "… = postOrden (espejo r) @ postOrden (espejo l) @ [x]" 
      by simp
    also have "… = rev (preOrden r) @ rev (preOrden l) @ [x]" 
      using H1 H2 by simp
    also have "… = rev (preOrden l @ preOrden r) @ [x]" by simp
    also have "… = rev ([x] @ preOrden l @ preOrden r)" by simp
    also have "… = rev (preOrden (N x l r))" by simp
    finally show ?thesis .
  qed
qed

(* antsancab1 *)
(* Después de hacerlo como en la anterior demostración se me ocurrió cómo
relacionar ambas demostraciones.
Como hemos demostrado que
preOrden (espejo a) = rev (postOrden a)
a la inversa también queda demostrado *)
lemma "postOrden (espejo a) = rev (preOrden a)"
apply (induct a)
apply simp
apply (simp add:pre_es_rev_post)
done

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

(* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal
   dancorgar josgarsan antsancab1 *) 
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  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 h1 h2 by simp 
  finally show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" 
    by simp
qed

(* danrodcha anaprarod *)
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) simp_all

(* danrodcha anaprarod *)
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 HIi: "?P i"
  assume HId: "?P d"
  show "?P (N x i d)" using HIi HId by simp
qed

(* pablucoto marpoldia1 jeamacpov paupeddeg marcarmor13 anaprarod *)
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"
  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 (x # inOrden d ) @ rev (inOrden i)" by simp
  also have "... = rev ( inOrden i @ x # inOrden d) " by simp
  also have "... = rev (inOrden (N x i d))" by simp
  finally show "?P (N x i d)" by simp
qed

(* lucnovdos pabrodmac paupeddeg fraortmoy *)
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) auto

(* pabrodmac *)
lemma
  fixes a ::"'b arbol" 
  shows "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?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 "… =rev(inOrden d)@[x]@rev(inOrden i)" using h1 h2 by simp
    also have "… =rev(inOrden (N x i d))" by simp
    finally show ?thesis .
 qed
qed

(* ferrenseg rubgonmar *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x l r  
  assume H1: "?P l"
  assume H2: "?P r"
  show "?P (N x l r)"
  proof -
    have "inOrden (espejo (N x l r)) = 
          inOrden (N x (espejo r) (espejo l))" by simp
    also have "… = inOrden (espejo r) @ [x] @ inOrden (espejo l)" 
      by simp
    also have "… = rev (inOrden r) @ [x] @ rev (inOrden l)" 
      using H1 H2 by simp
    also have "… = rev (inOrden l @ [x] @ inOrden r)" by simp
    also have "… = rev (inOrden (N x l r))" by simp
    finally show ?thesis .
  qed
qed

(* fraortmoy *)
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" 
    using h1 h2  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
  --------------------------------------------------------------------- 
*}

(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto 
   migtermor marpoldia1 wilmorort lucnovdos  juacabsou serrodcal 
   ferrenseg paupeddeg rubgonmar jeamacpov marcarmor13 fraortmoy 
   fracorjim1 josgarsan dancorgar anaprarod antsancab1 *)
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
  --------------------------------------------------------------------- 
*}

(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto 
   migtermor marpoldia1 wilmorort lucnovdos  juacabsou serrodcal 
   pabrodmac ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13
   fraortmoy fracorjim1 josgarsan dancorgar  anaprarod antsancab1 *)
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"

(* bowma *)
fun extremo_izquierda_1 :: "'a arbol ⇒ 'a" where
  "extremo_izquierda_1 (H t)     = t"
| "extremo_izquierda_1 (N t i d) = hd (inOrden (N t i d))"

(* ivamenjim *)
(* Metaejercicio de demostración. 
   Llamando teorema_13 al teorema del ejercicio 13 *)

lemma "extremo_izquierda a = extremo_izquierda_1 a"
by (induct a, simp_all add: aux_ej12_1 teorema_13)

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

(* danrodcha crigomgom manmorjim1 ivamenjim bowma pablucoto 
   migtermor marpoldia1 wilmorort lucnovdos  juacabsou pabrodmac 
   serrodcal ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13
   fraortmoy fracorjim1 josgarsan dancorgar anaprarod antsancab1 *)
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"

(* bowma *)
fun extremo_derecha_1 :: "'a arbol ⇒ 'a" where
  "extremo_derecha_1 (H t) = t"
| "extremo_derecha_1 (N t i d) = last (inOrden (N t i d))"

(* ivamenjim *)
(* Metaejercicio de demostración. 
   Llamando teorema_12 al teorema del ejercicio 12 *)

(*
lemma "extremo_derecha a = extremo_derecha_1 a"
by (induct a, simp_all add: aux_ej12_1 teorema_12)
*)

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 12. Demostrar o refutar
     last (inOrden a) = extremo_derecha a
  --------------------------------------------------------------------- 
*}

(* danrodcha anaprarod *)
lemma aux_ej12: "inOrden a ≠ []"
apply (induct a) 
apply simp  (* poniendo simp_all se agrupan estos dos *)
apply simp
done

(* danrodcha pablucoto crigomgom  wilmorort juacabsou serrodcal 
   rubgonmar jeamacpov marcarmor13*)
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 HIi: "?P i"
  assume HId: "?P d"
  have "last (inOrden (N x i d)) = last (inOrden i @ [x] @ inOrden d)" 
    by (simp only: inOrden.simps(2))
  also have "… = last (inOrden d)" by (simp add: aux_ej12)
  also have "… = extremo_derecha d" using HId by simp
  also have "… = extremo_derecha (N x i d)" by simp
  finally show "?P (N x i d)" by simp
qed

(* ivamenjim *)
lemma aux_ej12_1: "inOrden a ≠ []"
by (induct a) simp_all 

(* ivamenjim marpoldia1 paupeddeg anaprarod antsancab1 *)
(* Igual que la anterior, pero poniendo solo by simp en el primer have *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  have "last (inOrden (N x i d)) = 
        last ((inOrden i) @ [x] @ (inOrden d))" by simp 
  also have "... = last (inOrden d)" by (simp add: aux_ej12_1)
  also have "... = extremo_derecha d" using h2 by simp 
  finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)" 
    by simp
qed

(* bowma *)
(* Casi lo mismo que el anterior,pero no hace falta suponer "?p i" *)
theorem "last (inOrden a) = extremo_derecha a" (is "?p a")
proof (induct a)
  fix t
  show "?p (H t)" by simp
next 
  fix t i d
  assume HI: "?p d"
  have "last (inOrden (N t i d)) = last (inOrden i @ [t] @ inOrden d)" 
    by simp
  also have "... = last (inOrden d)" by (simp add:aux_ej12)
  also have "... = extremo_derecha d" using HI by simp
  finally show "?p (N t i d)" by simp
qed

(* lucnovdos*)
(* El mismo que el anterior,pero sin usar patrones *)
theorem "last (inOrden a) = extremo_derecha a"
proof (induct a)
  fix x ::"'a"
  show "last (inOrden (H x)) = extremo_derecha (H x)" by simp
next
  fix x   ::"'a"
  fix i d ::"'a arbol"
  assume HI: "last (inOrden d) = extremo_derecha d"
  have "last (inOrden (N x i d)) = 
        last ((inOrden i) @ [x] @ (inOrden d))" by simp 
  also have "… = last (inOrden d)" by (simp add: aux_ej12)
  also have "… = extremo_derecha d" using HI by simp
  also have "… = extremo_derecha (N x i d)" by simp
  finally show "last (inOrden (N x i d)) = extremo_derecha (N x i d)" 
    by simp
qed

(* migtermor *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix h
  show "?P (H h)" by simp
next
  fix n i
  fix d assume HId: "?P d"
  have AUX: "¬ (inOrden d = [])" (is "?Q d")
     proof (induct d)
      fix hd
      show "?Q (H hd)" by simp
     next
     fix nd
     fix id assume HIid: "?Q id"
     fix dd assume HIdd: "?Q dd"
     show "?Q (N nd id dd)" using HIid HIdd by simp
     qed
  have "last (inOrden (N n i d)) = last (inOrden i @[n]@inOrden d)" 
    by simp
  also have "… = last (inOrden d)" using AUX by simp
  also have "… = extremo_derecha d" using HId by simp
  finally show "?P (N n i d)"  by simp
qed

(* pabrodmac fraortmoy *)
lemma Aux_ej12: "inOrden a ≠ []"
by (induct a) auto

(* pabrodmac fraortmoy *)
theorem "last (inOrden a) = extremo_derecha a"
by (induct a)(auto simp add: Aux_ej12)

(* pabrodmac *)
lemma
  fixes a ::"'b arbol" 
  shows "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?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: Aux_ej12)
    also have "… = extremo_derecha d" using h1 h2 by simp
    also have "… = extremo_derecha (N x i d)" by simp
    finally show ?thesis .
  qed
qed

(* ferrenseg *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x l r
  assume HI: "?P r"
  show "?P (N x l r)"
  proof -  
    have "last (inOrden (N x l r)) = 
          last (inOrden r @ [x] @ inOrden r)" by simp
    also have "… = last (inOrden r)"  by (simp add: inOrden)
    also have "… = extremo_derecha r" using HI by simp
    also have "… =  extremo_derecha (N x l r)" by simp
    finally show ?thesis .
  qed
qed

(* fraortmoy *)
lemma
  fixes a ::"'b arbol" 
  shows "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (N x i d)" using h1 h2 by (simp add: Aux_ej12)  
qed

(* dancorgar *)
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix t
  show "?P (H t)" by simp
next
  fix t i d
  assume H2: "?P d"
  have "last (inOrden (N t i d)) = last ((inOrden i)@[t]@(inOrden d))" 
    by simp
  also have "… = last (inOrden d)"
  proof (induct d)
    fix x
    show "last (inOrden i @ [t] @ inOrden (H x)) = last (inOrden (H x))" 
      by simp
  next
    fix x1a d1 d2
    show "last (inOrden i @ [t] @ inOrden (N x1a d1 d2)) = 
          last (inOrden (N x1a d1 d2))" by simp
  qed
  finally show "last (inOrden (N t i d)) = extremo_derecha (N t i d)" 
    using H2 by simp
qed

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

(* danrodcha pablucoto crigomgom juacabsou serrodcal jeamacpov
   marcarmor13 *) 
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 HIi: "?P i"
  assume HId: "?P d"
  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: aux_ej12)
  also have "… = extremo_izquierda i" using HIi by simp
  also have "… = extremo_izquierda (N x i d)" by simp
  finally show "?P (N x i d)" by simp
qed

(* bowma lucnovdos dancorgar anaprarod *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?p a")
proof (induct a)
  fix t
  show "?p (H t)" by simp
next
  fix t i d 
  assume HI: "?p i"
  have "hd (inOrden (N t i d)) = hd (inOrden i @ [t] @ inOrden d)" 
    by simp
  also have "… = hd (inOrden i)" by (simp add: aux_ej12)
  also have "… = extremo_izquierda i" using HI by simp
  finally show "?p (N t i d)" by simp
qed

(* migtermor *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
  fix h
  show "?P (H h)" by simp
next
  fix n d
  fix i assume HId: "?P i"
  have AUX: "¬ (inOrden i = [])" (is "?Q i")
     proof (induct i)
      fix hi
      show "?Q (H hi)" by simp
     next
     fix ni
     fix ii assume HIid: "?Q ii"
     fix di assume HIdd: "?Q di"
     show "?Q (N ni ii di)" using HIid HIdd by simp
     qed
  have "hd (inOrden (N n i d)) = hd (inOrden i @[n]@inOrden d)" by simp
  also have "… = hd (inOrden i)" using AUX by simp
  also have "… = extremo_izquierda i" using HId by simp
  finally show "?P (N n i d)"  by simp
qed

(* ivamenjim marpoldia1 wilmorort paupeddeg rubgonmar antsancab1 *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  have "hd (inOrden (N x i d)) = hd ((inOrden i) @ [x] @ (inOrden d))" 
    by simp
  also have "... = hd (inOrden i)" by (simp add: aux_ej12_1)
  also have "... = extremo_izquierda i" using h1 by simp 
  finally show "hd (inOrden (N x i d)) = extremo_izquierda (N x i d)" 
    by simp
qed

(* pabrodmac paupeddeg*)
theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a)(auto simp add: Aux_ej12)

(* pabrodmac *)
lemma
  fixes a ::"'b arbol" 
  shows "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?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: Aux_ej12)
    also have "… = extremo_izquierda i" using h1 h2 by simp
    also have "… = extremo_izquierda (N x i d)" by simp
    finally show ?thesis .
  qed
qed

(* ferrenseg *)
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x l r
  assume HI: "?P l"
  show "?P (N x l r)"
  proof - 
    have "hd (inOrden (N x l r)) = 
          hd (inOrden l @ [x] @ inOrden r)" by simp
    also have "… = hd (inOrden l)"  by (simp add: Aux_ej12)
    also have "… = extremo_izquierda l" using HI by simp
    also have "… = extremo_izquierda (N x l r)" by simp
    finally show ?thesis .
  qed
qed

(* fraortmoy *)
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 h1: "?P i"
  assume h2: "?P d"
  show "?P (N x i d)" using h1 h2 by (simp add: Aux_ej12)
qed 

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

(* danrodcha pabrodmac dancorgar anaprarod *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
  fix x i d
  show "?P (N x i d)" by simp
qed

(* danrodcha *)
theorem "hd (preOrden1 a) = last (postOrden a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
  fix x i d
  assume HIi: "?P i"
  assume HId: "?P d"
  have "hd (preOrden1 (N x i d)) = hd (x#preOrden1 i @ preOrden1 d)"
    by (simp only: preOrden1.simps(2))
  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 only: postOrden.simps(2))
  finally show "?P (N x i d)" by simp
qed

(* pablucoto crigomgom bowma marpoldia1 wilmorort lucnovdos juacabsou
   jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *) 
(*Similar al anterior*) 
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"
  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 "?P (N x i d)" by simp
qed

(* migtermor *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
 fix h
 show "?P (H h)" by simp
next
 fix n i d
 have "hd (preOrden (N n (i :: 'a arbol) (d :: 'a arbol))) = 
       hd ([n]@preOrden i@preOrden d)" by simp
 (* Si no especifico que i y d son árboles, salta un error de tipo. 
    Supongo que será por no haber asumido hipótesis sobre ellos *)
 also have "… = last (postOrden (N n i d))" by simp
 show "?P (N n i d)" by simp
qed

(* ivamenjim serrodcal antsancab1 *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  have "hd (preOrden (N x i d)) = hd ([x] @ (preOrden i) @ (preOrden d))" 
    by simp
  also have "... = hd ([x])" by simp
  finally show "hd (preOrden (N x i d)) = last (postOrden (N x i d))" 
    by simp
qed

(* pabrodmac paupeddeg fraortmoy *)
theorem "hd (preOrden a) = last (postOrden a)"
by (induct a) auto  

(* pabrodmac *)
lemma
  fixes a ::"'b arbol" 
  shows "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (N x i d)"   
  proof -               
    have "hd (preOrden (N x i d) )= x" by simp
    also have "… = last (postOrden (N x i d))" by simp
    finally show ?thesis .
 qed
qed

(* Me he dado cuenta que no es necesario asumir ninguna hipótesis de
   inducción puesto que no es necesario utilizarlas, así que no se si
   está bien hecho puesto que no se aplicaría inducción *)  

(* ferrenseg *)
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 l r
  assume H: "a = N x l r"
  show "?P a"
  proof - 
    have "hd (preOrden a) = hd (preOrden (N x l r))" using H by simp
    also have "… = hd (x # (preOrden l @ preOrden r))" by simp
    also have "… = x" by simp
    also have "… = last (postOrden l @ postOrden r @ [x])" by simp
    also have "… = last (postOrden (N x l r))" by simp
    also have "… = last (postOrden a)" using H by simp
    finally show ?thesis .
  qed
qed  

(* fraortmoy *)
theorem "hd (preOrden a) = last (postOrden a)"
apply (induct a)
apply simp
apply simp
done

(* fraortmoy *)
(* como ya se ha comentado antes, no se usan hipótesis de inducción *)
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
  show "?P (N x i d)" by simp
qed


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

(* danrodcha *)
theorem "hd (preOrden1 a) = raiz a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next  
  fix x i d
  assume HIi: "?P i"
  assume HId: "?P d"
  have "hd (preOrden1 (N x i d)) = hd (x#preOrden1 i @ preOrden1 d)"
    by (simp only: preOrden1.simps(2))
  also have "… = x" by simp
  also have "… = raiz (N x i d)" by simp
  finally show "?P (N x i d)" by simp
qed

(* danrodcha pabrodmac dancorgar anaprarod *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
  fix x i d
  show "?P (N x i d)" by simp
qed

(* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos
   juacabsou serrodcal jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *) 
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"
  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 " ?P (N x i d)" by simp
qed

(* bowma *)
(* similar al anterior pero sin suponer "?p d" *)
theorem "hd (preOrden a) = last (postOrden a)" (is "?p a")
proof (induct a)
  fix t
  show "?p (H t)" by simp
next
  fix t i d
  assume HI: "?p i"
  have "hd (preOrden (N t i d)) = hd ([t] @ preOrden i @ preOrden d)" 
    by simp
  also have "… = t" by simp
  also have "… = last (postOrden i @ postOrden d @ [t])" by simp
  also have "… = last (postOrden (N t i d))" by simp
  finally show "?p (N t i d)" by simp
qed

(* migtermor *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
 fix h
 show "?P (H h)" by simp
next
 fix n i d
 have "hd (preOrden (N n (i :: 'a arbol) (d :: 'a arbol))) = 
       hd ([n]@preOrden i@preOrden d)" by simp
 also have "… = raiz (N n i d)" by simp
 finally show "?P (N n i d)" by simp
qed

(* ivamenjim: sin usar patrones *)
theorem "hd (preOrden a) = raiz a" 
proof (induct a)
  fix x ::"'a"
  show "hd (preOrden (H x)) = raiz (H x)" by simp 
next
  fix x ::"'a"
  fix i ::"'a arbol" assume h1: "hd (preOrden i) = raiz i"
  fix d ::"'a arbol" assume h2: "hd (preOrden d) = raiz d"
  have "hd (preOrden (N x i d)) = hd ([x] @ (preOrden i) @ (preOrden d))" 
    by simp
  also have "... = hd ([x])" by simp
  finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp
qed

(* pabrodmac paupeddeg fraortmoy *)
theorem "hd (preOrden a) = raiz a"
by (induct a) auto

(* pabrodmac *)
lemma
  fixes a ::"'b arbol" 
  shows "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (N x i d)"   
  proof -               
    have "hd (preOrden (N x i d) )= x" by simp
    also have "… = raiz (N x i d)" by simp
    finally show ?thesis .
 qed
qed

(* Me he dado cuenta que no es necesario asumir ninguna hipótesis de
   inducción puesto que no es necesario utilizarlas, así que no se si
   está bien hecho puesto que no se aplicaría inducción *)  

(* ferrenseg *)
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 l r
  assume H: "a = N x l r"
  show "?P a"
  proof -
    have "hd (preOrden a) = hd (preOrden (N x l r))" using H by simp
    also have "… = hd (x#(preOrden l @ preOrden r))" by simp
    also have "… = x" by simp
    also have "… = raiz (N x l r)" by simp
    also have "… = raiz a" using H by simp
    finally show ?thesis .
  qed
qed  

(* fraortmoy *)
theorem "hd (preOrden a) = raiz a"
  apply (induct a)
  apply simp
  apply simp
done

(* fraortmoy *)
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
  show "?P (N x i d)" by simp
qed

(* antsancab1 *)
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x
  fix i assume H1: "?P i"
  fix d assume H2: "?P d"
  have "hd (preOrden (N x i d)) = hd ([x] @ preOrden i @ preOrden d)" by simp
  also have "... = hd [x]" by simp
  also have "... = raiz (H x)" by simp
  also have "... = raiz (N x i d)" by simp (* estos dos últimos no eran necesarios pero me queda más claro *)
  finally show "hd (preOrden (N x i d)) = raiz (N x i d)" by simp
qed

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

(* crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos
   juacabsou pabrodmac serrodcal ferrenseg jeamacpov paupeddeg rubgonmar
   marcarmor13 fraortmoy dancorgar anaprarod antsancab1 *)  
theorem "hd (inOrden a) = raiz a"
quickcheck
oops

(* danrodcha anaprarod:
Auto Quickcheck found a counterexample:
  a = N a1 (H a2) (H a1)
Evaluated terms:
  hd (inOrden a) = a2
  raiz a = a1 *)

(* ivamenjim marpoldia1 *)
theorem "hd (inOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  have "hd (inOrden (N x i d)) = hd ((inOrden i) @ [x] @ (inOrden d))" by simp
  also have "... = hd (inOrden i)" by (simp add: aux_ej12_1) 
  (* Perdemos la x, luego se refuta el enunciado del teorema *)
oops

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 17. Demostrar o refutar
     last (postOrden a) = raiz a
  --------------------------------------------------------------------- 
*}

(* danrodcha pabrodmac dancorgar anaprarod *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
  fix x i d
  show "?P (N x i d)" by simp
qed

(* danrodcha *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
  fix x i d
  assume HIi: "?P i"
  assume HId: "?P d"
  have "last (postOrden (N x i d)) = 
        last (postOrden i @ postOrden d @ [x])"
    by (simp only: postOrden.simps(2))
  also have "… = x" by simp
  also have "… = raiz (N x i d)" by (simp only: raiz.simps(2))
  finally show "?P (N x i d)" by simp
qed

(* pablucoto crigomgom ivamenjim marpoldia1 wilmorort lucnovdos
   juacabsou serrodcal jeamacpov paupeddeg rubgonmar marcarmor13 anaprarod *) 
(* Similar al anterior *) 
theorem "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"
  have "last (postOrden (N x i d)) = 
        last ( postOrden i @ postOrden d @ [x])" by simp
  also have "... = x" by simp
  also have "... = raiz (N x i d) " by simp
  finally show " ?P (N x i d)" by simp
qed

(* bowma *)
(* También sin usar el supuesto "?p d" *)
theorem "last (postOrden a) = raiz a" (is "?p a")
proof (induct a)
  fix t
  show "?p (H t)" by simp
next
  fix t i d
  assume "?p i"
  (* si quito este supuesto, hay error pero no sé dónde se lo está
     usando *) 
  have "last (postOrden (N t i d)) = 
        last (postOrden i @ postOrden d @ [t])" by simp
  also have "... = t" by simp
  also have "... = raiz (N t i d)" by simp
  finally show "?p (N t i d)" by simp
qed
(*
Comentario de antsancab1:
No tengo muy claro por qué es, pero si en lugar de utilizar ?p al final lo pones completo:
finally show "last (postOrden (N t i d)) = raiz (N t i d)" by simp
No devuelve ningún error. No se si será que después de ?p espera un único elemento
*)

(* migtermor *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
 fix h
 show "?P (H h)" by simp
next
 fix n i d
 have "last (postOrden (N n (i :: 'a arbol) (d :: 'a arbol))) = 
       last (postOrden i@postOrden d@[n])" by simp
 also have "… = raiz (N n i d)" by simp
 finally show "?P (N n i d)" by simp
qed

(* ivamenjim: sin usar patrones *)
theorem "last (postOrden a) = raiz a" 
proof (induct a)
  fix x::"'a" 
  show "last (postOrden (H x)) = raiz (H x)" by simp 
next
  fix x::"'a"  
  fix i::"'a arbol" assume h1: "last (postOrden i) = raiz i"
  fix d::"'a arbol" assume h2: "last (postOrden d) = raiz d"
  have "last (postOrden (N x i d)) = 
        last ((postOrden i) @ (postOrden d) @ [x])" by simp
  also have "... = last ([x])" by simp 
  finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp
qed

(* pabrodmac paupeddeg fraortmoy *)
theorem "last (postOrden a) = raiz a"
by (induct a) auto
 
(* pabrodmac *)
lemma
  fixes a ::"'b arbol" 
  shows "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (H x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (N x i d)"   
  proof -               
    have "last (postOrden (N x i d))= x" by simp
    also have "… = raiz (N x i d)" by simp
    finally show ?thesis .
 qed
qed

(* Me he dado cuenta que no es necesario asumir ninguna hipótesis de
   inducción puesto que no es necesario utilizarlas, así que no se si
   está bien hecho puesto que no se aplicaría inducción *)  

(* ferrenseg *)

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 l r
  assume H: "a = N x l r"
  show "?P a"
  proof -
    have "last (postOrden a) = last (postOrden (N x l r))" using H by simp
    also have "… = last (postOrden l @ preOrden r @ [x])" by simp
    also have "… = x" by simp
    also have "… = raiz a" using H by simp
    finally show ?thesis .
  qed
qed  

(* fraortmoy *)
theorem "last (postOrden a) = raiz a"
apply (induct a)
apply simp
apply simp
done

(* fraortmoy *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x i d
  show "?P (N x i d)" by simp
qed

end

(* antsancab1 *)
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x
  show "?P (H x)" by simp
next
  fix x
  fix i assume H1: "?P i"
  fix d assume H2: "?P d"
  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 (H x)" by simp
  also have "... = raiz (N x i d)" by simp
  finally show "last (postOrden (N x i d)) = raiz (N x i d)" by simp
qed