DAO (Demostración asistida por ordenador) DAO (Demostración asistida por ordenador)

header {* R12: Menor posición válida *}

theory R12
imports Main 
begin

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

fun menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
  "menorValida P xs = undefined"

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

lemma "(menorValida P xs = length xs) = list_all (λ x. (¬ P x)) xs"
oops

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. 
  --------------------------------------------------------------------- 
*}

lemma "list_all (λx. ¬ P x) (take (menorValida P xs) xs)"
oops

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 {* 
  --------------------------------------------------------------------- 
  Ejercicio 5.  Si P implica Q, ¿qué relación puede deducirse entre 
  "menorValida P xs" y "menorValida Q xs"? Prueba tu conjetura.
  --------------------------------------------------------------------- 
*}

end