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,juacorvic"
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"

--"emimarriv"
fun todos3 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos3 p [] = True"
| "todos3 p (x#xs) = (if p x then (todos3 p xs) else False)"
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. 
  --------------------------------------------------------------------- 
*}

(* Errata. Debe ser False el caso base seguro porque si no,
 la función devuelve siempre True*)
--"jeshorcob,javrodviv1,juacorvic"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p [] = False"
 |"algunos p (x#xs) = (p x ∨ algunos p xs)"

--"jeshorcob"
fun algunos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos2 p xs =  foldr (λx. op ∨ (p x)) xs False"

value "algunos (λx. x>10) [3::int,2]"
value "algunos2 (λx. x>10) [3::int,2]"
 
-- "javrodviv1"
fun algunos3 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos3 p [] = False"
 |"algunos3 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*)
(* jeshorcob: Debe ser False y la función tiene una errata en
la segunda linea porque la recursión la debe hacer sobre la función 
algunos3  en lugar de todos *)

--"emimarriv"
fun algunos4  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos4 p [] =False"
| "algunos4 p (x#xs) = (if p x then True else (algunos4 p xs))"

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

-- "juacorvic" (*Muy parecida a la solución anterior*)
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 ∧ Q x ∧ todos P xs ∧ todos Q xs)" by simp
  also   have "... = ((P x ∧ todos P xs) ∧ (Q x ∧ todos Q xs))" by arith
  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

--"emimarriv"

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) =((todos (λx. P x ∧ Q x) [x]) ∧ (todos (λx. P x ∧ Q x) xs))" by simp
  also have "... = ((todos P [x] ∧ todos Q [x]) ∧ (todos P xs ∧ todos Q xs))" using HI by simp
  also have "... = ((todos P [x] ∧ todos P xs) ∧ (todos Q [x] ∧ todos Q xs))" by simp
  also have "... = (todos P (x#xs) ∧ todos Q (x#xs))" by simp (* emimarriv: Esta linea puede suprimirse, pero la dejo porque se sigue
                                                                            mejor el proceso*)
  finally show "todos (λx. P x ∧ Q x) (x#xs) = (todos P (x#xs) ∧ todos Q (x#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,juacorvic"
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, emimarriv"
(* es igual que la de jeshorcob pero nos podemos ahorrar 
        una linea de comando*)

lemma todos_append2:
  "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
 
-- "juacorvic" 
(* es igual que las anteriores pero salió con mayor nivel de detalle *)

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

-- "javrodviv1, juacorvic"

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, juacorvic"
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, emimarriv"

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

(*Pedrosrei: No sé cómo has conseguido el contraejemplo,
  probablemente algún fallo en los paréntesis, ya que la propiedad 
  resulta cierta como expongo abajo:
*)
(* jeshorcob: el contraejemplo existe. Fijate en lo siguiente: *)
fun p1 :: "int ⇒ bool" where
  "p1 x = (x=3)"
fun q1 :: "int ⇒ bool" where
  "q1 x = (x=2)"
value "algunos (λx. p1 x ∧ q1 x) [3,2]" -- "= False 
  (porque ningún elemento de la lista cumple a la vez p1 y q1)"
value "(algunos p1 [3,2] ∧ algunos q1 [3,2])" -- "= True 
  (porque cada elemento de la lista cumple una sola de p1 y q1)"
(*Por tanto:*)
value "algunos (λx. p1 x ∧ q1 x) [3,2] = 
(algunos p1 [3,2] ∧ algunos q1 [3,2])" -- "= False"
(*Esta es una instancia del contraejemplo que encuentra QuickCheck*)


lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
by (metis (full_types) algunos.simps(1) algunos.simps(2) list_nonempty_induct)

(*Al cambiar la definición de algunos para que coincida con list_ex es cierto el 
contraejemplo de Jesús
*)

-- "juacorvic"
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
 (* Ya no podemos seguir más ya que no se cuemple: 
      also have "... =  ((P a ∨ algunos P xs) ∧ (Q a ∨ algunos Q xs))   
   Tenemos que buscar un contraejemplo:
 *)
oops


--"jeshorcob, emimarriv, juacorvic"
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]
*}

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

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, jeshorcob, emimarriv, juacorvic"
 
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)
  --------------------------------------------------------------------- 
*}
(*Pedrosrei: Pongo la automática que parece se os resiste.*) 

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (metis algunos.simps(1) algunos.simps(2) list_nonempty_induct)

(*Si corregís la definición de algunos sería: *)

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

(*jeshorcob: Pedro, a la tuya no sé que le pasa que no me la coge bien. 
Dejo la mía *)

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

-- "javrodviv1, jeshorcob, emimarriv"
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 HI:"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
  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 HI by simp
  finally show "algunos P ((a # xs) @ ys) = 
         (algunos P (a # xs) ∨ algunos P ys)" by simp
qed
 
(*Igual que anterior, cambia uso de paréntesis y un paso más*)
-- "juacorvic" 
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 HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
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 HI by simp
also have "... = (algunos P (a # xs) ∨ algunos P ys)" by simp
finally show "algunos P ((a # xs) @ ys) = (algunos P (a # xs) ∨ algunos P ys)" by simp
qed


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

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

-- "javrodviv1, jeshorcob"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  show "algunos P (rev []) = algunos P []" by simp
next
  fix a xs
  assume HI:"algunos P (rev xs) = algunos P xs"
  have "algunos P (rev (a # xs)) = algunos P (rev xs @[a])" by simp
  also have "... = (algunos P xs ∨ (P a))" using HI using algunos_append by auto
  finally show " algunos P (rev (a # xs)) = algunos P (a # xs)" by auto
qed

-- "emimarriv"
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) ∨ (P x))" by (auto simp add: algunos_append)
  also have "... = (algunos P xs ∨ (P x))" using HI by simp
  finally show " algunos P (rev (x#xs)) = algunos P (x#xs)" by auto
qed

-- "juacorvic"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next 
fix a xs
assume HI: "algunos P (rev xs) = algunos P xs"
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 HI by simp
also have "... = (algunos P [a] ∨ algunos P xs)" by arith
also have "... =  algunos P (a # xs)" by simp
finally show "algunos P (rev (a # xs)) = algunos P (a # 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.
  --------------------------------------------------------------------- 
*}

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

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

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

Por ejemplo P= esVacio, xs = []. P es la propiedad de ser vacío
con nuestra construcción de algunos es cierto "algunos esVacio []"
Sin embargo, todos (λx. (¬ esVacio {})) [] es lo mismo que 
todos _ [] = True, por lo que ¬(todos (λx. (¬ esVacio {})) []) = False,
siendo falsa nuestra definición. Podemos coger de todas maneras la propiedad
que queramos y sigue siendo falso porque 
(algunos _ [] True) ∧ (¬(todos _ [])= False)
 *)
lemma 
shows "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
quickcheck
oops
(*Al corregir la definición de "algunos" deja de ser cierto lo dicho y 
correcto lo de abajo.
*)

(*jeshorcob: está claro que el fallo en todo era la definición esa*)

-- "javrodviv1, jeshorcob, juacorvic"
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)
  --------------------------------------------------------------------- 
*}
 
-- "javrodviv1, jeshorcob"
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
  finally show "algunos P (a # xs) =(¬ todos (λx. ¬ P x) (a#xs))" by auto
qed

-- "juacorvic"
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 
(* Este paso lo he puesto por inercia de otras demostraciones
pero realmente no veo como hacerlo más detallado *)
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
  --------------------------------------------------------------------- 
*}

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


-- "juacorvic" 
(*Si cambiamos el orden de la igualdad no tenemos que
utilizar auto en la demostración*)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x [] = False"
| "estaEn x (a#xs) = (a = x ∨ estaEn x xs)"


value "estaEn (2::nat) [3,2,4]" --"= True"
value "estaEn (1::nat) [3,2,4]" --"= False"
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 13. Expresar la relación existente entre estaEn y algunos. 
  Demostrar dicha relación de forma automática y detallada.
  --------------------------------------------------------------------- 
*}

--"jeshorcob,juacorvic"
lemma "algunos (λx. x=y) xs = estaEn y xs"
by (induct xs) auto

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

-- "juacorvic"
lemma "algunos (λx. x=y) xs = estaEn y xs"
proof (induct xs)
show "algunos (λx. x = y) [] = estaEn y []" by simp
  next
  fix a xs
  assume HI: "algunos (λx. x = y) xs = estaEn y xs"
have "algunos (λx. x = y) (a # xs) =  (a = y ∨ algunos (λx. x = y) xs)" by simp
also have "... = (a = y ∨ estaEn y xs)" using HI by simp 
also have "... = (estaEn y (a # xs))" by simp
finally show "algunos (λx. x = y) (a # xs) = estaEn y (a # 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
  --------------------------------------------------------------------- 
*}
 
-- "javrodviv1"
fun sinDuplicados :: "'a list ⇒ bool" where
  "sinDuplicados [] = False"
| "sinDuplicados (x#xs) = (estaEn x xs ∨ sinDuplicados xs)"

(*jeshorcob: Esta definición no es correcta. Véanse:*)
value "sinDuplicados [1::nat,4,2]" -- "= True"
value "sinDuplicados [1::nat,4,2,4]" -- "= False"

--"jeshorcob, juacorvic"
fun sinDuplicados2 :: "'a list ⇒ bool" where
  "sinDuplicados2 [] = True"
 |"sinDuplicados2 (x#xs) = (¬(estaEn x xs) ∧ sinDuplicados2 xs)"

value "sinDuplicados2 [1::nat,4,2]" -- "= True"
value "sinDuplicados2 [1::nat,4,2,4]" -- "= False"

--"emimarriv"
fun sinDuplicados3 :: "'a list ⇒ bool" where
  "sinDuplicados3 [] = True"
| "sinDuplicados3 (x#xs) = (if estaEn x xs then False else sinDuplicados3 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. 
  --------------------------------------------------------------------- 
*}

-- "javrodviv1, jeshorcob, juacorvic" 
fun borraDuplicados :: "'a list ⇒ 'a list" where
  "borraDuplicados [] = []"
| "borraDuplicados (x#xs) = (if estaEn x xs then borraDuplicados xs else (x#(borraDuplicados xs)))"
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 16.1. Demostrar o refutar automáticamente
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}
 
-- "javrodviv1, jeshorcob, juacorvic" 
lemma "length (borraDuplicados xs) ≤ length xs"
by (induct xs) auto
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 16.2. Demostrar o refutar detalladamente
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}
 
-- "javrodviv1, jeshorcob" 
lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
  show "length (borraDuplicados []) ≤ length []" by simp
next
  fix a xs
  assume HI:"length (borraDuplicados xs) ≤ length xs"
  have "length (borraDuplicados (a#xs))≤length (a#borraDuplicados xs)" by simp
  also have "... = 1+ length (borraDuplicados xs)" by simp
  also have "... ≤ 1+ length xs" using HI by simp
  finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)" by simp
qed
 
-- "juacorvic"
(*Igual pero con 1 paso más*)
lemma length_borraDuplicados: 
   "length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
  show "length (borraDuplicados []) ≤ length []" by simp
next
  fix a xs 
  assume HI: "length (borraDuplicados xs) ≤ length xs"
  have "length (borraDuplicados (a # xs)) ≤ length (a # (borraDuplicados xs))" by simp
  also have "... ≤ 1 + length (borraDuplicados xs)" by simp
  also have "... ≤ 1 + length xs" using HI by simp
  also have "... ≤ length (a # xs)" by simp
  finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)" by simp
qed
(*Nota: así conseguimos demostrar el caso de que el elemento 'a' no esté repetido
en la lista. Que pasa con la demostración para el caso de una lista cuyos los elementos 
sean todos duplicados. Por ejemplo [1::1,1,1,1,1,1].
Esto no se reduce:
  have "length (borraDuplicados (a # xs)) ≤ length (borraDuplicados xs)" by simp
*)

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

-- "javrodviv1, juacorvic" 
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto

--"jeshorcob"
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs, auto)
done
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 17.2. Demostrar o refutar detalladamente
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
*}
 

(*Pedrosrei: con esta definición de borraDuplicados es falso si cogemos
xs= []. Además del quickcheck, podemos hacer "apply (induct xs, auto)" 
y ver que nos pide que demostremos False.
*)
lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
oops


(*jeshorcob: dejo la prueba por inducción y casos*)
--"jeshorcob"
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 a1:"estaEn x xs"
    then have "estaEn a (borraDuplicados (x#xs)) = 
                estaEn a (borraDuplicados xs)" by simp
    also have "... = estaEn a xs" using hi by simp
    also have "... = estaEn a (x#xs)" using a1 by auto
    finally show ?thesis by simp
  next
    assume a2:"¬(estaEn x xs)"
    then have "estaEn a (borraDuplicados (x#xs)) =
                estaEn a (x#borraDuplicados xs)" by simp
    also have "... = (a = x ∨ estaEn a (borraDuplicados xs))" by simp
    finally show ?thesis using hi by simp
  qed
qed
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 18.1. Demostrar o refutar automáticamente 
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}
 
--"jeshorcob"
lemma "sinDuplicados2 (borraDuplicados xs)"
by (induct xs) (auto simp add: estaEn_borraDuplicados)
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 18.2. Demostrar o refutar detalladamente
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}
 
--"jeshorcob"
lemma sinDuplicados_borraDuplicados:
  "sinDuplicados2 (borraDuplicados xs)"
proof (induct xs)
  show "sinDuplicados2 (borraDuplicados [])" by simp
next
  fix x::"'a"
  fix xs::"'a list"
  assume hi: "sinDuplicados2 (borraDuplicados xs)"
  have "sinDuplicados2 (borraDuplicados (x#xs)) =
          sinDuplicados2 ((if estaEn x xs then borraDuplicados xs 
                           else x # borraDuplicados xs))" by simp
  also have "... = (if estaEn x xs 
                      then sinDuplicados2 (borraDuplicados xs) 
                    else sinDuplicados2 (x#borraDuplicados xs))" by simp
  also have "...= (if estaEn x xs then sinDuplicados2 (borraDuplicados xs)
                   else (¬estaEn x (borraDuplicados xs) 
                          ∧ sinDuplicados2 (borraDuplicados xs)))" by simp
  also have "...= (if estaEn x xs then sinDuplicados2 (borraDuplicados xs) 
                   else (¬estaEn x xs ∧ sinDuplicados2 (borraDuplicados xs)))"
                     by (simp add: estaEn_borraDuplicados)
then show "sinDuplicados2 (borraDuplicados (x#xs))" 
             using hi by (simp add: estaEn_borraDuplicados)
qed
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 19. Demostrar o refutar:
    borraDuplicados (rev xs) = rev (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}
 
 (*Pedrosrei: es falso, como podemos ver si cogemos [1,2,1] y evaluamos:
*)
lemma "borraDuplicados' (rev xs) = rev (borraDuplicados' xs)"
quickcheck
oops

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

text {* Encuentra el contraejemplo
xs = [a⇩1, a⇩2, a⇩1]
Evaluated terms:
borraDuplicados (rev xs) = [a⇩2, a⇩1]
rev (borraDuplicados xs) = [a⇩1, a⇩2]
*}
 
end