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"

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

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

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"
 
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"
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"
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
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.1. Demostrar o refutar automáticamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

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

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

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"
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"
 
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" 
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" 
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
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 17.1. Demostrar o refutar automáticamente 
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
*}

-- "javrodviv1" 
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
De Razonamiento automático (2014-15)
