header {* R11: Plegados de listas y de árboles *}
theory R11
imports Main
begin
section {* Nuevas funciones sobre listas *}
text {*
Nota. En esta relación se usará la función suma tal que (suma xs) es
la suma de los elementos de xs, definida por
*}
fun suma :: "nat list ⇒ nat" where
"suma xs = undefined"
text {*
Las funciones de plegado, foldr y foldl, están definidas en la teoría
List.thy por
foldr :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a list ⇒ 'b ⇒ 'b"
foldr f [] = id
foldr f (x # xs) = f x ∘ foldr f xs
foldl :: "('b ⇒ 'a ⇒ 'b) ⇒ 'b ⇒ 'a list ⇒ 'b"
foldl f a [] = a
foldl f a (x # xs) = foldl f (f a x) xs"
Por ejemplo,
foldr (op +) [a,b,c] d = a + (b + (c + d))
foldl (op +) d [a,b,c] = ((d + a) + b) + c
foldr (op -) [9,4,2] (0::int) = 7
foldl (op -) (0::int) [9,4,2] = -15
*}
value "foldr (op +) [a,b,c] d" -- "= a + (b + (c + d))"
value "foldl (op +) d [a,b,c]" -- "= ((d + a) + b) + c"
value "foldr (op -) [9,4,2] (0::int)" -- "= 7"
value "foldl (op -) (0::int) [9,4,2]" -- "= -15"
text {*
---------------------------------------------------------------------
Ejercicio 1. Demostrar que
suma xs = foldr (op +) xs 0
---------------------------------------------------------------------
*}
lemma suma_foldr: "suma xs = foldr (op +) xs 0"
oops
text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar que
length xs = foldr (λ x res. 1 + res) xs 0
---------------------------------------------------------------------
*}
lemma length_foldr: "length xs = foldr (λ x res. 1 + res) xs 0"
oops
text {*
---------------------------------------------------------------------
Ejercicio 3. La aplicación repetida de foldr y map tiene el
inconveniente de que la lista se recorre varias veces. Sin embargo, es
suficiente recorrerla una vez como se muestra en el siguiente ejemplo,
suma (map (λx. x + 3) xs) = foldr h xs b
Determinar los valores de h y b para que se verifique la igualdad
anterior y demostrarla.
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 4. Generalizar el resultado anterior; es decir determinar
los valores de h y b para que se verifique la igualdad
foldr g (map f xs) a = foldr h xs b
y demostrarla.
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 5. La siguiente función invierte una lista en tiempo lineal
fun inversa_ac :: "['a list, 'a list] ⇒ 'a list" where
"inversa_ac [] ys = ys"
| "inversa_ac (x#xs) ys = (inversa_ac xs (x#ys))"
definition inversa_ac :: "'a list ⇒ 'a list" where
"inversa_ac xs ≡ inversa_ac_aux xs []"
Por ejemplo,
inversa_ac [a,d,b,c] = [c, b, d, a]
Demostrar que inversa_ac se puede definir unsando foldl.
---------------------------------------------------------------------
*}
fun inversa_ac_aux :: "['a list, 'a list] ⇒ 'a list" where
"inversa_ac_aux [] ys = ys"
| "inversa_ac_aux (x#xs) ys = (inversa_ac_aux xs (x#ys))"
definition inversa_ac :: "'a list ⇒ 'a list" where
"inversa_ac xs ≡ inversa_ac_aux xs []"
value "inversa_ac [a,d,b,c]" -- "= [c, b, d, a]"
lemma inversa_ac_aux_foldl:
"inversa_ac_aux xs a = foldl undefined a xs"
oops
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar la siguiente propiedad distributiva de la suma
sobre la concatenación:
suma (xs @ ys) = suma xs + suma ys
---------------------------------------------------------------------
*}
lemma suma_append [simp]:
"suma (xs @ ys) = suma xs + suma ys"
oops
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar una propiedad similar para foldr
foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)
En este caso, hay que restringir el resultado teniendo en cuenta
propiedades algebraicas de f y a.
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 8. Definir, usando foldr, la función
prod :: "nat list ⇒ nat"
tal que (prod xs) es el producto de los elementos de xs. Por ejemplo,
---------------------------------------------------------------------
*}
definition prod :: "nat list ⇒ nat" where
"prod xs ≡ undefined"
value "prod [2::nat,3,5]" -- "= 30"
text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar directamente (es decir, sin inducción) que
prod (xs @ ys) = prod xs * prod ys
---------------------------------------------------------------------
*}
lemma "prod (xs @ ys) = prod xs * prod ys"
oops
section {* Functiones sobre árboles *}
text {*
---------------------------------------------------------------------
Ejercicio 10. Definir el tipo de datos arbol para representar los
árboles binarios que tiene información sólo en los nodos. Por ejemplo,
el árbol
e
/ \
/ \
c g
/ \ / \
· · · ·
se representa por "N (N H c H) e (N H g H)"
---------------------------------------------------------------------
*}
datatype 'a arbol = H | N "'a arbol" "'a" "'a arbol"
value "N (N H c H) e (N H g H)"
text {*
---------------------------------------------------------------------
Ejercicio 11. 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 (N H c H) e (N H g H))
= [e,c,g]
---------------------------------------------------------------------
*}
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden t = undefined"
value "preOrden (N (N H c H) e (N H g H))"
-- "= [e,c,g]"
text {*
---------------------------------------------------------------------
Ejercicio 12. 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 (N H c H) e (N H g H))
= [c,g,e]
---------------------------------------------------------------------
*}
fun postOrden :: "'a arbol ⇒ 'a list" where
"postOrden t = undefined"
value "postOrden (N (N H c H) e (N H g H))"
-- "= [c,g,e]"
text {*
---------------------------------------------------------------------
Ejercicio 13. Definir, usando un acumulador, la función
postOrdenA :: "'a arbol ⇒ 'a list"
tal que (postOrdenA a) es el recorrido post orden del árbol a. Por
ejemplo,
postOrdenA (N (N H c H) e (N H g H))
= [c,g,e]
---------------------------------------------------------------------
*}
fun postOrdenAaux :: "['a arbol, 'a list] ⇒ 'a list" where
"postOrdenAaux t = undefined"
definition postOrdenA :: "'a arbol ⇒ 'a list" where
"postOrdenA a ≡ undefined"
value "postOrdenA (N (N H c H) e (N H g H))"
-- "= [c,g,e]"
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar que
postOrdenAaux a xs = (postOrden a) @ xs
---------------------------------------------------------------------
*}
lemma "postOrdenAaux a xs = (postOrden a) @ xs"
oops
text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la función
foldl_arbol :: "('b => 'a => 'b) ⇒ 'b ⇒ 'a arbol ⇒ 'b" where
tal que (foldl_arbol f b a) es el plegado izquierdo del árbol a con la
operación f y elemento inicial b.
---------------------------------------------------------------------
*}
fun foldl_arbol :: "('b => 'a => 'b) ⇒ 'b ⇒ 'a arbol ⇒ 'b" where
"foldl_arbol f b t = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar que
postOrdenAaux t a = foldl_arbol (λ xs x. Cons x xs) a t
---------------------------------------------------------------------
*}
lemma "postOrdenAaux t a = foldl_arbol (λ xs x. Cons x xs) a t"
oops
text {*
---------------------------------------------------------------------
Ejercicio 17. Definir la función
suma_arbol :: "nat arbol ⇒ nat"
tal que (suma_arbol a) es la suma de los elementos del árbol de
números naturales a.
---------------------------------------------------------------------
*}
fun suma_arbol :: "nat arbol ⇒ nat" where
"suma_arbol t = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 18. Demostrar que
suma_arbol a = suma (preOrden a)"
---------------------------------------------------------------------
*}
lemma "suma_arbol a = suma (preOrden a)"
oops
end
