R12

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