Acciones

Diferencia entre revisiones de «Rel 6»

De Razonamiento automático (2010-11)

(Página creada con '<source lang="isar"> header {* 6ª relación de ejercicios *} theory Relacion_6 imports Main begin section {* Número de elementos válidos *} text {* -------------------...')
 
 
(No se muestran 2 ediciones intermedias del mismo usuario)
Línea 1: Línea 1:
<source lang="isar">
+
<source lang="isabelle">
 
header {* 6ª relación de ejercicios *}
 
header {* 6ª relación de ejercicios *}
  
Línea 11: Línea 11:
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
 
   Ejercicio 1. Definir la función  
 
   Ejercicio 1. Definir la función  
     cuentaP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
+
     cuentaP :: "('a bool) 'a list nat"
 
   tal que (cuentaP Q xs) es el número de elementos de la lista xs que
 
   tal que (cuentaP Q xs) es el número de elementos de la lista xs que
 
   satisfacen el predicado Q. Por ejemplo,   
 
   satisfacen el predicado Q. Por ejemplo,   
     cuentaP (\<lambda>x. 2<x) [1,3,4,0,5] = 3
+
     cuentaP (λx. 2<x) [1,3,4,0,5] = 3
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
 
*}
 
*}

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