RA12 Relación 15

header {* R15: Suma y aplanamiento de listas *}

theory R15
imports Main R10
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
  --------------------------------------------------------------------- 
*}

fun suma :: "nat list ⇒ nat" where
  "suma xs = undefined"

value "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]
  --------------------------------------------------------------------- 
*}

fun aplana :: "'a list list ⇒ 'a list" where
  "aplana xs = undefined"

value "aplana [[2::nat,3], [4,5], [7,9]]" -- "= [2,3,4,5,7,9]"

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar o refutar
     length (aplana xs) = suma (map length xs)
  --------------------------------------------------------------------- 
*}

lemma length_aplana:
  "length (aplana xs) = suma (map length xs)"
oops

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 4. Demostrar o refutar
     suma (xs @ ys) = suma xs + suma ys
  --------------------------------------------------------------------- 
*}

lemma suma_append: 
  "suma (xs @ ys) = suma xs + suma ys"
oops

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 5. Demostrar o refutar
     aplana (xs @ ys) = (aplana xs) @ (aplana ys)
  --------------------------------------------------------------------- 
*}

lemma aplana_append: 
  "aplana (xs @ ys) = (aplana xs) @ (aplana ys)"
oops

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar
     aplana (map rev (rev xs)) = rev (aplana xs)
  --------------------------------------------------------------------- 
*}

lemma aplana_map_rev_rev: 
  "aplana (map rev (rev xs)) = rev (aplana xs)"
oops

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar o refutar
     aplana (rev (map rev xs)) = rev (aplana xs)
  --------------------------------------------------------------------- 
*}

lemma aplana_rev_map_rev:
  "aplana (rev (map rev xs)) = rev (aplana xs)"
oops

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar o refutar
     list_all (list_all P) xs = list_all P (aplana xs)
  --------------------------------------------------------------------- 
*}

lemma list_all_list_all:
  "list_all (list_all P) xs = list_all P (aplana xs)"
oops

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 9. Demostrar o refutar
     aplana (rev xs) = aplana xs
  --------------------------------------------------------------------- 
*}

lemma aplana_rev:
  "aplana (rev xs) = aplana xs"
oops

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 10. Demostrar o refutar
     suma (rev xs) = suma xs
  --------------------------------------------------------------------- 
*}

lemma suma_rev:
  "suma (rev xs) = suma xs"
oops

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)
  --------------------------------------------------------------------- 
*}

lemma algunos_algunos: 
  "algunos (algunos P) xs = algunos P (aplana xs)"
oops

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.  
  --------------------------------------------------------------------- 
*}

fun algunos2 :: "('a ⇒ bool) ⇒ ('a list ⇒ bool)" where
  "algunos2 P xs = undefined"

lemma algunos2_algunos: 
  "algunos2 P xs = algunos P xs"
oops

end
De DAO (Demostración asistida por ordenador)
