Relación 5 - Historial de revisiones

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

2018-07-16T07:51:51Z

Texto reemplazado: «"isar"» por «"isabelle"»

Jmuros en 21:15 16 feb 2011

2011-02-16T21:15:18Z

Enrique Sarrión en 22:30 15 feb 2011

2011-02-15T22:30:00Z

Enrique Sarrión en 22:13 15 feb 2011

2011-02-15T22:13:36Z

Jmuros en 21:45 15 feb 2011

2011-02-15T21:45:12Z

Julianmina en 15:52 15 feb 2011

2011-02-15T15:52:20Z

Julianmina en 15:40 15 feb 2011

2011-02-15T15:40:02Z

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:09:03Z

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:51 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 *}

@@ Línea 35: / Línea 35: @@
 lemma "menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5"
 by auto
 text {*
@@ Línea 49: / Línea 40: @@
    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
+   la propiedad P.
    ---------------------------------------------------------------------
 *}
@@ Línea 58: / Línea 49: @@
 lemma "menorValida (λx. 4<x) [1::nat, 2, 3, 4, 7] = 5"
-by auto
+quickcheck

@@ Línea 36: / Línea 36: @@
 by auto
--- "Un comentario a la vista de esta propuesta: si lo que pide el enunciado
 es una demostración, considero que no basta con exhibir un ejemplo en el que
 el resultado se satisface."