Jalonso: Texto reemplazado: «lang="isar"» por «lang="isabelle"»

2018-07-15T11:49:42Z

Texto reemplazado: «lang="isar"» por «lang="isabelle"»

Jalonso: Página creada con ' header {* R20: Plegados de listas y de árboles } theory R20 imports Main begin section { Nuevas funciones sobre listas } text { Nota. En esta r...'

2013-05-23T11:48:36Z

Página creada con '<source lang="isar"> header {* R20: Plegados de listas y de árboles *} theory R20 imports Main begin section {* Nuevas funciones sobre listas *} text {* Nota. En esta r...'

Página nueva

<source lang="isar">
header {* R20: Plegados de listas y de árboles *}

theory R20
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
</source>

← Revisión anterior		Revisión del 11:49 15 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R20: Plegados de listas y de árboles *}		header {* R20: Plegados de listas y de árboles *}

RA12 Relación 20 - Historial de revisiones

Jalonso: Texto reemplazado: «lang="isar"» por «lang="isabelle"»

Jalonso: Página creada con ' header {* R20: Plegados de listas y de árboles *} theory R20 imports Main begin section {* Nuevas funciones sobre listas *} text {* Nota. En esta r...'

Jalonso: Página creada con ' header {* R20: Plegados de listas y de árboles } theory R20 imports Main begin section { Nuevas funciones sobre listas } text { Nota. En esta r...'