Relación 6

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
  --------------------------------------------------------------------- 
*}



primrec cuentaP :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
  "cuentaP Q [] = 0"
| "cuentaP Q (x#xs) = (if Q x then 1 + cuentaP Q xs else cuentaP Q xs)"




text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar o refutar:
     cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys*
  --------------------------------------------------------------------- 
*}


text {* 
Se puede demostrar tal como se indica a continuación
*}


lemma "cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys"
by (induct xs arbitrary: ys) auto



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