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

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

--"jeshorcob"
fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos2 p xs =  foldr (λx. op ∧ (p x)) xs True"

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

--"jeshorcob,javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p [] = True"
 |"algunos p (x#xs) = (p x ∨ todos p xs)"

--"jeshorcob"
fun algunos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos2 p xs =  foldr (λx. op ∨ (p x)) xs True"
 
-- "javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p [] = False"
 |"algunos p (x#xs) = (p x ∨ todos p xs)"
(* Nota. Nos da igual que sea True o False, pero para una proposición
         de más a delante necesitamos que sea False*)

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

--"jeshorcob,javrodviv1" 
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)
  --------------------------------------------------------------------- 
*}

--"jeshorcob"

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

-- "javrodviv1"
 
lemma todo_append:
 "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
  finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))" by auto
qed

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

--"jeshorcob,javrodviv1"
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)
  --------------------------------------------------------------------- 
*}
 
--"jeshorcob"
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) = (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

-- "javrodviv1"
(* es igual que la de jeshorcob pero nos podemos ahorrar 
        una linea de comando*)

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) = ((P a) ∧ todos P (x @ y))" by simp
  also have " ... = ((P a) ∧ todos P x ∧ todos P y)" using HI 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
  --------------------------------------------------------------------- 
*}
 
--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
apply (induct xs)
apply (auto simp add: todos_append)
done

-- "javrodviv1"

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
  --------------------------------------------------------------------- 
*}
 
--"jeshorcob"
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 (simp add: todos_append)
  also have "... = (todos P xs ∧ todos P [x])" using HI by simp
  also have "... = (todos P xs ∧ P x)" by simp
  also have "... = (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

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs" 
proof (induct xs)
  show " todos P (rev []) = todos P []" by simp
next
  fix a xs
  assume HI: "todos P (rev xs) = todos P xs "
  have "todos P (rev (a # xs)) = todos P ((rev xs) @ [a])" by simp
  also have " ... = (todos P (rev xs) ∧ todos P [a])" 
        by (simp add: todos_append)
  also have "... = (todos P xs ∧ todos P [a])" using HI by simp
  finally show " todos P (rev (a # xs)) = todos P (a # xs)" by auto
qed
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar:
    algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
  --------------------------------------------------------------------- 
*}
 
--"jeshorcob"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops

text {* Encuentra el contraejemplo
P = {a⇩1}
Q = {a⇩2}
xs = [a⇩1, a⇩2]
*}

-- "javrodviv1"
(* A mi no me encuentra contraejemplo así que decidí probarlo pero me
     atasque, dejo mi demostración hasta donde estoy atascado*)

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
oops

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

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

-- "javrodviv1"
 
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  show " algunos P (map f []) = algunos (P ∘ f) []" by simp
next 
  fix a xs
  assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have "algunos P (map f (a # xs)) = ((P (f a)) ∨ algunos P (map f xs))" by simp
  also have " ... = (((P ∘ f) a) ∨ algunos (P ∘ f) xs)" using HI by simp
  finally show " algunos P (map f (a # xs)) = algunos (P ∘ f) (a # 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)"
oops
 
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)"
oops
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.1. Demostrar o refutar automáticamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}
 
lemma "algunos P (rev xs) = algunos P xs"
oops
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.2. Demostrar o refutar detalladamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}
 
lemma "algunos P (rev xs) = algunos P xs"
oops
 
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.
  --------------------------------------------------------------------- 
*}
 
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)"
oops
 
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)"
oops
 
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 xs = undefined"
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 13. Expresar la relación existente entre estaEn y algunos. 
  Demostrar dicha relación de forma automática y detallada.
  --------------------------------------------------------------------- 
*}
 
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 xs = undefined"
 
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 xs = undefined"
 
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"
oops
 
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"
oops
 
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)"
oops
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 19. Demostrar o refutar:
    borraDuplicados (rev xs) = rev (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}
 
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
oops
 
end