Relación 6
De Razonamiento automático (2016-17)
Revisión del 20:11 6 dic 2016 de Pabrodmac (discusión | contribuciones)
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*)
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 *)
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 *)
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 *)
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 *)
fun inOrden :: "'a arbol ⇒ 'a list" where
"inOrden (H t) = [t]"
| "inOrden (N t i d) = (inOrden i) @ [t] @ (inOrden d)"
(* danrodcha manmorjim1 *)
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 *)
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 *)
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 *)
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induct a) simp_all
(* danrodcha crigomgom*)
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"
have "preOrden (espejo (N x i d)) = preOrden (N x (espejo d) (espejo i))"
by (simp only: espejo.simps(2))
also have "… = x#preOrden (espejo d) @ preOrden (espejo i)"
by (simp only: preOrden.simps(2))
also have"… = x#rev (postOrden d) @ rev (postOrden i)"
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 *)
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*)
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
(* 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
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que
postOrden (espejo a) = rev (preOrden a)
---------------------------------------------------------------------
*}
(* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal *)
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 *)
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*)
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*)
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a) auto
(*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
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que
inOrden (espejo a) = rev (inOrden a)
---------------------------------------------------------------------
*}
(* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal *)
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 *)
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a) simp_all
(* danrodcha *)
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 *)
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 *)
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
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*)
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 *)
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 *)
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 *)
lemma aux_ej12: "inOrden a ≠ []"
apply (induct a)
apply simp
apply simp
done
(* danrodcha pablucoto crigomgom wilmorort juacabsou *)
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 *)
(* 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 *)
lemma Aux_ej12: "inOrden a ≠ []"
by (induct a) auto
(* pabrodmac *)
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
text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
hd (inOrden a) = extremo_izquierda a
---------------------------------------------------------------------
*}
(* danrodcha pablucoto crigomgom juacabsou*)
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 *)
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 *)
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 *)
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
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
hd (preOrden a) = last (postOrden a)
---------------------------------------------------------------------
*}
(* danrodcha pabrodmac *)
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 (preOrden 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 (preOrden (N x i d)) = hd (x#preOrden i @ preOrden d)"
by (simp only: preOrden.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 *) (*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 *)
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 *)
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
text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
*}
(* danrodcha *)
theorem "hd (preOrden 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 "hd (preOrden (N x i d)) = hd (x#preOrden i @ preOrden d)"
by (simp only: preOrden.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 *)
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 *)
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 *)
theorem "hd (preOrden a) = raiz a"
by (induct a) auto
text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
*}
(*crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos juacabsou *)
theorem "hd (inOrden a) = raiz a"
quickcheck
oops
(* danrodcha:
Auto Quickcheck found a counterexample:
a = N a⇩1 (H a⇩2) (H a⇩1)
Evaluated terms:
hd (inOrden a) = a⇩2
raiz a = a⇩1 *)
(* 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 *)
qed
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
*}
(* 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
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 *) (*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
(* 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
end