header {* R13: Número de elementos válidos *}
theory R13
imports Main
begin
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
---------------------------------------------------------------------
*}
fun cuentaP :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
"cuentaP Q xs = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys*
---------------------------------------------------------------------
*}
lemma cuentaP_append_auto:
"cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys"
oops
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.
---------------------------------------------------------------------
*}
lemma cuentaP_rev:
"cuentaP P xs = cuentaP P (rev xs)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 4. Encontrar y demostrar una relación entre las funciones
filter y cuentaP.
---------------------------------------------------------------------
*}
end
