theory Relacion_8
imports Main Efficient_Nat Relacion_3
begin
section {* Suma y aplanamiento de listas *}
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
suma :: "nat list ⇒ nat"
tal que (suma xs) es la suma de los elementos de la lista de números
naturales xs. Por ejemplo,
suma [3::nat,2,4] = 9
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
aplana :: "'a list list ⇒ 'a list"
tal que (aplana xss) es la obtenida concatenando los miembros de la
lista de listas "xss". Por ejemplo,
aplana [[2,3], [4,5], [7,9]] = [2,3,4,5,7,9]
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar
length (aplana xs) = suma (map length xs)
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar
suma (xs @ ys) = suma xs + suma ys
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
aplana (xs @ ys) = (aplana xs) @ (aplana ys)
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
aplana (map rev (rev xs)) = rev (aplana xs)
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar
aplana (rev (map rev xs)) = rev (aplana xs)
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar
list_all (list_all P) xs = list_all P (aplana xs)
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar o refutar
aplana (rev xs) = aplana xs
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar
suma (rev xs) = suma xs
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 11. Buscar un predicado P para que se verifique la siguiente
propiedad
list_all P xs ⟶ length xs ≤ suma xs
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar
algunos (algunos P) xs = algunos P (aplana xs)
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 13. Redefinir, usando la función list_all, la función
algunos. Llamar la nueva función algunos2 y demostrar que es
equivalente a algunos.
---------------------------------------------------------------------
*}
end
