R11

chapter ‹ R11: Razonamiento sobre programas en Isabelle/HOL (II)›
 
theory R11
imports Main 
begin


text ‹ --------------------------------------------------------------- 
   En toda la relación de ejercicios las demostraciones han de realizarse
   de las formas siguientes:
    + automática
    + en el ejercicio 1.2, la prueba detallada usando "simp only:..."
      (bien de forma declarativa o aplicativa) 
    + en los ejercicios 5, 6 y 7 sólo es necesario hacer la demostración 
      detallada usando "simp", sin llegar al detalle de usar "simp only:..."
  ------------------------------------------------------------------ ›
    
text ‹ --------------------------------------------------------------- 
  Ejercicio 1.1. Definir la función
    factR :: nat ⇒ nat
  tal que (factR n) es el factorial de n. Por ejemplo,
    factR 4 = 24
  ------------------------------------------------------------------ ›
 
fun factR :: "nat ⇒ nat" where
  "factR 0       = 1"
| "factR (Suc n) = Suc n * factR n"
 
value "factR 4" ― ‹= 24›
 
text ‹ --------------------------------------------------------------- 
  Ejercicio 1.2. Se considera la siguiente definición iterativa de la
  función factorial 
     factI :: "nat ⇒ nat" where
     factI n = factI' n 1
 
     factI' :: nat ⇒ nat ⇒ nat" where
     factI' 0       x = x
     factI' (Suc n) x = factI' n (Suc n)*x
  Demostrar que, para todo n y todo x, se tiene 
     factI' n x = x * factR n
  ------------------------------------------------------------------- ›
 
fun factI' :: "nat ⇒ nat ⇒ nat" where
  "factI' 0       x = x"
| "factI' (Suc n) x = factI' n (x* (Suc n))"
 
fun factI :: "nat ⇒ nat" where
  "factI n = factI' n 1"
 
 ― ‹Demostración automática:›
lemma "factI' n x = x * factR n"  
  oops

 ― ‹Demostración detallada:›
lemma fact_d: "factI' n x = x * factR n"
  oops
 
text ‹ --------------------------------------------------------------- 
  Ejercicio 1.3. Demostrar que
     factI n = factR n
  ------------------------------------------------------------------- ›
 
corollary fact_equiv: "factI n = factR n"
  oops

 text ‹
  --------------------------------------------------------------------- 
  Ejercicio 2. 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) = (x=a ∨ estaEn x xs)"


text ‹ 
  --------------------------------------------------------------------- 
  Ejercicio 3. Definir la función
     sinDuplicados :: 'a list ⇒ bool
  tal que (sinDuplicados xs) se verifica si la lista xs no contiene
  duplicados. Por ejemplo,  
     sinDuplicados [1::nat,4,2]   = True
     sinDuplicados [1::nat,4,2,4] = False
  --------------------------------------------------------------------- 
›

fun sinDuplicados :: "'a list ⇒ bool" where
  "sinDuplicados []     = True"
| "sinDuplicados (a#xs) = ((¬ estaEn a xs) ∧ sinDuplicados xs)"


text ‹ 
  --------------------------------------------------------------------- 
  Ejercicio 4. Definir la función
     borraDuplicados :: 'a list ⇒ bool
  tal que (borraDuplicados xs) es la lista obtenida eliminando los
  elementos duplicados de la lista xs. Por ejemplo, 
     borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

  Nota: La función borraDuplicados es equivalente a la predefinida 
  remdups. 
  --------------------------------------------------------------------- 
›


fun borraDuplicados :: "'a list ⇒ 'a list" where
  "borraDuplicados []     = []"
| "borraDuplicados (a#xs) = (if estaEn a xs
                             then borraDuplicados xs
                             else (a#borraDuplicados xs))"

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 5. Demostrar o refutar
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
›

 ― ‹Demostración automática:›
lemma "length (borraDuplicados xs) ≤ length xs"
  oops

 ― ‹Demostración detallada:›
lemma length_borraDuplicados_d:
"length (borraDuplicados xs) ≤ length xs"
  oops

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
›

 ― ‹Demostración automática:›
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
  oops  

 ― ‹Demostración detallada:›
lemma estaEn_borraDuplicados_d:
  "estaEn a (borraDuplicados xs) = estaEn a xs"
  oops

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar o refutar
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
›

 ― ‹Demostración automática:›
lemma "sinDuplicados (borraDuplicados xs)"
  oops

 ― ‹Demostración detallada:›
lemma sinDuplicados_borraDuplicados_d:
  "sinDuplicados (borraDuplicados xs)"
  oops

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar o refutar:
    borraDuplicados (rev xs) = rev (borraDuplicados xs)
  --------------------------------------------------------------------- 
›

lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
  oops


end