Acciones

Diferencia entre revisiones de «Relación 6»

De Razonamiento automático (2016-17)
m (Texto reemplazado: «isar» por «isabelle»)
 
(No se muestran 207 ediciones intermedias de 25 usuarios)
Línea 1: Línea 1:
−
<source lang="isar">
+
<source lang="isabelle">
 
chapter {* R6: Recorridos de árboles *}
 
chapter {* R6: Recorridos de árboles *}
  
Línea 16: Línea 16:
 
       c    g
 
       c    g
 
       / \  / \
 
       / \  / \
−
     a  d f  h
+
     a  d f  3
 
   se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
 
   se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
 
*}
 
*}
  
−
(* ivamenjim marpoldia1*)
+
(* 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"
 
datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"
Línea 38: Línea 41:
 
*}
 
*}
  
−
(* ivamenjim *)
+
(* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor
 +
  wilmorort lucnovdos serrodcal pabrodmac jeamacpov paupeddeg
 +
  marcarmor13 josgarsan dancorgar anaprarod antsancab1 *)
  
 
fun preOrden :: "'a arbol ⇒ 'a list" where
 
fun preOrden :: "'a arbol ⇒ 'a list" where
−
   "preOrden (H t) = [t]"
+
   "preOrden (H t)     = [t]"
 
| "preOrden (N t i d) = [t] @ (preOrden i) @ (preOrden d)"
 
| "preOrden (N t i d) = [t] @ (preOrden i) @ (preOrden d)"
  
−
(* danrodcha crigomgom *)
+
(* danrodcha crigomgom manmorjim1 bowma juacabsou ferrenseg
 +
  rubgonmar paupeddeg fracorjim1 *)
 
fun preOrden1 :: "'a arbol ⇒ 'a list" where
 
fun preOrden1 :: "'a arbol ⇒ 'a list" where
−
   "preOrden1 (H x) = [x]"
+
   "preOrden1 (H x)     = [x]"
−
| "preOrden1 (N x i d) = x#preOrden1 i @ preOrden1 d"
+
| "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)))   
 
value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))   
Línea 69: Línea 75:
 
*}
 
*}
  
−
(* ivamenjim  danrodcha crigomgom*)
+
(* 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
 
fun postOrden :: "'a arbol ⇒ 'a list" where
−
   "postOrden (H t) = [t]"
+
   "postOrden (H t)     = [t]"
 
| "postOrden (N t i d) = (postOrden i) @ (postOrden d) @ [t]"
 
| "postOrden (N t i d) = (postOrden i) @ (postOrden d) @ [t]"
  
Línea 89: Línea 98:
 
*}
 
*}
  
−
(* ivamenjim crigomgom*)
+
(* 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
 
fun inOrden :: "'a arbol ⇒ 'a list" where
−
   "inOrden (H t) = [t]"
+
   "inOrden (H t)     = [t]"
 
| "inOrden (N t i d) = (inOrden i) @ [t] @ (inOrden d)"
 
| "inOrden (N t i d) = (inOrden i) @ [t] @ (inOrden d)"
  
−
(* danrodcha *)
+
(* danrodcha manmorjim1 fracorjim1 *)
 
fun inOrden1 :: "'a arbol ⇒ 'a list" where
 
fun inOrden1 :: "'a arbol ⇒ 'a list" where
−
   "inOrden1 (H t) = [t]"
+
   "inOrden1 (H t)     = [t]"
 
| "inOrden1 (N t i d) = inOrden1 i @ t#inOrden1 d"
 
| "inOrden1 (N t i d) = inOrden1 i @ t#inOrden1 d"
  
Línea 104: Línea 115:
 
value "inOrden1 (N e (N c (H a) (H d)) (N g (H f) (H h)))
 
value "inOrden1 (N e (N c (H a) (H d)) (N g (H f) (H h)))
 
       = [a,c,d,e,f,g,h]"
 
       = [a,c,d,e,f,g,h]"
 +
 +
(* manmorjim1 *)
 +
lemma "inOrden t = inOrden1 t"
 +
apply (induct t)
 +
apply auto
 +
done
  
 
text {*   
 
text {*   
Línea 115: Línea 132:
 
*}
 
*}
  
−
(* ivamenjim danrodcha crigomgom*)
+
(* 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
 
fun espejo :: "'a arbol ⇒ 'a arbol" where
−
   "espejo (H t) = H t"
+
   "espejo (H t)     = H t"
 
| "espejo (N t i d) = N t (espejo d) (espejo i)"
 
| "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)))  
 
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))"
 
       = N e (N g (H h) (H f)) (N c (H d) (H a))"
−
 
  
 
text {*   
 
text {*   
Línea 132: Línea 150:
 
*}
 
*}
  
−
(* ivamenjim *)
+
(* ivamenjim migtermor wilmorort juacabsou serrodcal dancorgar josgarsan
−
 
+
*)  
 
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
 
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 142: Línea 160:
 
   fix i assume h1: "?P i"
 
   fix i assume h1: "?P i"
 
   fix d assume h2: "?P d"
 
   fix d assume h2: "?P d"
−
   have "preOrden (espejo (N x i d)) = preOrden (N x (espejo d) (espejo i))" by simp
+
   have "preOrden (espejo (N x i d)) =  
−
   also have "... = [x] @ (preOrden (espejo d)) @ (preOrden (espejo i))" by simp
+
        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 "... = [x] @ (preOrden (espejo d)) @ (preOrden (espejo i))"  
−
   finally show "preOrden (espejo (N x i d)) = rev (postOrden (N x i d))" by simp
+
    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
 
qed
  
−
(* danrodcha *)
+
(* danrodcha paupeddeg anaprarod *)
 
lemma  "preOrden (espejo a) = rev (postOrden a)"
 
lemma  "preOrden (espejo a) = rev (postOrden a)"
 
by (induct a) simp_all
 
by (induct a) simp_all
  
−
(* danrodcha crigomgom*)
+
 
−
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
+
(* danrodcha crigomgom fracorjim1 *)
 +
lemma  "preOrden1 (espejo a) = rev (postOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
 
   fix x
 
   fix x
Línea 161: Línea 184:
 
   assume HIi: "?P i"
 
   assume HIi: "?P i"
 
   assume HId: "?P d"
 
   assume HId: "?P d"
−
   have "preOrden (espejo (N x i d)) = preOrden (N x (espejo d) (espejo i))"
+
   have "preOrden1 (espejo (N x i d)) =  
 +
        preOrden1 (N x (espejo d) (espejo i))"
 
     by (simp only: espejo.simps(2))
 
     by (simp only: espejo.simps(2))
−
   also have "… = x#preOrden (espejo d) @ preOrden (espejo i)"
+
   also have "… = x#preOrden1 (espejo d) @ preOrden1 (espejo i)"
−
     by (simp only: preOrden.simps(2))
+
     by (simp only: preOrden1.simps(2))
 
   also have"… = x#rev (postOrden d) @ rev (postOrden i)"  
 
   also have"… = x#rev (postOrden d) @ rev (postOrden i)"  
 
     using HIi HId by simp
 
     using HIi HId by simp
Línea 171: Línea 195:
 
qed
 
qed
  
−
(* danrodcha *)
+
(* danrodcha fraortmoy anaprarod *)
 
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
 
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 181: Línea 205:
 
   assume HId: "?P d"
 
   assume HId: "?P d"
 
   show "?P (N x i d)" using HIi HId by simp
 
   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
 
qed
  
Línea 190: Línea 333:
 
*}
 
*}
  
−
(* ivamenjim crigomgom*)
+
(* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal
−
 
+
  dancorgar josgarsan antsancab1 *)  
 
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
 
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 200: Línea 343:
 
   fix i assume h1: "?P i"
 
   fix i assume h1: "?P i"
 
   fix d assume h2: "?P d"
 
   fix d assume h2: "?P d"
−
   have "postOrden (espejo (N x i d)) = postOrden (N x (espejo d) (espejo i))" by simp
+
   have "postOrden (espejo (N x i d)) =  
−
   also have "... = (postOrden (espejo d)) @ (postOrden (espejo i)) @ [x]" by simp
+
        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 "... = (postOrden (espejo d)) @ (postOrden (espejo i)) @ [x]"  
−
   finally show "postOrden (espejo (N x i d)) = rev (preOrden (N x i d))" by simp
+
    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
 
qed
  
−
(* danrodcha *)
+
(* danrodcha fraortmoy anaprarod *)
 
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
 
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 217: Línea 365:
 
   show "?P (N x i d)" using HIi HId by simp
 
   show "?P (N x i d)" using HIi HId by simp
 
qed
 
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 {*   
 
text {*   
Línea 225: Línea 460:
 
*}
 
*}
  
−
(* ivamenjim crigomgom*)
+
(* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal
−
 
+
  dancorgar josgarsan antsancab1 *)  
 
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
 
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 235: Línea 470:
 
   fix i assume h1: "?P i"
 
   fix i assume h1: "?P i"
 
   fix d assume h2: "?P d"
 
   fix d assume h2: "?P d"
−
   have "inOrden (espejo (N x i d)) = inOrden (N x (espejo d) (espejo i))" by simp
+
   have "inOrden (espejo (N x i d)) = inOrden (N x (espejo d) (espejo i))"  
−
   also have "... = (inOrden (espejo d)) @ [x] @ (inOrden (espejo i))" by simp
+
    by simp
−
   also have "... = rev (inOrden d) @ [x] @ rev (inOrden i)" using h1 h2 by simp  
+
   also have "... = (inOrden (espejo d)) @ [x] @ (inOrden (espejo i))"  
−
   finally show "inOrden (espejo (N x i d)) = rev (inOrden (N x i d))" by simp
+
    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
 
qed
  
−
(* danrodcha *)
+
(* danrodcha anaprarod *)
 
theorem "inOrden (espejo a) = rev (inOrden a)"
 
theorem "inOrden (espejo a) = rev (inOrden a)"
 
by (induct a) simp_all
 
by (induct a) simp_all
  
−
(* danrodcha *)
+
(* danrodcha anaprarod *)
 
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
 
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 255: Línea 494:
 
   assume HId: "?P d"
 
   assume HId: "?P d"
 
   show "?P (N x i d)" using HIi HId by simp
 
   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
 
qed
  
Línea 266: Línea 587:
 
*}
 
*}
  
−
(* danrodcha crigomgom*)
+
(* 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
 
fun raiz :: "'a arbol ⇒ 'a" where
−
   "raiz (H x) = x"
+
   "raiz (H x)     = x"
 
| "raiz (N x i d) = x"
 
| "raiz (N x i d) = x"
  
Línea 283: Línea 607:
 
*}
 
*}
  
−
(* danrodcha crigomgom*)
+
(* 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
 
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
−
   "extremo_izquierda (H x) = x"
+
   "extremo_izquierda (H x)     = x"
 
| "extremo_izquierda (N x i d) = extremo_izquierda i"
 
| "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"
 
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 {*   
 
text {*   
Línea 300: Línea 639:
 
*}
 
*}
  
−
(* danrodcha crigomgom*)
+
(* 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
 
fun extremo_derecha :: "'a arbol ⇒ 'a" where
 
   "extremo_derecha (H x) = x"
 
   "extremo_derecha (H x) = x"
Línea 306: Línea 648:
  
 
value "extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h"
 
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 {*   
 
text {*   
Línea 314: Línea 670:
 
*}
 
*}
  
−
(* danrodcha *)
+
(* danrodcha anaprarod *)
 
lemma aux_ej12: "inOrden a ≠ []"
 
lemma aux_ej12: "inOrden a ≠ []"
 
apply (induct a)  
 
apply (induct a)  
−
apply simp
+
apply simp (* poniendo simp_all se agrupan estos dos *)
 
apply simp
 
apply simp
 
done
 
done
  
−
(* danrodcha *)
+
(* danrodcha pablucoto crigomgom  wilmorort juacabsou serrodcal
 +
  rubgonmar jeamacpov marcarmor13*)
 
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
 
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 336: Línea 693:
 
   also have "… = extremo_derecha (N x i d)" by simp
 
   also have "… = extremo_derecha (N x i d)" by simp
 
   finally show "?P (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
 
qed
  
Línea 345: Línea 871:
 
*}
 
*}
  
−
(* danrodcha *)
+
(* danrodcha pablucoto crigomgom juacabsou serrodcal jeamacpov
 +
  marcarmor13 *)  
 
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
 
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 361: Línea 888:
 
   finally show "?P (N x i d)" by simp
 
   finally show "?P (N x i d)" by simp
 
qed
 
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 {*   
 
text {*   
Línea 369: Línea 1009:
 
*}
 
*}
  
−
(* danrodcha *)
+
(* danrodcha pabrodmac dancorgar anaprarod *)
 
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
 
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 379: Línea 1019:
  
 
(* danrodcha *)
 
(* danrodcha *)
−
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
+
theorem "hd (preOrden1 a) = last (postOrden a)" (is "?P a")
 
proof (induct a)
 
proof (induct a)
 
   fix x
 
   fix x
Línea 386: Línea 1026:
 
   assume HIi: "?P i"
 
   assume HIi: "?P i"
 
   assume HId: "?P d"
 
   assume HId: "?P d"
−
   have "hd (preOrden (N x i d)) = hd (x#preOrden i @ preOrden d)"
+
   have "hd (preOrden1 (N x i d)) = hd (x#preOrden1 i @ preOrden1 d)"
−
     by (simp only: preOrden.simps(2))
+
     by (simp only: preOrden1.simps(2))
 
   also have "… = x" by simp
 
   also have "… = x" by simp
 
   also have "… = last (postOrden i @ postOrden d @ [x])" by simp
 
   also have "… = last (postOrden i @ postOrden d @ [x])" by simp
Línea 394: Línea 1034:
 
   finally show "?P (N x i d)" by simp
 
   finally show "?P (N x i d)" by simp
 
qed
 
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 {*   
 
text {*   
Línea 403: Línea 1160:
  
 
(* danrodcha *)
 
(* danrodcha *)
−
theorem "hd (preOrden a) = raiz a" (is "?P a")
+
theorem "hd (preOrden1 a) = raiz a" (is "?P a")
 
proof (induct a)
 
proof (induct a)
 
   fix x
 
   fix x
 
   show "?P (H x)" by simp
 
   show "?P (H x)" by simp
 +
next 
 
   fix x i d
 
   fix x i d
 
   assume HIi: "?P i"
 
   assume HIi: "?P i"
 
   assume HId: "?P d"
 
   assume HId: "?P d"
−
   have "hd (preOrden (N x i d)) = hd (x#preOrden i @ preOrden d)"
+
   have "hd (preOrden1 (N x i d)) = hd (x#preOrden1 i @ preOrden1 d)"
−
     by (simp only: preOrden.simps(2))
+
     by (simp only: preOrden1.simps(2))
 
   also have "… = x" by simp
 
   also have "… = x" by simp
 
   also have "… = raiz (N x i d)" by simp
 
   also have "… = raiz (N x i d)" by simp
Línea 417: Línea 1175:
 
qed
 
qed
  
−
(* danrodcha *)
+
(* 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")
 
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)
 
proof (induct a)
 
   fix x
 
   fix x
 
   show "?P (H x)" by simp
 
   show "?P (H x)" by simp
 +
next
 
   fix x i d
 
   fix x i d
 
   show "?P (N x i d)" by simp
 
   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
 
qed
  
Línea 433: Línea 1333:
 
*}
 
*}
  
 +
(* 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"
 
theorem "hd (inOrden a) = raiz a"
 +
quickcheck
 
oops
 
oops
  
−
(* danrodcha:
+
(* danrodcha anaprarod:
 
Auto Quickcheck found a counterexample:
 
Auto Quickcheck found a counterexample:
−
   a = N a⇩1 (H a⇩2) (H a⇩1)
+
   a = N a1 (H a2) (H a1)
 
Evaluated terms:
 
Evaluated terms:
−
   hd (inOrden a) = a⇩2
+
   hd (inOrden a) = a2
−
   raiz a = a⇩1 *)
+
   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 {*   
 
text {*   
Línea 450: Línea 1368:
 
*}
 
*}
  
−
(* danrodcha *)
+
(* danrodcha pabrodmac dancorgar anaprarod *)
 
theorem "last (postOrden a) = raiz a" (is "?P a")
 
theorem "last (postOrden a) = raiz a" (is "?P a")
 
proof (induct a)
 
proof (induct a)
Línea 467: Línea 1385:
 
   assume HIi: "?P i"
 
   assume HIi: "?P i"
 
   assume HId: "?P d"
 
   assume HId: "?P d"
−
   have "last (postOrden (N x i d)) = last (postOrden i @ postOrden d @ [x])"
+
   have "last (postOrden (N x i d)) =  
 +
        last (postOrden i @ postOrden d @ [x])"
 
     by (simp only: postOrden.simps(2))
 
     by (simp only: postOrden.simps(2))
 
   also have "… = x" by simp
 
   also have "… = x" by simp
 
   also have "… = raiz (N x i d)" by (simp only: raiz.simps(2))
 
   also have "… = raiz (N x i d)" by (simp only: raiz.simps(2))
 
   finally show "?P (N x i d)" by simp
 
   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
 
qed
  
 
end
 
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
 +
 
</source>
 
</source>

Revisión actual del 13:11 16 jul 2018

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
Obtenido de «https://www.glc.us.es/~jalonso/RA2016/index.php?title=Relación_6&oldid=1474»