Rel 6 - Historial de revisiones

Jalonso en 07:50 16 jul 2018

2018-07-16T07:50:53Z

Jalonso: Protegió «Rel 6» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2011-02-21T19:46:17Z

Protegió «Rel 6» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso en 19:46 21 feb 2011

2011-02-21T19:46:02Z

Jalonso: Página creada con ' header {* 6ª relación de ejercicios } theory Relacion_6 imports Main begin section { Número de elementos válidos } text { -------------------...'

2011-02-21T19:44:56Z

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 {* -------------------...'

Página nueva

<source lang="isar">
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 \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
tal que (cuentaP Q xs) es el número de elementos de la lista xs que
satisfacen el predicado Q. Por ejemplo,
cuentaP (\<lambda>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
</source>

← Revisión anterior		Revisión del 07:50 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* 6ª relación de ejercicios *}		header {* 6ª relación de ejercicios *}

← Revisión anterior	Revisión del 19:46 21 feb 2011
(Sin diferencias)

@@ Línea 11: / Línea 11: @@
    ---------------------------------------------------------------------
    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
    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
    ---------------------------------------------------------------------
 *}

Rel 6 - Historial de revisiones

Jalonso en 07:50 16 jul 2018

Jalonso: Protegió «Rel 6» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso en 19:46 21 feb 2011

Jalonso: Página creada con ' header {* 6ª relación de ejercicios *} theory Relacion_6 imports Main begin section {* Número de elementos válidos *} text {* -------------------...'

Jalonso: Página creada con ' header {* 6ª relación de ejercicios } theory Relacion_6 imports Main begin section { Número de elementos válidos } text { -------------------...'