Razonamiento automático (2010-11) Razonamiento automático (2010-11)

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 {* 
  --------------------------------------------------------------------- 
  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