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
---------------------------------------------------------------------
*}
primrec suma :: "nat list ⇒ nat" where
"suma [] = 0"
| "suma (x#xs) = x + suma xs"
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]
---------------------------------------------------------------------
*}
primrec aplana :: "'a list list ⇒ 'a list" where
"aplana [] = []"
| "aplana (xs#xss) = xs @ aplana xss"
text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar
length (aplana xs) = suma (map length xs)
---------------------------------------------------------------------
*}
text {*
La igualdad propuesta es verdadera y se puede demostrar
de forma automática como sigue.
*}
lemma "length (aplana xs) = suma (map length xs)"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar
suma (xs @ ys) = suma xs + suma ys
---------------------------------------------------------------------
*}
lemma "suma (xs @ ys) = suma xs + suma ys"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
aplana (xs @ ys) = (aplana xs) @ (aplana ys)
---------------------------------------------------------------------
*}
lemma "aplana (xs @ ys) = (aplana xs) @ (aplana ys)"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
aplana (map rev (rev xs)) = rev (aplana xs)
---------------------------------------------------------------------
*}
text {*
El ejercicio debería de comenzar de la siguiente manera:
*}
lemma "aplana (map rev (rev xs)) = rev (aplana xs)"
proof (induct xs)
show "aplana (map rev (rev [])) = rev (aplana [])" by simp
next
fix b xs
assume HI: "aplana (map rev (rev xs)) = rev (aplana xs)"
thus "aplana (map rev (rev (b # xs))) = rev (aplana (b # xs))"
proof -
oops
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
---------------------------------------------------------------------
*}
lemma "aplana (rev xs) = aplana xs"
quickcheck
oops
text {* El contraejemplo encontrado es xs = [[2], [1, 2]]. Esto tiene
sentido ya que el orden influye en la funcion aplanar *}
text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar
suma (rev xs) = suma xs
---------------------------------------------------------------------
En cambio este ejercicio respecto al anterior tiene sentido que haya
que demostrarlo, ya que el orden en la suma no afecta, por lo que no se
encontrará ningún contra ejemplo.
*}
lemma "suma (rev xs) = suma xs"
proof (induct xs)
show "suma (rev []) = suma []" by simp
next
fix b xs
assume HI: "suma (rev xs) = suma xs"
thus "suma (rev (b # xs)) = suma (b # xs)"
proof -
oops
text{*
En teoria debería de continuarse con una sentencia parecida a la siguiente:
have "suma (rev (b # xs)) = suma (rev [b] @ xs)" by auto
*}
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.
---------------------------------------------------------------------
*}
text {*
La siguiente definición se construye utilizando la palabra reservada
"definition". Aunque se trata de una función recursiva primitiva no
es necesario utilizar la palabra reservada "primrec" porque la función
"list_all" está definida recursivamente o en la cadena de definiciones de
la que depende, hay una función definida recursivamente.
*}
definition algunos2 :: "('a => bool) => 'a list => bool" where
"algunos2 P xs ≡ ¬ list_all (λx. ¬ P x) xs"
end
