header {* R14: Contador de occurrencias *}
theory R14
imports Main
begin
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
---------------------------------------------------------------------
*}
fun veces :: "'a ⇒ 'a list ⇒ nat" where
"veces x ys = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
veces a (xs @ ys) = veces a xs + veces a ys
---------------------------------------------------------------------
*}
lemma veces_append:
"veces a (xs @ ys) = veces a xs + veces a ys"
oops
text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar:
veces a xs = veces a (rev xs)
---------------------------------------------------------------------
*}
lemma veces_rev:
"veces a xs = veces a (rev xs)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar:
"veces a xs ≤ length xs".
---------------------------------------------------------------------
*}
lemma veces_le_length_auto:
"veces a xs ≤ length xs"
oops
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_map:
"veces a (map f xs) = veces (f a) xs"
oops
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
y demostrar la conjetura.
---------------------------------------------------------------------
*}
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.
---------------------------------------------------------------------
*}
fun borraDups :: "'a list ⇒ 'a list" where
"borraDups xs = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 8. Encontrar una expresión e que no contenga la función
borraDups tal que se verifique
veces x (borraDups xs) = e
y demostrar la conjetura.
---------------------------------------------------------------------
*}
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".
---------------------------------------------------------------------
*}
fun distintos :: "'a list ⇒ bool" where
"distintos xs = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que el valor de "borraDups" verifica
"distintos".
---------------------------------------------------------------------
*}
lemma distintos_borraDups:
"distintos (borraDups xs)"
oops
end
