2014-11-18T09:52:14Z

Juacorvic:

<source lang="isar">
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"
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"

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

Relación 5

2014-11-18T09:31:10Z

Juacorvic:

<source lang="isar">
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"
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
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"

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