Diferencia entre revisiones de «Rel 6»
De Razonamiento automático (2010-11)
m (Protegió «Rel 6» ([edit=sysop] (indefinido) [move=sysop] (indefinido))) |
|||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
header {* 6ª relación de ejercicios *} | header {* 6ª relación de ejercicios *} | ||
Revisión actual del 09:50 16 jul 2018
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