DAO (Demostración asistida por ordenador) DAO (Demostración asistida por ordenador)

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