Rel 5

header {* R5: Cuantificadores sobre listas *}

theory R5
imports Main 
begin

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 1. 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. 
  --------------------------------------------------------------------- 
*}

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


text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. 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. 
  --------------------------------------------------------------------- 
*}

fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p [] = False"
  |"algunos p (x#xs) = (p x ∨ algunos p xs)"
   

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.1. Demostrar o refutar automáticamente 
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}

lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by(induct xs) auto


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

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 HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (a#xs) = ((P a ∧ Q a) ∧ todos (λx. P x ∧ Q x)xs)" by simp
also have "... = (P a ∧ Q a ∧ todos P xs ∧ todos Q xs)" using HI by simp
also have "... = (P a ∧ todos P xs ∧ Q a ∧ todos Q xs)" by arith
also have "... = (todos P (a#xs) ∧ todos Q (a#xs))" by simp
finally show "todos (λx. P x ∧ Q x) (a#xs) = (todos P (a#xs) ∧ todos Q (a#xs))" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.1. Demostrar o refutar automáticamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}

lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto

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

lemma todos_append:
  "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
assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a#x) @ y) = todos P (a#(x@ y))" by simp
also have "... = (P a ∧ todos P (x@y))" by simp
also have "... = (P a ∧ todos P x ∧ todos P y)" using HI by simp
also have "... = (todos P (a#x) ∧ todos P y)" by simp
finally show "todos P ((a#x) @ y) = (todos P (a#x) ∧ todos P y)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.1. Demostrar o refutar automáticamente 
     todos P (rev xs) = todos P xs
  --------------------------------------------------------------------- 
*}

lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)


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

lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix x xs
assume HI:"todos P (rev xs) = todos P xs"
have "todos P (rev (x#xs)) = todos P (rev xs @ [x])" by simp
also have "... = (todos P (rev xs) ∧ todos P [x])" by (rule todos_append)
also have "... = (todos P xs ∧ todos P [x])" using HI by simp
also have "... = (todos P [x] ∧ todos P xs)" by arith
also have "... = todos P (x#xs)" by simp
finally show "todos P (rev (x#xs)) = todos P (x#xs)" by simp
qed


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

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

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7.1. Demostrar o refutar automáticamente 
     algunos P (map f xs) = algunos (P ∘ f) xs
  --------------------------------------------------------------------- 
*}

lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto


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

lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
show "algunos P (map f []) = algunos (P o f) []" by simp
next
fix x xs
assume HI: "algunos P (map f xs) = algunos (P o f) xs"
have "algunos P (map f (x#xs)) = algunos P (f x # map f xs)" by simp
also have "... =(P (f x) ∨ algunos P (map f xs))" by simp
also have "... = (P(f x) ∨ algunos (P o f) xs)" using HI by simp
also have "... = algunos (P o f) (x#xs)" by simp
finally show "algunos P (map f (x#xs)) = algunos (P o f) (x#xs)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8.1. Demostrar o refutar automáticamente 
     algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
  --------------------------------------------------------------------- 
*}

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs) auto


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

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 x xs
assume HI:"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
have "algunos P ((x#xs) @ ys) = algunos P (x#(xs@ys))" by simp
also have "... = (P x ∨ algunos P (xs@ys))" by simp
also have "... = (P x ∨ algunos P xs ∨ algunos P ys)" using HI by simp
also have "... = (algunos P (x#xs)∨ algunos P ys)" by simp
finally show "algunos P ((x#xs) @ ys) = (algunos P (x#xs) ∨ algunos P ys)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.1. Demostrar o refutar automáticamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append)


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

lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix x xs
assume HI:"algunos P (rev xs) = algunos P xs"
have "algunos P (rev (x#xs)) = algunos P (rev xs @ [x])" by simp
also have "... = (algunos P (rev xs) ∨ algunos P [x])" by (rule algunos_append)
also have "... = (algunos P xs ∨ algunos P [x])" using HI by simp
also have "... = (algunos P [x] ∨ algunos P xs)" by arith
also have "... = algunos P (x#xs)" by simp
finally show "algunos P (rev (x#xs)) = algunos P (x#xs)" by simp
qed 


text {*
  --------------------------------------------------------------------- 
  Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la 
  siguiente ecuación:
     algunos (λx. P x ∨ Q x) xs = Z
  y demostrar la equivalencia de forma automática y detallada.
  --------------------------------------------------------------------- 
*}

lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
by(induct xs)auto


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 HI: "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
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 HI by simp
also have "... = (P a ∨ Q a ∨ algunos P xs ∨ algunos Q xs)" by simp
also have "... = (algunos P (a#xs) ∨ algunos Q (a#xs))" by auto
finally show "algunos (λx. P x ∨ Q x) (a#xs)=(algunos P (a#xs) ∨ algunos Q (a#xs))" by simp
qed


text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.1. Demostrar o refutar automáticamente
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by(induct xs)auto

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

lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof(induct xs)
show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
fix a xs
assume HI: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
have "algunos P (a#xs) = (P a ∨ algunos P xs)" by simp
also have "... = (P a ∨ (¬ todos (λx. (¬ P x)) xs ))" using HI by simp
also have "... = (¬ todos (λx. (¬ P x)) (a#xs))" by simp
finally show "algunos P (a#xs) = (¬ todos (λx. (¬ P x)) (a#xs))" by simp
qed
     
text {*
  --------------------------------------------------------------------- 
  Ejercicio 12. 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
  --------------------------------------------------------------------- 
*}

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

text {*
  --------------------------------------------------------------------- 
  Ejercicio 13. Expresar la relación existente entre estaEn y algunos. 
  Demostrar dicha relación de forma automática y detallada.
  --------------------------------------------------------------------- 
*}

lemma "algunos (λx. x=a) xs = estaEn a xs"
by(induct xs)auto


lemma "algunos (λx. x=a) xs = estaEn a xs"
proof (induct xs)
 show "algunos (λx. x=a) [] = estaEn a []" by simp
next 
fix y xs
assume HI: "algunos (λx. x=a) xs = estaEn a xs"
have "algunos (λx. x=a) (y#xs) = (y=a ∨ algunos (λx. x=a) xs)" by simp
also have "... = (y=a ∨ estaEn a xs)" using HI by simp
also have "... = estaEn a (y#xs)" by auto
finally show "algunos (λx. x=a) (y#xs) = estaEn a (y#xs)" by simp
qed


text {* 
  --------------------------------------------------------------------- 
  Ejercicio 14. 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
  --------------------------------------------------------------------- 
*}

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


text {* 
  --------------------------------------------------------------------- 
  Ejercicio 15. 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. 
  --------------------------------------------------------------------- 
*}

fun borraDuplicados :: "'a list ⇒ 'a list" where
   "borraDuplicados [] = []"
 | "borraDuplicados (x#xs) = (case estaEn x xs of True => borraDuplicados xs 
                                                | False => x#borraDuplicados xs)"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 16.1. Demostrar o refutar automáticamente
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}

lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
oops

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

lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
proof(induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix x xs
assume HI:"length (borraDuplicados xs) ≤ length xs"
show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"
proof(cases)
assume HI1:"estaEn x xs"
have "length (borraDuplicados (x # xs)) = length (borraDuplicados xs)" using HI1 by simp
also have "... ≤ length xs" using HI by simp
also have "... ≤ 1+ length xs" by simp
finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)" by simp
next
assume HI2:"¬estaEn x xs"
have "length (borraDuplicados (x # xs)) = 1+length (borraDuplicados xs)" using HI2 by simp
also have "... ≤ 1+ length xs" using HI by simp
finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)" by simp
qed
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 17.1. Demostrar o refutar automáticamente 
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
*}

lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
oops

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

lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
proof(induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []" by  simp
next
fix x xs
assume HI:"estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#xs)"
proof(cases)
assume HI1: "estaEn x xs"
have "estaEn a (borraDuplicados (x#xs)) = estaEn a (borraDuplicados xs)" using HI1 by simp
also have "... = estaEn a xs" using HI by simp
finally show "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#xs)" by auto
next
assume HI2: "¬(estaEn x xs)"
have "estaEn a (borraDuplicados (x#xs)) = estaEn a (x # borraDuplicados xs)" using HI2 by simp
also have "... = (a = x ∨ estaEn a (borraDuplicados xs))" by simp
also have "... = (a = x ∨ estaEn a xs)" using HI by simp
also have "... = estaEn a (x#xs)" by simp
finally show "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#xs)" by simp
qed
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 18.1. Demostrar o refutar automáticamente 
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

lemma "sinDuplicados (borraDuplicados xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 18.2. Demostrar o refutar detalladamente
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

lemma sinDuplicados_borraDuplicados:
  "sinDuplicados (borraDuplicados xs)"
proof(induct xs)
show "sinDuplicados (borraDuplicados [])" by simp
next
fix x xs
assume HI: "sinDuplicados (borraDuplicados xs)"
show "sinDuplicados (borraDuplicados (x#xs))"
proof(cases)
assume HI1: "estaEn x xs"
have "sinDuplicados (borraDuplicados (x#xs)) = sinDuplicados (borraDuplicados xs)"using HI1 by simp
also have "... = True" using HI by simp
finally show "sinDuplicados (borraDuplicados (x#xs))" using HI by simp
next
assume HI2:"¬estaEn x xs"
have "sinDuplicados (borraDuplicados (x#xs)) = sinDuplicados(x#borraDuplicados xs)" using HI2 by simp
also have "... = (¬estaEn x (borraDuplicados xs) ∧ sinDuplicados(borraDuplicados xs))" by auto
also have "... = (¬estaEn x (borraDuplicados xs) ∧ True)" using HI by simp
also have "... = (¬estaEn x (borraDuplicados xs))" by simp
also have "...= (¬estaEn x xs)" by (simp add:estaEn_borraD)
also have "... = True" using HI2 by simp
finally show "sinDuplicados(borraDuplicados (x#xs))" by simp
qed
qed


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

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

text{* Contraejemplo: xs = [a⇩1, a⇩2, a⇩1]

  borraDuplicados (rev xs) = [a⇩2, a⇩1]
  rev (borraDuplicados xs) = [a⇩1, a⇩2]
*}

end