Jalonso en 07:50 16 jul 2018

2018-07-16T07:50:34Z

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

2011-02-14T22:50:39Z

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

Jalonso: Página creada con ' header {* 5ª relación de ejercicios } theory Relacion_5 imports Main begin section { Menor posición válida } text { -------------------------...'

2011-02-14T22:50:28Z

Página creada con '<source lang="isar"> header {* 5ª relación de ejercicios *} theory Relacion_5 imports Main begin section {* Menor posición válida *} text {* -------------------------...'

Página nueva

<source lang="isar">
header {* 5ª relación de ejercicios *}

theory Relacion_5
imports Main
begin

section {* Menor posición válida *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
tal que (menorValida p xs) es el índice del primer elemento de una
lista xs que satisface el predicado p y es la longitud de xs si
ningún elemento satisface el predicado p. Por ejemplo,
menorValida (λx. 4<x) [1::nat, 3, 5, 3, 1] = 2
menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5
menorValida (λx. 1<length x) [[], [1, 2], [3]] = 1
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar que menorValida devuelve la longitud de la
lista syss ningún elemento satisface el predicado dado.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar si n es el valor de (menorValida P xs),
entonces ninguno de los primeros n elementos de la lista xs verifica
la propiedad P.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 4. ¿Cómo se puede relacionar
"menorValida (λ x. P x ∨ Q x) xs"
con
"menorValida P xs" y "menorValida Q xs"?
¿Se puede decir algo parecido con la conjunción de P y Q?
Prueba tus conjeturas.
---------------------------------------------------------------------
*}

text {*
La relación es la siguiente: La menor posición de los elementos que
verifican la propiedad "P ∨ Q" es el mínimo de la menor posición de
los elementos que verifican P y de la menor posición de los elementos
que verifican Q.
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Si P implica Q, ¿qué relación puede deducirse entre
"menorValida P xs" y "menorValida Q xs"?
---------------------------------------------------------------------
*}

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 {* 5ª relación de ejercicios *}		header {* 5ª relación de ejercicios *}

← Revisión anterior	Revisión del 22:50 14 feb 2011
(Sin diferencias)

Rel 5 - Historial de revisiones

Jalonso en 07:50 16 jul 2018

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

Jalonso: Página creada con ' header {* 5ª relación de ejercicios *} theory Relacion_5 imports Main begin section {* Menor posición válida *} text {* -------------------------...'

Jalonso: Página creada con ' header {* 5ª relación de ejercicios } theory Relacion_5 imports Main begin section { Menor posición válida } text { -------------------------...'