Rel 3

header {* 3ª relación de ejercicios *}

theory Relacion_3
imports Main 
begin

section {* Cons inverso *}

text {*
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir recursivamente la función 
     snoc :: "'a list ⇒ 'a ⇒ 'a list"
  tal que (snoc xs a) es la lista obtenida al añadir el elemento a al
  final de la lista xs. Por ejemplo, 
     value "snoc [2,5] (3::int)" == [2,5,3]

  Nota: No usar @.
  --------------------------------------------------------------------- 
*}

text {*
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}

-- "La demostración automática del lema es"
lemma "snoc xs a = xs @ [a]"
oops

-- "La demostración estructurada del lema es"
lemma snoc_append: "snoc xs a = xs @ [a]"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar el siguiente teorema 
     rev (x # xs) = snoc (rev xs) x"
  --------------------------------------------------------------------- 
*}

-- "La demostración automática del teorema es"
theorem rev_cons_auto: "rev (x # xs) = snoc (rev xs) x"
oops

-- "La demostración estructurada del teorema es"
theorem rev_cons: "rev (x # xs) = snoc (rev xs) x"
oops

section {* Cuantificadores sobre listas *}

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 4. Definir la función 
     todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (todos p xs) se verifica si todos los elementos de la lista 
  xs cumplen la propiedad p. Por ejemplo, se verifica 
     todos (λx. 1<length x) [[2,1,4],[1,3]]
     ¬ todos (λx. 1<length x) [[2,1,4],[3]]

  Nota: La función todos es equivalente a la predefinida list_all. 
  --------------------------------------------------------------------- 
*}

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 5. Definir la función 
     algunos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (algunos p xs) se verifica si algunos elementos de la lista 
  xs cumplen la propiedad p. Por ejemplo, se verifica 
     algunos (λx. 1<length x) [[2,1,4],[3]]
     ¬ algunos (λx. 1<length x) [[],[3]]"

  Nota: La función algunos es equivalente a la predefinida list_ex. 
  --------------------------------------------------------------------- 
*}

text {*
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar: 
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
oops

-- "La demostración estructurada es"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar o refutar: 
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
oops

-- "La demostración estructurada es"
lemma todos_append [simp]: 
  "todos P (x @ y) = (todos P x ∧ todos P y)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar o refutar: 
     todos P (rev xs) = todos P xs
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma "todos P (rev xs) = todos P xs"
oops

-- "La demostración estructurada es"
lemma "todos P (rev xs) = todos P xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9. Demostrar o refutar:
    algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
  --------------------------------------------------------------------- 
*}

-- "Se busca un contraejemplo con nitpick"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
oops

text {*
  El contraejemplo encontrado es
*}

text {*
  --------------------------------------------------------------------- 
  Ejercicio 10. Demostrar o refutar: 
     algunos P (map f xs) = algunos (P ∘ f) xs
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma "algunos P (map f xs) = algunos (P o f) xs"
oops

-- "La demostración estructurada es"
lemma "algunos P (map f xs) = algunos (P ∘ f) xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 11. Demostrar o refutar: 
     algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

-- "La demostración estructurada es"
lemma algunos_append: 
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 12. Demostrar o refutar: 
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma "algunos P (rev xs) = algunos P xs"
oops

-- "La demostración estructurada es"
lemma "algunos P (rev xs) = algunos P xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 13. Encontrar un término no trivial Z tal que sea cierta la 
  siguiente ecuación:
     algunos (λx. P x ∨ Q x) xs = Z
  --------------------------------------------------------------------- 
*}

text {*
  Solución: La ecuación se verifica eligiendo como Z el término  
     algunos P xs ∨ algunos Q xs
  En efecto,
*}

lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
oops

-- "De forma estructurada"
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 14. Demostrar o refutar:
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops
     
-- "La demostración estructurada es"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 15. Definir la funcion primitiva recursiva 
     estaEn :: 'a ⇒ 'a list ⇒ bool
  tal que (estaEn x xs) se verifica si el elemento x está en la lista
  xs. Por ejemplo, 
     estaEn (2::nat) [3,2,4] = True
     estaEn (1::nat) [3,2,4] = False
  --------------------------------------------------------------------- 
*}

text {*
  --------------------------------------------------------------------- 
  Ejercicio 16. Expresar la relación existente entre estaEn y algunos. 
  --------------------------------------------------------------------- 
*}

text {*
  Solución: La relación es 

  En efecto,  
*}

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 17. Definir la función primitiva recursiva 
     sinDuplicados :: 'a list ⇒ bool
  tal que (sinDuplicados xs) se verifica si la lista xs no contiene
  duplicados. Por ejemplo,  
     sinDuplicados [1::nat,4,2]   = True
     sinDuplicados [1::nat,4,2,4] = False
  --------------------------------------------------------------------- 
*}

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 18. Definir la función primitiva recursiva 
     borraDuplicados :: 'a list ⇒ bool
  tal que (borraDuplicados xs) es la lista obtenida eliminando los
  elementos duplicados de la lista xs. Por ejemplo, 
     borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

  Nota: La función borraDuplicados es equivalente a la predefinida remdups. 
  --------------------------------------------------------------------- 
*}

text {*
  --------------------------------------------------------------------- 
  Ejercicio 19. Demostrar o refutar:
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma "length (borraDuplicados xs) ≤ length xs"
oops

-- "La demostración estructurada es"
lemma length_borraDuplicados: 
  "length (borraDuplicados xs) ≤ length xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 20. Demostrar o refutar: 
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
lemma estaEn_borraDuplicados_auto: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
oops

-- "La demostración estructurada es"
lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 21. Demostrar o refutar: 
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

-- "La demostración automática"
lemma "sinDuplicados (borraDuplicados xs)"
oops

-- "La demostración estructurada es"
lemma sinDuplicados_borraDuplicados:
  "sinDuplicados (borraDuplicados xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 22. Demostrar o refutar:
    borraDuplicados (rev xs) = rev (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
oops

end