header {* 7ª relación de ejercicios *}
theory Relacion_7_sol
imports Main Efficient_Nat
begin
section {* Contador de occurrencias *}
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
veces :: "'a ⇒ 'a list ⇒ nat"
tal que (veces x ys) es el número de occurrencias del elemento x en la
lista ys. Por ejemplo,
veces (2::nat) [2,1,2,5,2] = 3
---------------------------------------------------------------------
*}
primrec veces :: "'a ⇒ 'a list ⇒ nat" where
"veces x [] = 0"
| "veces x (y#ys) = (if x = y then 1 + veces x ys else veces x ys)"
text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
veces a (xs @ ys) = veces a xs + veces a ys
---------------------------------------------------------------------
*}
lemma "veces a (xs @ ys) = veces a xs + veces a ys"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar:
veces a xs = veces a (rev xs)
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar:
"veces a xs ≤ length xs".
---------------------------------------------------------------------
*}
lemma "veces a xs ≤ length xs"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 5. Sabiendo que la función map aplica una función a todos los
elementos de una lista:
map f [x\<^isub>1,…,x\<^isub>n] = [f x\<^isub>1,…,f x\<^isub>n],
demostrar o refutar
veces a (map f xs) = veces (f a) xs
---------------------------------------------------------------------
*}
lemma "veces a (map f xs) = veces (f a) xs"
quickcheck
oops
text{*
El contraejemplo encontrado es el siguiente:
xs = [1]
f = (λx. 0)(1 := 0, 0 := 0)
a = 0
Esto es: 0 = f(1) pero f(0) ≠ 1
*}
text {*
---------------------------------------------------------------------
Ejercicio 6. La función
filter :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list"
está definida por
filter P [] = []
filter P (x # xs) = (if P x then x # filter P xs else filter P xs)
Encontrar una expresión e que no contenga filter tal que se verifique
la siguiente propiedad:
veces a (filter P xs) = e
---------------------------------------------------------------------
*}
lemma "veces a (filter P xs) = (if P a then veces a xs else 0)"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 7. Usando veces, definir la función
borraDups :: "'a list ⇒ bool"
tal que (borraDups xs) es la lista obtenida eliminando los elementos
duplicados de la lista xs. Por ejemplo,
borraDups [1::nat,2,4,2,3] = [1,4,2,3]
Nota: La función borraDups es equivalente a la predefinida remdups.
---------------------------------------------------------------------
*}
text {*
El tipo correspondiente al conjunto imagen de la función definida
no coincide con el indicado en la declaración de tipos del enunciado,
dado que en él aparece erróneamente la salida de tipo bool, mientras
que del resto del texto se deduce que la salida es una lista de
elementos de tipo 'a.
*}
primrec borraDups :: "'a list ⇒ 'a list" where
"borraDups [] = []"
| "borraDups (x#xs) = (if veces x xs > 0 then borraDups xs else (x#borraDups xs))"
text {*
Nota: para que no muestre error la función de evaluación
hay que indicarle el tipo de los elementos de la lista.
Por ejemplo:
value "borraDups [1::nat,2,4,2,3]"
*}
text {*
---------------------------------------------------------------------
Ejercicio 8. Encontrar una expresión e que no contenga la función
borraDups tal que se verifique
veces x (borraDups xs) = e
---------------------------------------------------------------------
*}
lemma "veces x (borraDups xs) = (if (veces x xs) >= 1 then 1 else 0)"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 9. Usando la función "veces", definir la función
distintos :: "'a list ⇒ bool"
tal que (distintos xs) se verifica si cada elemento de xs aparece tan
solo una vez. Por ejemplo,
distintos [1,4,3]
¬ distintos [1,4,1]
Nota: La función "distintos" es equivalente a la predefinida "distinct".
---------------------------------------------------------------------
*}
primrec distintos :: "'a list ⇒ bool" where
"distintos [] = True"
| "distintos (x#xs) = (if veces x xs > 0 then False else distintos xs)"
text {*
Nota: para que no muestre error la función de evaluación
hay que indicarle el tipo de los elementos de la lista.
Por ejemplo:
value "distintos [1::nat,4,1]"
*}
text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que el valor de "borraDups" verifica "distintos".
---------------------------------------------------------------------
*}
lemma "(distintos xs) ⟶ ((length xs) = (length (borraDups xs)))"
by (induct xs) auto
text{*
Si xs verifica el predicado distintos, entonces el tamaño de xs debe de ser el mismo
antes y despues de borrar los duplcados.
*}
end
