Relación 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 @.
  --------------------------------------------------------------------- 
*}

primrec snoc :: "'a list ⇒ 'a ⇒ 'a list" where
  "snoc [] y = [y]"
| "snoc (x#xs) y = x#(snoc xs y)"

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]"
by (induct xs) auto

-- "La demostración estructurada del lema es"
lemma snoc_append: "snoc xs a = xs @ [a]"
proof (induct xs)
  show "snoc [] a = [] @ [a]" by simp
next 
  fix b xs 
  assume HI: "snoc xs a = xs @ [a]"
  thus "snoc (b # xs) a = (b # xs) @ [a]"
  proof -
    have "snoc (b # xs) a = b#(snoc xs a)" by simp
    also have "... =  b#(xs @ [a])" using HI by simp
    also have "... = (b#xs) @ [a]" by simp
    finally show ?thesis .
  qed
qed

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"
by (simp add:snoc_append)

-- "La demostración estructurada del teorema es"
theorem rev_cons: "rev (x # xs) = snoc (rev xs) x"
proof -
 have "rev(x#xs)=(rev xs) @ [x]" by simp 
 also have "... = snoc (rev xs) x" by (simp add:snoc_append)
 finally show ?thesis .  
qed





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


primrec todos :: "('a ⇒ bool) ⇒ ('a list ⇒ bool)" where
   "todos P [] = True"
  |"todos P (x#xs) = (P x ∧ todos P xs)"


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


primrec algunos :: "('a => bool) => 'a list => bool" where
  "algunos P [] = False"
  | "algunos P (x#xs) = (P x ∨ algunos P xs)"


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)"
by (induct xs) auto



-- "La demostración estructurada es"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
  show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
  fix a xs
  assume 1:  "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
  thus "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))"
  proof -
    have 2: "todos (λx. P x ∧ Q x) (a # xs) = ((P a ∧ Q a) ∧ (todos (λx. P x ∧ Q x) xs))" by simp
    also have 3: "... = ((P a ∧ Q a) ∧ (todos P xs ∧ todos Q xs))" using 1 by simp
    also have 4: "... = ((P a ∧ todos P xs) ∧ (Q a ∧ todos Q xs))" by blast
    also have 5: "... = ((todos P (a # xs) ∧ todos Q (a # xs)))" by simp
    finally show ?thesis .
  qed
qed




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)"
by (induct x) auto



-- "La demostración estructurada es"
lemma todos_append [simp]: 
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
  show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
  fix a x y
  assume 1: "todos P (x @ y) = (todos P x ∧ todos P y)"
  thus "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)"
  proof -
    have "(todos P ((a # x) @ y)) = (P a ∧ todos P (x @ y))" by simp
    also have "... = (P a ∧ todos P x ∧ todos P y)" using 1 by simp
    also have "... = (todos P (a #x) ∧ todos P y)" by simp
    finally show ?thesis .
  qed
qed



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"
by (induct xs) auto



-- "La demostración estructurada es"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
  show "todos P (rev []) = todos P []" by simp
next
  fix a xs
  assume 1: "todos P (rev xs) = todos P xs"
  thus "todos P (rev (a # xs)) = todos P (a # xs)"
  proof -
    have "todos P (rev (a # xs)) = todos P (rev (xs) @ [a])" by simp
    also have "... = (todos P (rev (xs)) ∧ todos P [a])" by simp
    also have "... = (todos P xs ∧ todos P [a])" using 1 by simp
    also have "... = (todos P [a] ∧ todos P xs)" by blast
    also have "... = todos P ([a] @ xs)" by simp
    also have "... = todos P (a # xs)" by simp
    finally show ?thesis .
  qed
qed




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 que encuentra Quickcheck es (retocando su codificación
para que no haya problemas al exportarlo a Isabelle):
  P = {a1}
  Q = {a2}
  xs = [a1, a2]
El contraejemplo que encuentra Nitpick se aparta del anterior en algunos
detalles:
  P = {a1, a2}
  Q = {a3}
  xs = [a3, a2]
Refute sin embargo agota el tiempo sin llegar a encontrar un contraejemplo.
*}

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"
by (induct xs) auto



-- "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)"
by (induct xs) auto


-- "La demostración estructurada es"
lemma algunos_append: 
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
  show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)" by simp
next
  fix a xs
  assume 1: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
  thus "algunos P ((a # xs) @ ys) = (algunos P (a # xs) ∨ algunos P ys)"
  proof -
    have "algunos P ((a # xs) @ ys) = (P a ∨ algunos P (xs @ ys))" by simp
    also have "... = (P a ∨ (algunos P xs ∨ algunos P ys))" using 1 by simp
    also have "... = ((P a ∨ algunos P xs) ∨ algunos P ys)" by blast
    also have "... = (algunos P (a#xs) ∨ algunos P ys)" by simp
    finally show ?thesis .
  qed
qed



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"
by (induct xs) (auto simp add:algunos_append)



-- "La demostración estructurada es"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  show " algunos P (rev []) = algunos P []" by simp
next
  fix a xs
  assume 1: "algunos P (rev xs) = algunos P xs"
  thus "algunos P (rev (a # xs)) = algunos P (a # xs)"
  proof -
    have "algunos P (rev (a # xs)) = algunos P (rev (xs) @ [a])" by simp
    also have "... = (algunos P (rev (xs)) ∨ algunos P ([a]))" by (simp add:algunos_append)
    also have "... = (algunos P xs ∨ algunos P [a])" using 1 by simp
    also have "... = (algunos P [a] ∨ algunos P xs)" by blast
    also have "... = algunos P (a # xs)" by simp
    finally show ?thesis .
  qed
qed




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)"
by (induct xs) auto


-- "De forma estructurada"
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
proof (induct xs)
  show "algunos (λx. P x ∨ Q x) [] = (algunos P [] ∨ algunos Q [])" by simp
next
  fix a xs
  assume 1: "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
  thus "algunos (λx. P x ∨ Q x) (a # xs) = (algunos P (a # xs) ∨ algunos Q (a # xs))"
  proof -
    have "algunos (λx. P x ∨ Q x) (a # xs) = ((P a ∨ Q a) ∨ (algunos (λx. P x ∨ Q x) xs))" by simp
    also have "... = ((P a ∨ Q a) ∨ (algunos P xs ∨ algunos Q xs))" using 1 by auto
    also have "... = ((P a ∨ algunos P xs) ∨ (Q a ∨ algunos Q xs))" by auto
    also have "... = (algunos P (a # xs) ∨ algunos Q (a # xs))" by auto
    finally show ?thesis by auto
  qed
qed



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)"
by (induct xs) auto

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


primrec estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x []     = False"
| "estaEn x (a#xs) = (x=a ∨ estaEn x xs)"  


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


text {*
  Solución: La relación es:
"estaEn x xs ⟶ algunos (λx. True ) xs".
  En efecto,  
*}


lemma "estaEn x xs ⟶ algunos (λx. True ) xs"
by (induct xs arbitrary: x) auto


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



primrec sinDuplicados :: "'a list ⇒ bool" where
  "sinDuplicados [] = True"
| "sinDuplicados (a#xs) = ((¬ (estaEn a xs)) ∧ sinDuplicados xs)"



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



primrec borraDuplicados :: "'a list ⇒ 'a list" where
  "borraDuplicados []     = []"
| "borraDuplicados (a#xs) = 
  (if estaEn a xs 
   then borraDuplicados xs 
   else (a#borraDuplicados xs))"

text {* 
  El tipo correspondiente al conjunto imagen de la función definida
  no coincide con el indicado en la declaración de tipos del enunciado,
  dado que en él aparece erróneamente la salida de tipo bool, mientras
  que del resto del texto se deduce que la salida es una lista de
  elementos de tipo 'a. 
*}


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


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



-- "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"
by (induct xs) auto


-- "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)"
by (induct xs arbitrary: x) (auto simp add: estaEn_borraDuplicados_auto)



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


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


text {*
La igualdad propuesta es falsa.
El contraejemplo que encuentra Quickcheck es (retocando su
codificación para que no haya problemas al exportarlo a Isabelle):
xs = [a1, a2, a1].
En este caso Nitpick encuentra el mismo contraejemplo.
Por su parte, Refute de nuevo no encuentra contraejemplo alguno.
*}

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

end