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