R12

<source lang = "isabelle" chapter ‹ R12: Razonamiento sobre programas en Isabelle/HOL (III)›

theory R12 imports Main begin

text ‹------------------------------------------------------------------

 En toda la relación de ejercicios las demostraciones han de realizarse
 de las formas siguientes:
 + en lenguaje natural
 + aplicativa o declarativa usando "simp"
 + aplicativa o declarativa usando "simp only: ..."  
 + automática

 Además, se recomienda el uso de lemas auxiliares (nuevos o de los 
 ejercicios anteriores) para que las demostraciones sean más cortas y 
 claras.
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Ejercicio 1. Definir la función
    estaEn :: 'a ⇒ 'a list ⇒ bool
 tal que (estaEn x xs) se verifica si el elemento x está en la lista
 xs. Por ejemplo, 
    estaEn (2::nat) [3,2,4] = True
    estaEn (1::nat) [3,2,4] = False
 ---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where

 "estaEn x []     = False"

| "estaEn x (a#xs) = (a=x ∨ estaEn x xs)"

text ‹------------------------------------------------------------------

 Ejercicio 2. Definir la función 
    sublista :: "'a list ⇒ 'a list ⇒ bool
 tal que (sublista xs ys) se verifica si todos los elementos de la
 lista xs están en la lista ys. Por ejemplo,
    sublista [(1::nat),2,3] [3,2,1,2] = True
    sublista [(1::nat),2,3] [2,1,2]   = False
----------------------------------------------------------------------›

fun sublista :: "'a list ⇒ 'a list ⇒ bool" where

 "sublista [] ys     = True"

| "sublista (x#xs) ys = (estaEn x ys ∧ sublista xs ys )"

text ‹------------------------------------------------------------------

 Ejercicio 3. Demostrar la siguiente propiedad: si xs es sublista de 
 ys, entonces xs también es sublista de la lista (y#ys). Es decir,
    sublista xs ys ⟹ sublista xs (y#ys)
----------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma sublistaMono_d:

 "sublista xs ys ⟶ sublista xs (y#ys)"
 oops

― ‹Demostración aplicativa:›

lemma sublistaMono: "sublista xs ys ⟹ sublista xs (y#ys)"

 oops

text ‹------------------------------------------------------------------

 Ejercicio 4. Demostrar que la relación sublista es reflexiva. Es 
 decir,
    sublista xs xs
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma sublistaReflexiva_d: "sublista xs xs"

 oops

― ‹Demostración aplicativa:›

lemma sublistaReflexiva: "sublista xs xs"

 oops

text ‹------------------------------------------------------------------

 Ejercicio 5. Probar, como corolario, que 
    sublista xs (x#xs)
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

corollary sublistaInc_d: "sublista xs (x#xs)"

 oops

― ‹Demostración aplicativa:›

corollary sublistaInc: "sublista xs (x#xs)"

 oops

text ‹------------------------------------------------------------------

 Ejercicio 6. Probar que la relación sublista es transitiva. Es decir,
    sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma sublistaTransitiva_d:

 "sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
 oops

― ‹Demostración aplicativa:›

lemma sublistaTransitiva:

 "sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
 oops

text ‹------------------------------------------------------------------

 Ejercicio 7. Definir la función
    coge :: nat ⇒ 'a list ⇒ 'a list
 tal que (coge n xs) es la lista de los n primeros elementos de xs. Por 
 ejemplo, 
    coge 2 [a,c,d,b,e] = [a,c]
 ------------------------------------------------------------------ ›

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where

 "coge n []           = []"

| "coge 0 xs = []" | "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [a,c,d,b,e] = [a,c]"

text ‹------------------------------------------------------------------

 Ejercicio 8. Probar que 
    coge 0 xs = []
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma coge0_d: "coge 0 xs = []"

 oops

― ‹Demostración aplicativa:›

lemma coge0: "coge 0 xs = []"

 oops

text ‹------------------------------------------------------------------

 Ejercicio 9. Probar que 
    length xs ≤ n ⟹ coge n xs = xs
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma cogeTodos_d:

   "length xs ≤ n ⟶ coge n xs = xs"
 oops

― ‹Demostración aplicativa:›

lemma cogeTodos: "length xs ≤ n ⟹ coge n xs = xs"

 oops

text ‹------------------------------------------------------------------

 Ejercicio 10. Probar que 
    length (coge n xs) ≤ n
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma cogeLongN_d: "length (coge n xs) ≤ n"

 oops

― ‹Demostración aplicativa:›

lemma cogeLongN: "length (coge n xs) ≤ n"

 oops

text ‹------------------------------------------------------------------

 Ejercicio 11. Probar que 
     length (coge n xs) ≤ length xs
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma cogeLongL_d: "length (coge n xs) ≤ length xs"

 oops

― ‹Demostración aplicativa:›

lemma cogeLongL: "length (coge n xs) ≤ length xs"

 oops

text ‹------------------------------------------------------------------

 Ejercicio 12. Probar que 
    length (coge n xs) = min n (length xs)
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma lengthCogeMin_d:"length (coge n xs) = min n (length xs)"

 oops

― ‹Demostración aplicativa:›

lemma lengthCogeMin: "length (coge n xs) = min n (length xs)"

 oops

text ‹------------------------------------------------------------------

 Ejercicio 13. Probar que
    estaEn x (coge n xs) ⟹ estaEn x xs
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma estaEnCoge_d:

   "estaEn x (coge n xs) ⟶ estaEn x xs"
 oops

― ‹Demostración aplicativa:›

lemma estaEnCoge:

 "estaEn x (coge n xs) ⟹ estaEn x xs"
 oops

text ‹------------------------------------------------------------------

 Ejercicio 14. Probar que 
    sublista (coge n xs) xs
 ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------

 Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma sublistaCoge_d: "sublista (coge n xs) xs"

 oops

― ‹Demostración aplicativa:›

lemma sublistaCoge: "sublista (coge n xs) xs"

 oops

end </source>