Lógica matemática y fundamentos (2018-19) Lógica matemática y fundamentos (2018-19)

chapter ‹Tema 6: Razonamiento sobre programas›

theory T6_Razonamiento_sobre_programas
imports Main 
begin

text ‹En este tema se demuestra con Isabelle las propiedades de los
  programas funcionales de tema 6 http://bit.ly/2Za6YWY

  Para cada propiedades se presentan distintos tipos de demostraciones:
  automáticas, aplicativas y declarativas.› 

section ‹Razonamiento ecuacional›

text ‹-----------------------------------------------------------------
  Ejemplo 1. Definir, por recursión, la función
     longitud :: 'a list ⇒ nat
  tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
     longitud [a,c,d] = 3
  --------------------------------------------------------------------›

fun longitud :: "'a list ⇒ nat" where
  "longitud []     = 0"
| "longitud (x#xs) = 1 + longitud xs"
   
value "longitud [a,c,d] = 3"

text ‹ --------------------------------------------------------------- 
  Ejemplo 2. Demostrar que 
     longitud [a,c,d] = 3
  ------------------------------------------------------------------- ›

lemma "longitud [a,c,d] = 3"
  apply simp
  done

lemma "longitud [a,c,d] = 3"
  by simp

text ‹ --------------------------------------------------------------- 
  Ejemplo 3. Definir la función
     fun intercambia :: 'a × 'b ⇒ 'b × 'a
  tal que (intercambia p) es el par obtenido intercambiando las
  componentes del par p. Por ejemplo,
     intercambia (u,v) = (v,u)
  ------------------------------------------------------------------ ›

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
  "intercambia (x,y) = (y,x)"

value "intercambia (u,v) = (v,u)"

text ‹La definición de la función intercambia genera una regla de
  simplificación
  · intercambia.simps: intercambia (x,y) = (y,x)
  
  Se puede ver con 
  · thm intercambia.simps 
›

thm intercambia.simps
(* da intercambia (?x, ?y) = (?y, ?x) *)

text ‹ --------------------------------------------------------------- 
  Ejemplo 4. (p.6) Demostrar que 
     intercambia (intercambia (x,y)) = (x,y)
  ------------------------------------------------------------------- ›

(* Demostración automática *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  by auto

(* Demostración automática 1 *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  by simp 

(* Demostración automática 2 *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  by (simp only: intercambia.simps)

(* Demostración aplicativa *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  apply (simp only: intercambia.simps)
  done

(* Demostración declarativa 1 *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
  have "intercambia (intercambia (x,y)) = intercambia (y,x)"  
    by simp
  also have "… = (x,y)" 
    by simp 
  finally show "intercambia (intercambia (x,y)) = (x,y)" 
    by simp
qed

(* Demostración detallada *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
  have "intercambia (intercambia (x,y)) = intercambia (y,x)"  
    by (simp only: intercambia.simps)
  also have "… = (x,y)" 
    by (simp only: intercambia.simps)
  finally show "intercambia (intercambia (x,y)) = (x,y)" 
    by simp
qed

text ‹Notas sobre el lenguaje: En la demostración anterior se ha usado
  · "proof" para iniciar la prueba,
  · "-" (después de "proof") para no usar el método por defecto,
  · "have" para establecer un paso,
  · "by (simp only: intercambia.simps)" para indicar que sólo se usa
    como regla de escritura la correspondiente a la definición de
    intercambia,
  · "also" para encadenar pasos ecuacionales,
  · "…" para representar la derecha de la igualdad anterior en un
    razonamiento ecuacional,
  · "finally" para indicar el último pasa de un razonamiento ecuacional,
  · "show" para establecer la conclusión.
  · "by simp" para indicar el método de demostración por simplificación y 
  · "qed" para terminar la pruebas.›

text ‹--------------------------------------------------------------- 
  Ejemplo 5. Definir, por recursión, la función
     inversa :: 'a list ⇒ 'a list
  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
  elementos de xs. Por ejemplo,
     inversa [a,d,c] = [c,d,a]
  ------------------------------------------------------------------ ›

fun inversa :: "'a list ⇒ 'a list" where
  "inversa []     = []"
| "inversa (x#xs) = inversa xs @ [x]"

value "inversa [a,d,c] = [c,d,a]"

text ‹ --------------------------------------------------------------- 
  Ejemplo 6. (p. 9) Demostrar que 
     inversa [x] = [x]
  ------------------------------------------------------------------- ›

(* La demostración automática es *)
lemma "inversa [x] = [x]"
  by simp

(* La demostración aplicativa es *)
lemma "inversa [x] = [x]"
  apply simp
  done

text ‹En la demostración anterior se usaron las siguientes reglas:
  · inversa.simps(1): inversa [] = []
  · inversa.simps(2): inversa (x#xs) = inversa xs @ [x]
  · append_Nil:       [] @ ys = ys
  Vamos a explicitar su aplicación.
›

find_theorems
find_theorems "_ @ _ = _"
find_theorems "[] @ _ = _"

(* La demostración aplicativa detallada es *)
lemma "inversa [x] = [x]"
  apply (simp only: inversa.simps(2)) (* inversa [] @ [x] = [x] *)
  apply (simp only: inversa.simps(1)) (* [] @ [x] = [x] *)
  apply (simp only: append_Nil)       (* No subgoals! *)
  done

(* La demostración declarativa simplificada es *)
lemma "inversa [x] = [x]"
proof -
  have "inversa [x] = inversa (x#[])" by simp
  also have "… = (inversa []) @ [x]" by simp
  also have "… = [] @ [x]" by simp
  also have "… = [x]" by simp 
  finally show "inversa [x] = [x]" by simp
qed

(* La demostración declarativa detallada es *)
lemma "inversa [x] = [x]"
proof -
  have "inversa [x] = inversa (x#[])"  
    by simp
  also have "… = (inversa []) @ [x]" 
    by (simp only: inversa.simps(2))
  also have "… = [] @ [x]" 
    by (simp only: inversa.simps(1))
  also have "… = [x]" 
    by (simp only: append_Nil) 
  finally show "inversa [x] = [x]" by simp
qed

section ‹Razonamiento por inducción sobre los naturales ›

text ‹[Principio de inducción sobre los naturales] Para demostrar una
  propiedad P para todos los números naturales basta probar que el 0
  tiene la propiedad P y que si n tiene la propiedad P, entonces n+1
  también la tiene.  
     ⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m

  En Isabelle el principio de inducción sobre los naturales está
  formalizado en el teorema nat.induct y puede verse con
     thm nat.induct
›

thm nat.induct

text ‹--------------------------------------------------------------- 
  Ejemplo 7. Definir la función
     repite :: nat ⇒ 'a ⇒ 'a list
  tal que (repite n x) es la lista formada por n copias del elemento
  x. Por ejemplo, 
     repite 3 a = [a,a,a]
  ------------------------------------------------------------------ ›

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
  "repite 0 x       = []"
| "repite (Suc n) x = x # (repite n x)"

value "repite 3 a = [a,a,a]"

text ‹ --------------------------------------------------------------- 
  Ejemplo 8. (p. 18) Demostrar que 
     longitud (repite n x) = n
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "longitud (repite n x) = n"
  apply (induct n) (* 1. longitud (repite 0 x) = 0
                      2. ⋀n. longitud (repite n x) = n ⟹
                         longitud (repite (Suc n) x) = Suc n *)
   apply simp      (* 1. ⋀n. longitud (repite n x) = n ⟹
                         longitud (repite (Suc n) x) = Suc n *)
  apply simp       (* No subgoals *)
  done

(* La demostración aplicativa con simp_all es *)
lemma "longitud (repite n x) = n"
  apply (induct n) (* 1. longitud (repite 0 x) = 0
                      2. ⋀n. longitud (repite n x) = n ⟹
                         longitud (repite (Suc n) x) = Suc n *)
   apply simp_all  (* No subgoals *)
  done

(* La demostración automática es *)
lemma "longitud (repite n x) = n"
  by (induct n) simp_all

(* La demostración declarativa es *)
lemma "longitud (repite n x) = n"
proof (induct n)
  show "longitud (repite 0 x) = 0" 
    by simp
next 
  fix n
  assume HI: "longitud (repite n x) = n"
  have "longitud (repite (Suc n) x) = longitud (x # (repite n x))" 
    by simp
  also have "… = 1 + longitud (repite n x)" 
    by simp
  also have "… = 1 + n" 
    using HI by simp
  finally show "longitud (repite (Suc n) x) = Suc n" 
    by simp
qed

text ‹Comentarios sobre la demostración anterior:
  · A la derecha de proof se indica el método de la demostración.
  · (induct n) indica que la demostración se hará por inducción en n.
  · Se generan dos subobjetivos correspondientes a la base y el paso de
    inducción:
    1. longitud (repite 0 x) = 0
    2. ⋀n. longitud (repite n x) = n ⟹ 
            longitud (repite (Suc n) x) = Suc n
    donde ⋀n se lee "para todo n".  
  · "next" indica el siguiente subobjetivo.
  · "fix n" indica "sea n un número natural cualquiera"
  · assume HI: "longitud (repite n x) = n" indica «supongamos que 
    "longitud (repite n x) = n" y sea HI la etiqueta de este supuesto».
  · "using HI" usando la propiedad etiquetada con HI. ›

(* La demostración declarativa detallada es *)
lemma "longitud (repite n x) = n"
proof (induct n)
  show "longitud (repite 0 x) = 0"
    by (simp only: repite.simps(1)
                   longitud.simps(1))
next 
  fix n
  assume HI: "longitud (repite n x) = n"
  have "longitud (repite (Suc n) x) = longitud (x # (repite n x))" 
    by (simp only: repite.simps(2))
  also have "… = 1 + longitud (repite n x)" 
    by (simp only: longitud.simps(2))
  also have "… = 1 + n" 
    by (simp only: HI)
  also have "… = Suc n"
    find_theorems "Suc _ = _ + _"
    by (simp only: Suc_eq_plus1_left)
  finally show "longitud (repite (Suc n) x) = Suc n" 
    by this
qed

section ‹Razonamiento por inducción sobre listas ›

text ‹Para demostrar una propiedad para todas las listas basta demostrar
  que la lista vacía tiene la propiedad y que al añadir un elemento a
  una lista que tiene la propiedad se obtiene otra lista que también
  tiene la propiedad. 

  En Isabelle el principio de inducción sobre listas está formalizado
  mediante el teorema list.induct 
     ⟦P []; 
      ⋀x xs. P xs ⟹ P (x#xs)⟧ 
     ⟹ P xs
›

thm list.induct

text ‹--------------------------------------------------------------- 
  Ejemplo 9. Definir la función
     conc :: 'a list ⇒ 'a list ⇒ 'a list
  tal que (conc xs ys) es la concatención de las listas xs e ys. Por
  ejemplo, 
     conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
  ------------------------------------------------------------------ ›

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
  "conc []     ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"

value "conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]"

text ‹ --------------------------------------------------------------- 
  Ejemplo 10. (p. 24) Demostrar que 
     conc xs (conc ys zs) = (conc xs ys) zs
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
  apply (induct xs) (*  1. conc [] (conc ys zs) = conc (conc [] ys) zs
                        2. ⋀a xs.
                              conc xs (conc ys zs) =
                              conc (conc xs ys) zs ⟹
                              conc (a # xs) (conc ys zs) =
                              conc (conc (a # xs) ys) zs *)
   apply simp_all   (* No subgoals! *)
  done  

(* La demostración automática es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
  by (induct xs) simp_all

(* La demostración declarativa es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
  show "conc [] (conc ys zs) = conc (conc [] ys) zs" 
    by simp
next
  fix x xs
  assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs" 
  have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" 
    by simp
  also have "… = x # (conc (conc xs ys) zs)" 
    using HI by simp
  also have "… = conc (conc (x # xs) ys) zs" 
    by simp
  finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs" 
    by simp
qed

(* La demostración declarativa detallada es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
  show "conc [] (conc ys zs) = conc (conc [] ys) zs" 
    by (simp only: conc.simps(1))
next
  fix x xs
  assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs" 
  have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" 
    by (simp only: conc.simps(2))
  also have "… = x # (conc (conc xs ys) zs)" 
    using HI by (simp only:)
  also have "… = conc (conc (x # xs) ys) zs" 
    by (simp only: conc.simps(2))
  finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs" 
    by this
qed

text ‹--------------------------------------------------------------- 
  Ejemplo 11. Refutar que 
     conc xs ys = conc ys xs
  ------------------------------------------------------------------- ›

lemma "conc xs ys = conc ys xs"
  quickcheck
  oops

text ‹ Encuentra el contraejemplo, 
  xs = [a2]
  ys = [a1] ›

text ‹--------------------------------------------------------------- 
  Ejemplo 12. (p. 28) Demostrar que 
     conc xs [] = xs
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "conc xs [] = xs"
  apply (induct xs) (* 1. conc [] [] = []
                       2. ⋀a xs.
                             conc xs [] = xs ⟹
                             conc (a # xs) [] = a # xs *)
   apply simp_all   (* No subgoals! *)
  done  

(* La demostración automática es *)
lemma "conc xs [] = xs"
  by (induct xs) simp_all

(* La demostración declarativa es *)
lemma "conc xs [] = xs"
proof (induct xs)
  show "conc [] [] = []" by simp
next 
  fix x xs
  assume HI: "conc xs [] = xs" 
  have "conc (x # xs) [] = x # (conc xs [])" 
    by simp
  also have "… = x # xs" 
    using HI by simp
  finally show "conc (x # xs) [] = x # xs" 
    by simp
qed

(* declare [[show_types]] *)

(* La demostración declarativa es *)
lemma "conc xs [] = xs"
proof (induct xs)
  show "conc [] [] = []" by simp
next 
  fix x :: "'a" and xs :: "'a list"
  assume HI: "conc xs [] = xs" 
  have "conc (x # xs) [] = x # (conc xs [])" 
    by simp
  also have "… = x # xs" 
    using HI by simp
  finally show "conc (x # xs) [] = x # xs" 
    by simp
qed

(* La demostración declarativa detallada es *)
lemma "conc xs [] = xs"
proof (induct xs)
  show "conc [] [] = []" 
    by (simp only: conc.simps(1))
next 
  fix x :: "'a" and xs :: "'a list"
  assume HI: "conc xs [] = xs" 
  have "conc (x # xs) [] = x # (conc xs [])" 
    by (simp only: conc.simps(2))
  also have "… = x # xs" 
    using HI by (simp only:)
  finally show "conc (x # xs) [] = x # xs" 
    by this
qed

text ‹--------------------------------------------------------------- 
  Ejemplo 13. (p. 30) Demostrar que 
     longitud (conc xs ys) = longitud xs + longitud ys
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
  apply (induct xs) (* 1. longitud (conc [] ys) =
                          longitud [] + longitud ys
                       2. ⋀a xs.
                             longitud (conc xs ys) =
                             longitud xs + longitud ys ⟹
                             longitud (conc (a # xs) ys) =
                             longitud (a # xs) + longitud ys *) 
   apply simp_all   (* No subgoals! *)
  done  

(* La demostración automática es *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
  by (induct xs) simp_all

(* La demostración declarativa es *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
proof (induct xs)
  show "longitud (conc [] ys) = longitud [] + longitud ys" by simp
next
  fix x xs
  assume HI: "longitud (conc xs ys) = longitud xs + longitud ys"
  have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))" 
    by simp
  also have "… = 1 + longitud (conc xs ys)" 
    by simp
  also have "… = 1 + longitud xs + longitud ys" 
    using HI by simp
  also have "… = longitud (x # xs) + longitud ys" 
    by simp
  finally show "longitud (conc (x # xs) ys) = 
                longitud (x # xs) + longitud ys" 
    by simp
qed

(* La demostración declarativa detallada es *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
proof (induct xs)
  show "longitud (conc [] ys) = longitud [] + longitud ys" 
    by (simp only: conc.simps(1)
                   longitud.simps(1))
next
  fix x xs
  assume HI: "longitud (conc xs ys) = longitud xs + longitud ys"
  have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))" 
    by (simp only: conc.simps(2))
  also have "… = 1 + longitud (conc xs ys)" 
    by (simp only: longitud.simps(2))
  also have "… = 1 + longitud xs + longitud ys" 
    using HI by (simp only:)
  also have "… = longitud (x # xs) + longitud ys" 
    by (simp only: longitud.simps(2))
  finally show "longitud (conc (x # xs) ys) = 
                longitud (x # xs) + longitud ys" 
    by this
qed

section ‹Inducción correspondiente a la definición recursiva ›

text ‹--------------------------------------------------------------- 
  Ejemplo 14. 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 ‹--------------------------------------------------------------- 
  Ejemplo 15. Definir la función
     elimina :: nat ⇒ 'a list ⇒ 'a list
  tal que (elimina n xs) es la lista obtenida eliminando los n primeros
  elementos de xs. Por ejemplo, 
     elimina 2 [a,c,d,b,e] = [d,b,e]
  ------------------------------------------------------------------ ›

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
  "elimina n []           = []"
| "elimina 0 xs           = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

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

text ‹ 
  La definición coge genera el esquema de inducción coge.induct:
     ⟦⋀n. P n []; 
      ⋀x xs. P 0 (x#xs); 
      ⋀n x xs. P n xs ⟹ P (Suc n) (x#xs)⟧
     ⟹ P n x

  Puede verse usando "thm coge.induct". ›

thm coge.induct

text ‹--------------------------------------------------------------- 
  Ejemplo 16. (p. 35) Demostrar que 
     conc (coge n xs) (elimina n xs) = xs
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "conc (coge n xs) (elimina n xs) = xs"
  apply (induct rule: coge.induct) 
      (*  1. ⋀n. conc (coge n []) (elimina n []) = []
          2. ⋀v va. conc (coge 0 (v # va)) (elimina 0 (v # va)) =
                     v # va
          3. ⋀n x xs. conc (coge n xs) (elimina n xs) = xs ⟹
                       conc (coge (Suc n) (x # xs)) 
                            (elimina (Suc n) (x # xs)) =
                       x # xs *)
    apply simp_all
      (* No subgoals! *)
  done

(* La demostración automática es *)
lemma "conc (coge n xs) (elimina n xs) = xs"
  by (induct rule: coge.induct) simp_all

(* La demostración declarativa es *)
lemma "conc (coge n xs) (elimina n xs) = xs"
proof (induct rule: coge.induct)
  fix n
  show "conc (coge n []) (elimina n []) = []" 
    by simp
next
  fix x :: "'a" and xs :: "'a list"
  show "conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs" 
    by simp
next
  fix n and x :: "'a" and xs :: "'a list"
  assume HI: "conc (coge n xs) (elimina n xs) = xs"
  have "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = 
        conc (x#(coge n xs)) (elimina n xs)" 
    by simp
  also have "… = x#(conc (coge n xs) (elimina n xs))" 
    by simp
  also have "… = x#xs" 
    using HI by simp  
  finally show "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = 
                x#xs"
    by simp
qed

text ‹Comentario sobre la demostración anterior:
  · (induct rule: coge.induct) indica que el método de demostración es
    por el esquema de inducción correspondiente a la definición de la
    función coge.
  · Se generan 3 subobjetivos:
    · 1. ⋀n. conc (coge n []) (elimina n []) = []
    · 2. ⋀x xs. conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs
    · 3. ⋀n x xs. 
            conc (coge n xs) (elimina n xs) = xs ⟹
            conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs
›

(* La demostración declarativa detallada es *)
lemma "conc (coge n xs) (elimina n xs) = xs"
proof (induct rule: coge.induct)
  fix n
  show "conc (coge n []) (elimina n []) = []" 
    by (simp only: coge.simps(1)
                   elimina.simps(1)
                   conc.simps(1))
next
  fix x :: "'a" and xs :: "'a list"
  show "conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs" 
    by (simp only: coge.simps(2)
                   elimina.simps(2)
                   conc.simps(1))
next
  fix n and x :: "'a" and xs :: "'a list"
  assume HI: "conc (coge n xs) (elimina n xs) = xs"
  have "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = 
        conc (x#(coge n xs)) (elimina n xs)" 
    by (simp only: coge.simps(3)
                   elimina.simps(3))
  also have "… = x#(conc (coge n xs) (elimina n xs))" 
    by (simp only: conc.simps(2))
  also have "… = x#xs" 
    using HI by (simp only:) 
  finally show "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = 
                x#xs"
    by this
qed

section ‹Razonamiento por casos ›

text ‹ --------------------------------------------------------------- 
  Ejemplo 17. Definir la función
     esVacia :: 'a list ⇒ bool
  tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
     esVacia []  = True
     esVacia [1] = False
  ------------------------------------------------------------------ ›

fun esVacia :: "'a list ⇒ bool" where
  "esVacia []     = True"
| "esVacia (x#xs) = False"

value "esVacia []  = True"
value "esVacia [a] = False"

text ‹--------------------------------------------------------------- 
  Ejemplo 18 (p. 39) . Demostrar que 
     esVacia xs = esVacia (conc xs xs)
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "esVacia xs = esVacia (conc xs xs)"
  apply (cases xs) 
     (* 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs)
        2. ⋀a list. xs = a # list ⟹
                    esVacia xs = esVacia (conc xs xs) *)
   apply simp_all
     (* No subgoals! *)
  done

(* La demostración automática es *)
lemma "esVacia xs = esVacia (conc xs xs)"
  by (cases xs) simp_all

(* La demostración declarativa es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  assume "xs = []"
  then show "esVacia xs = esVacia (conc xs xs)" 
    by simp
next
  fix y ys
  assume "xs = y#ys"
  then show "esVacia xs = esVacia (conc xs xs)" 
    by simp
qed

text ‹Comentarios sobre la demostración anterior:
  · "(cases xs)" es el método de demostración por casos según xs.
  · Se generan dos subobjetivos  correspondientes a los dos
    constructores de listas:
    · 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs)
    · 2. ⋀y ys. xs = y#ys ⟹ esVacia xs = esVacia (conc xs xs)
  · "then" indica "usando la propiedad anterior"
›

(* La demostración declarativa detallada es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  assume "xs = []"
  then show "esVacia xs = esVacia (conc xs xs)" 
    by (simp only: conc.simps(1))
next
  fix y ys
  assume "xs = y#ys"
  then show "esVacia xs = esVacia (conc xs xs)" 
    by (simp only: esVacia.simps(2)
                   conc.simps(2))
qed

(* La demostración declarativa simplificada es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  case Nil
  then show "esVacia xs = esVacia (conc xs xs)" 
    by simp
next
  case Cons
  then show "esVacia xs = esVacia (conc xs xs)" 
    by simp
qed

text ‹
  Comentarios sobre la demostración anterior:
  · "case Nil" es una abreviatura de "assume xs = []"
  · "case Cons" es una abreviatura de "fix y ys assume xs = y#ys"›

(* La demostración con el patrón sugerido es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  case Nil
  then show ?thesis by simp
next
  case (Cons x xs)
  then show ?thesis by simp
qed

section ‹Heurística de generalización ›

text ‹--------------------------------------------------------------- 
  Ejemplo 19. Definir la función
     inversaAc :: 'a list ⇒ 'a list
  tal que (inversaAc xs) es a inversa de xs calculada usando
  acumuladores. Por ejemplo, 
     inversaAc [a,c,b,e] = [e,b,c,a]
  ------------------------------------------------------------------ ›

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
  "inversaAcAux [] ys     = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

definition inversaAc :: "'a list ⇒ 'a list" where
  "inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e] = [e,b,c,a]"

text ‹Lema. [Ejemplo de equivalencia entre las definiciones]
  La inversa de [a,b,c] es lo mismo calculada con la primera definición
  que con la segunda.›

lemma "inversaAc [a,b,c] = inversa [a,b,c]"
  by (simp add: inversaAc_def)

text ‹Nota. [Ejemplo fallido de demostración por inducción]
  El siguiente intento de demostrar que para cualquier lista xs, se
  tiene que  "inversaAc xs = inversa xs" falla.›

lemma "inversaAc xs = inversa xs"
proof (induct xs)
  show "inversaAc [] = inversa []" 
    by (simp add: inversaAc_def)
next
  fix a :: "'b" and xs :: "'b list" 
  assume HI: "inversaAc xs = inversa xs"
  have "inversaAc (a#xs) = inversaAcAux (a#xs) []" 
    by (simp add: inversaAc_def)
  also have "… = inversaAcAux xs [a]" 
    by simp
  also have "… = inversa (a#xs)"
  (* Problema: la hipótesis de inducción no es aplicable. *)
oops

text ‹Nota. [Heurística de generalización]
  Cuando se use demostración estructural, cuantificar universalmente las 
  variables libres (o, equivalentemente, considerar las variables libres
  como variables arbitrarias).

  Lema. [Lema con generalización]
  Para toda lista ys se tiene 
     inversaAcAux xs ys = (inversa xs) @ ys
›

text ‹--------------------------------------------------------------- 
  Ejemplo 20. (p. 44) Demostrar que 
     inversaAcAux xs ys = (inversa xs) @ ys
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "inversaAcAux xs ys = (inversa xs)@ys"
  apply (induct xs arbitrary: ys) 
     (* 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys
        2. ⋀a xs ys.
              (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹
              inversaAcAux (a # xs) ys = inversa (a # xs) @ ys *)
   apply simp_all
     (* No subgoals! *)
  done

(* La demostración automática es *)
lemma "inversaAcAux xs ys = (inversa xs)@ys"
  by (induct xs arbitrary: ys) simp_all

(* La demostración declarativa es *)
lemma
  "inversaAcAux xs ys = (inversa xs) @ ys"
proof (induct xs arbitrary: ys)
  show "⋀ys. inversaAcAux [] ys = (inversa [])@ys" 
    by simp
next
  fix a :: "'b" and xs :: "'b list" 
  assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"
  show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"
  proof -
    fix ys
    have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" 
      by simp
    also have "… = inversa xs@(a#ys)" 
      using HI by simp
    also have "… = inversa (a#xs)@ys" using [[simp_trace]] 
      by simp 
    finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" 
      by simp
  qed
qed

text ‹Comentarios sobre la demostración anterior:
  · "(induct xs arbitrary: ys)" es el método de demostración por
    inducción sobre xs usando ys como variable arbitraria.
  · Se generan dos subobjetivos:
    · 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys
    · 2. ⋀a xs ys. (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹
                    inversaAcAux (a # xs) ys = inversa (a # xs) @ ys
  · Dentro de una demostración se pueden incluir otras demostraciones.
  · Para demostrar la propiedad universal "⋀ys. P(ys)" se elige una
    lista arbitraria (con "fix ys") y se demuestra "P(ys)". ›

text ‹Nota. En el paso "inversa xs@(a#ys) = inversa (a#xs)@ys" se usan
  lemas de la teoría List. Se puede observar, insertano 
     using [[simp_trace]]
  entre la igualdad y by simp, que los lemas usados son 
  · List.append_simps_1: []@ys = ys
  · List.append_simps_2: (x#xs)@ys = x#(xs@ys)
  · List.append_assoc:   (xs @ ys) @ zs = xs @ (ys @ zs)
  Las dos primeras son las ecuaciones de la definición de append.

  En la siguiente demostración se detallan los lemas utilizados.
›

― ‹Demostración aplicativa›
lemma "(inversa xs)@(a#ys) = (inversa (a#xs))@ys"
  apply (simp only: inversa.simps(2))
    (* inversa xs @ (a # ys) = (inversa xs @ [a]) @ ys*)
  apply (simp only: append_assoc)
    (* inversa xs @ (a # ys) = inversa xs @ ([a] @ ys) *)
  apply (simp only: append.simps(2))
    (* inversa xs @ (a # ys) = inversa xs @ (a # ([] @ ys)) *)
  apply (simp only: append.simps(1))
    (* *)
  done

― ‹Demostración declarativa detallada del lema auxiliar›
lemma auxiliar: "(inversa xs)@(a#ys) = (inversa (a#xs))@ys"
proof -
  have "(inversa xs)@(a#ys) = (inversa xs)@(a#([]@ys))" 
    by (simp only: append.simps(1))
  also have "… = (inversa xs)@([a]@ys)" 
    by (simp only: append.simps(2))
  also have "… = ((inversa xs)@[a])@ys" 
    by (simp only: append_assoc)
  also have "… = (inversa (a#xs))@ys" 
    by (simp only: inversa.simps(2))
  finally show ?thesis 
    by this
qed

(* La demostración declarativa detallada es *)
lemma inversaAcAux_es_inversa:
  "inversaAcAux xs ys = (inversa xs) @ ys"
proof (induct xs arbitrary: ys)
  fix ys :: "'b list"
  show "inversaAcAux [] ys = (inversa [])@ys" 
    by (simp only: inversaAcAux.simps(1)
                   inversa.simps(1)
                   append.simps(1))
next
  fix a :: "'b" and xs :: "'b list"
  assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"
  show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"
  proof -
    fix ys
    have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" 
      by (simp only: inversaAcAux.simps(2))
    also have "… = inversa xs@(a#ys)" 
      using HI by (simp only:)
    also have "… = inversa (a#xs)@ys" 
      by (rule auxiliar) 
    finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" 
      by this
  qed
qed

text ‹--------------------------------------------------------------- 
  Ejemplo 21. (p. 43) Demostrar que 
     inversaAc xs = inversa xs
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
corollary "inversaAc xs = inversa xs"
  apply (simp add: inversaAcAux_es_inversa inversaAc_def)
  done 

(* La demostración automática es *)
corollary "inversaAc xs = inversa xs"
  by (simp add: inversaAcAux_es_inversa inversaAc_def)

text ‹Comentario de la demostración anterior:
  · "(simp add: inversaAcAux_es_inversa inversaAc_def)" es el método de 
    demostración por simplificación usando como regla de simplificación 
    las propiedades inversaAcAux_es_inversa e inversaAc_def. ›
 
section ‹Demostración por inducción para funciones de orden superior ›

text ‹ --------------------------------------------------------------- 
  Ejemplo 22. Definir la función
     sum :: nat list ⇒ nat
  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
     sum [3,2,5] = 10
  ------------------------------------------------------------------ ›

fun sum :: "nat list ⇒ nat" where
  "sum []     = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5] = 10"

text ‹--------------------------------------------------------------- 
  Ejemplo 23. Definir la función
     map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
  tal que (map f xs) es la lista obtenida aplicando la función f a los
  elementos de xs. Por ejemplo,
     map (λx. 2*x) [3::nat,2,5] = [6,4,10]
     map ((*) 2) [3::nat,2,5] = [6,4,10]
     map ((+) 2)   [3::nat,2,5] = [5,4,7]
  ------------------------------------------------------------------ ›

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
  "map f []     = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::nat,2,5] = [6,4,10]"
value "map ((*) 2)   [3::nat,2,5] = [6,4,10]"
value "map ((+) 2)   [3::nat,2,5] = [5,4,7]"

text ‹--------------------------------------------------------------- 
  Ejemplo 24. (p. 45) Demostrar que 
     sum (map ((*) 2) xs) = 2 * (sum xs)
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "sum (map ((*) 2) xs) = 2 * (sum xs)"
  apply (induct xs) 
     (* 1. sum (map (( * ) 2) []) = 2 * sum []
        2. ⋀a xs. sum (map (( * ) 2) xs) = 2 * sum xs ⟹
                  sum (map (( * ) 2) (a # xs)) = 2 * sum (a # xs) *)
   apply simp_all
     (* No subgoals! *)
  done

(* La demostración automática es *)
lemma "sum (map ((*) 2) xs) = 2 * (sum xs)"
  by (induct xs) simp_all

(* La demostración declarativa es *)
lemma "sum (map ((*) 2) xs) = 2 * (sum xs)"
proof (induct xs)
  show "sum (map ((*) 2) []) = 2 * (sum [])" by simp
next
  fix a xs
  assume HI: "sum (map ((*) 2) xs) = 2 * (sum xs)"
  have "sum (map ((*) 2) (a#xs)) = sum ((2*a)#(map ((*) 2) xs))" 
    by simp
  also have "… = 2*a + sum (map ((*) 2) xs)" 
    by simp
  also have "… = 2*a + 2*(sum xs)" 
    using HI by simp
  also have "… = 2*(a + sum xs)" 
    by simp
  also have "… = 2*(sum (a#xs))" 
    by simp
  finally show "sum (map ((*) 2) (a#xs)) = 2*(sum (a#xs))" 
    by simp
qed

(* La demostración declarativa detallada es *)
lemma "sum (map ((*) 2) xs) = 2 * (sum xs)"
proof (induct xs)
  show "sum (map ((*) 2) []) = 2 * (sum [])" 
    by (simp only: map.simps(1)
                   sum.simps(1))
next
  fix a xs
  assume HI: "sum (map ((*) 2) xs) = 2 * (sum xs)"
  have "sum (map ((*) 2) (a#xs)) = sum ((2*a)#(map ((*) 2) xs))" 
    by (simp only: map.simps(2))
  also have "… = 2*a + sum (map ((*) 2) xs)" 
    by (simp only: sum.simps(2))
  also have "… = 2*a + 2*(sum xs)" 
    using HI by (simp only:)
  also have "… = 2*(a + sum xs)" 
    find_theorems "_ * (_ + _)"
    by (simp only: add_mult_distrib2)
  also have "… = 2*(sum (a#xs))" 
    by (simp only: sum.simps(2))
  finally show "sum (map ((*) 2) (a#xs)) = 2*(sum (a#xs))" 
    by this
qed

text ‹ --------------------------------------------------------------- 
  Ejemplo 25. (p. 48) Demostrar que 
     longitud (map f xs) = longitud xs
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "longitud (map f xs) = longitud xs"
  apply (induct xs) 
     (* 1. longitud (map f []) = longitud []
        2. ⋀a xs. longitud (map f xs) = longitud xs ⟹
                   longitud (map f (a # xs)) = longitud (a # xs) *)
   apply simp_all
     (* No subgoals! *)
  done

(* La demostración automática es *)
lemma "longitud (map f xs) = longitud xs"
  by (induct xs) simp_all

(* La demostración declarativa es *)
lemma "longitud (map f xs) = longitud xs"
proof (induct xs)
  show "longitud (map f []) = longitud []" 
    by simp
next
  fix a xs
  assume HI: "longitud (map f xs) = longitud xs"
  have "longitud (map f (a#xs)) = longitud (f a # (map f xs))" 
    by simp
  also have "… = 1 + longitud (map f xs)" 
    by simp
  also have "… = 1 + longitud xs" 
    using HI by simp
  also have "… = longitud (a#xs)" 
    by simp
  finally show "longitud (map f (a#xs)) = longitud (a#xs)" 
    by simp
qed

(* La demostración declarativa detallada es *)
lemma "longitud (map f xs) = longitud xs"
proof (induct xs)
  show "longitud (map f []) = longitud []" 
    by (simp only: map.simps(1)
                   longitud.simps(1))
next
  fix a xs
  assume HI: "longitud (map f xs) = longitud xs"
  have "longitud (map f (a#xs)) = longitud (f a # (map f xs))" 
    by (simp only: map.simps(2))
  also have "… = 1 + longitud (map f xs)" 
    by (simp only: longitud.simps(2))
  also have "… = 1 + longitud xs" 
    using HI by (simp only:)
  also have "… = longitud (a#xs)" 
    by (simp only: longitud.simps(2))
  finally show "longitud (map f (a#xs)) = longitud (a#xs)" 
    by this
qed

section ‹Referencias›

text ‹
  · J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3
  · G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about
    programms". 
  · S. Thompson. "Haskell: the Craft of Functional Programming, 3rd
    Edition. Cap. 8 "Reasoning about programms". 
  · L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6. 
    "Reasoning about functional programs". 
›

end