Mjoseh: Página creada con « chapter ‹R13: Recorridos de árboles› theory R13_sol imports Main begin text ‹---------------------------------------------------------…»

2020-05-21T09:54:48Z

Página creada con «<source lang = "isabelle"> chapter ‹R13: Recorridos de árboles› theory R13_sol imports Main begin text ‹---------------------------------------------------------…»

Página nueva

<source lang = "isabelle">
chapter ‹R13: Recorridos de árboles›

theory R13_sol
imports Main
begin

text ‹------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que tiene información en los nodos y en las hojas.
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
a d f h
se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
---------------------------------------------------------------------›

datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"

value "N e (N c (H a) (H d)) (N g (H f) (H h))"

text ‹------------------------------------------------------------------
Ejercicio 2. Definir la función
preOrden :: "'a arbol ⇒ 'a list"
tal que (preOrden a) es el recorrido pre orden del árbol a. Por
ejemplo,
preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]
---------------------------------------------------------------------›

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

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

text ‹------------------------------------------------------------------
Ejercicio 3. Definir la función
postOrden :: "'a arbol ⇒ 'a list"
tal que (postOrden a) es el recorrido post orden del árbol a. Por
ejemplo,
postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,d,c,f,h,g,e]
---------------------------------------------------------------------›

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

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

text ‹------------------------------------------------------------------
Ejercicio 4. Definir la función
inOrden :: "'a arbol ⇒ 'a list"
tal que (inOrden a) es el recorrido in orden del árbol a. Por
ejemplo,
inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]
---------------------------------------------------------------------›

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

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

text ‹------------------------------------------------------------------
Ejercicio 5. Definir la función
espejo :: "'a arbol ⇒ 'a arbol"
tal que (espejo a) es la imagen especular del árbol a. Por ejemplo,
espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))
---------------------------------------------------------------------›

fun espejo :: "'a arbol ⇒ 'a arbol" where
"espejo (H x) = (H x)"
| "espejo (N x i d) = N x (espejo d) (espejo i)"

value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h))) =
N e (N g (H h) (H f)) (N c (H d) (H a))"

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

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

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

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

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

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

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

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

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

― ‹La demostración estructurada es›
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HI1: "?P i"
assume HI2: "?P d"
show "?P (N x i d)"
proof -
have "preOrden (espejo (N x i d)) =
preOrden (N x (espejo d) (espejo i))" by simp
also have "… = x # (preOrden (espejo d) @ preOrden (espejo i))"
by simp
also have "… = x # (rev (postOrden d) @ rev (postOrden i))"
using HI1 HI2 by simp
also have "… = x # rev (postOrden i @ postOrden d)" by simp
also have "… = rev ((postOrden i) @ (postOrden d) @ [x])" by simp
also have "… = rev (postOrden (N x i d))" by simp
finally show ?thesis .
qed
qed

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

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

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

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

― ‹La demostración estructurada es›
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HI1: "?P i"
assume HI2: "?P d"
show "?P (N x i d)"
proof -
have "postOrden (espejo (N x i d)) =
postOrden (N x (espejo d) (espejo i))" by simp
also have "… = postOrden (espejo d) @ postOrden (espejo i) @ [x]" by simp
also have "… = rev (preOrden d) @ rev (preOrden i) @ [x]"
using HI1 HI2 by simp
also have "… = rev (preOrden i @ preOrden d) @ [x]" by simp
also have "… = rev ([x] @ preOrden i @ preOrden d)" by simp
also have "… = rev (preOrden (N x i d))" by simp
finally show ?thesis .
qed
qed

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

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

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

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

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

― ‹La demostración estructurada es›
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x i d
assume HI1: "?P i"
assume HI2: "?P d"
show "?P (N x i d)"
proof -
have "inOrden (espejo (N x i d)) =
inOrden (N x (espejo d) (espejo i))" by simp
also have "… = inOrden (espejo d) @ [x] @ inOrden (espejo i)" by simp
also have "… = rev (inOrden d) @ [x] @ rev (inOrden i)"
using HI1 HI2 by simp
also have "… = rev (inOrden i @ [x] @ inOrden d)" by simp
also have "… = rev (inOrden (N x i d))" by simp
finally show ?thesis .
qed
qed

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

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

text ‹
---------------------------------------------------------------------
Ejercicio 9. Definir la función
raiz :: "'a arbol ⇒ 'a"
tal que (raiz a) es la raiz del árbol a. Por ejemplo,
raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e
---------------------------------------------------------------------
›

fun raiz :: "'a arbol ⇒ 'a" where
"raiz (H x) = x"
| "raiz (N x i d) = x"

value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h)))" ― ‹= e›

text ‹
---------------------------------------------------------------------
Ejercicio 10. Definir la función
extremo_izquierda :: "'a arbol ⇒ 'a"
tal que (extremo_izquierda a) es el nodo más a la izquierda del árbol
a. Por ejemplo,
extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a
---------------------------------------------------------------------
›

fun extremo_izquierda :: "'a arbol ⇒ 'a" where
"extremo_izquierda (H x) = x"
| "extremo_izquierda (N x i d) = extremo_izquierda i"

value "extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a"

text ‹
---------------------------------------------------------------------
Ejercicio 11. Definir la función
extremo_derecha :: "'a arbol ⇒ 'a"
tal que (extremo_derecha a) es el nodo más a la derecha del árbol
a. Por ejemplo,
extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h
---------------------------------------------------------------------
›

fun extremo_derecha :: "'a arbol ⇒ 'a" where
"extremo_derecha (H x) = x"
| "extremo_derecha (N x i d) = extremo_derecha d"

value "extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h"

text ‹
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar
last (inOrden a) = extremo_derecha a
---------------------------------------------------------------------
›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

text ‹
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
›

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

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

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

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

text ‹
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
›

theorem "hd (inOrden a) = raiz a"
quickcheck
oops

text ‹
Quickcheck found a counterexample:
a = N a1 (H a2) (H a1)

Evaluated terms:
hd (inOrden a) = a2
raiz a = a1
›

text ‹
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
›

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

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

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

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

end

</source>

Rel 13 (sol) - Historial de revisiones

Mjoseh: Protegió «Rel 13 (sol)» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹R13: Recorridos de árboles› theory R13_sol imports Main begin text ‹---------------------------------------------------------…»

← Revisión anterior	Revisión del 09:54 21 may 2020
(Sin diferencias)