header {* 6ª relación de ejercicios *}
theory Relacion_6
imports Main
begin
section {* Número de elementos válidos *}
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
cuentaP :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
tal que (cuentaP Q xs) es el número de elementos de la lista xs que
satisfacen el predicado Q. Por ejemplo,
cuentaP (λx. 2<x) [1,3,4,0,5] = 3
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys*
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar que el número de elementos de una lista que
cumplen una determinada propiedad es el mismo que el de esa lista
invertida.
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 4. Encontrar y demostrar una relación entre las funciones
filter y cuentaP.
---------------------------------------------------------------------
*}
end