Demostración asistida por ordenador (2011-12) Demostración asistida por ordenador (2011-12)

header {* Tema 8: Distinción de casos e inducción *}

theory Tema_8
imports Main Parity
begin

section {* Razonamiento por distinción de casos *}

subsection {* Distinción de casos booleanos *}

text {*
  Lema. [Demostración por distinción de casos booleanos]
     ¬A ∨ A
*}

lemma "¬A ∨ A" 
proof cases
  assume "A" thus ?thesis ..
next
  assume "¬A" thus ?thesis ..
qed

text {*
  Lema. [Demostración por distinción de casos booleanos nominados]
     ¬A ∨ A
*}

lemma "¬A ∨ A" 
proof (cases "A")
  case True thus ?thesis ..
next
  case False thus ?thesis .. 
qed

text {*
  El método "cases" sobre una fórmula:
  · El método (cases F) es una abreviatura de la aplicación de la regla
       ⟦F ⟹ Q; ¬F ⟹ Q⟧ ⟹ Q  
  · La expresión "case True" es una abreviatura de F.
  · La expresión "case False" es una abreviatura de ¬F.
  · Ventajas de "cases" con nombre: 
    · reduce la escritura de la fórmula y
    · es independiente del orden de los casos.
*}

subsection {* Distinción de casos sobre otros tipos de datos *}

text {*
  Lema. [Distinción de casos sobre listas]
  La longitud del resto de una lista es la longitud de la lista menos 1.
*}

lemma "length(tl xs) = length xs - 1" 
proof (cases xs)
  case Nil thus ?thesis by simp
next
  case Cons thus ?thesis by simp 
qed

text {*
  Distinción de casos sobre listas:
  · El método de distinción de casos se activa con (cases xs) donde xs
    es del tipo lista. 
  · "case Nil" es una abreviatura de 
       "assume Nil: xs =[]".
  · "case Cons" es una abreviatura de 
       "fix ? ?? assume Cons: xs = ? # ??"
    donde ? y ?? son variables anónimas. 

  Lema. [Ejemplo de análisis de casos]
  El resultado de eliminar los n+1 primeros elementos de xs es el mismo
  que eliminar los n primeros elementos del resto de xs.  
*}

lemma "drop (n + 1) xs = drop n (tl xs)"
proof (cases xs)
  case Nil thus "drop (n + 1) xs = drop n (tl xs)" by simp
next
  case Cons thus "drop (n + 1) xs = drop n (tl xs)" by simp
qed

text {*
  La función drop está definida en la teoría List de forma que
  (drop n xs) la lista obtenida eliminando en xs} los n primeros
  elementos. Su definición es la siguiente  
     primrec drop:: "nat => 'a list => 'a list" where
     drop_Nil:  "drop n [] = []" |
     drop_Cons: "drop n (x#xs) = (case n of 
                                    0 => x#xs | 
                                    Suc(m) => drop m xs)"
*}

section {* Inducción matemática *}

text {*
  [Principio de inducción matemática]
  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
  
  Ejemplo de demostración por inducción: Usaremos el principio de
  inducción matemática para demostrar que 
     1 + 3 + ... + (2n-1) = n^2

  Definición. [Suma de los primeros impares] 
  (suma_impares n) la suma de los n números impares.    
*}

primrec suma_impares :: "nat ⇒ nat" where
"suma_impares 0 = 0" |
"suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n"

text {* 
  Lema. [Ejemplo de suma de impares]
  La suma de los 3 primeros números impares es 9.
*}

lemma "suma_impares 2 = 4"
by (simp add: suma_impares_def)

text {*
  La suma de los 3 primero número impares se puede calcular mediante "value". 
*}

value "suma_impares 3"

text {*
  Lema. [Ejemplo de demostración por inducción matemática]
  La suma de los n primeros números impares es n^2.
  
  Demostración automática: Por inducción en n.
*}

lemma "suma_impares n = n * n"
by (induct n) simp_all

text {*
  En la demostración "by (induct n) simp_all" se aplica inducción en n y
  los dos casos se prueban por simplificación.  
  
  Demostración del lema anterior usando patrones.
*}

lemma "suma_impares n = n * n" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix n assume "?P n"
  thus "?P (Suc n)" by simp
qed

text {*
  Patrones: Cualquier fórmula seguida de (is patrón) equipara el patrón
  con la fórmula.

  Demostración del lema anterior con patrones y razonamiento ecuacional.
*}

lemma "suma_impares n = n * n" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix n assume HI: "?P n"
  have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n" by simp
  also have "… = (2 * (Suc n) - 1) + n * n" using HI by simp
  also have "… = n * n + 2 * n + 1" by simp
  finally show "?P (Suc n)" by simp
qed

text {*
  Demostración del lema anterior por inducción y razonamiento ecuacional.
*}

lemma "suma_impares n = n * n"
proof (induct n)
  show "suma_impares 0 = 0 * 0" by simp
next
  fix n assume HI: "suma_impares n = n * n"
  have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n" by simp
  also have "… = (2 * (Suc n) - 1) + n * n" using HI by simp
  also have "… = n * n + 2 * n + 1" by simp
  finally show "suma_impares (Suc n) = (Suc n) * (Suc n)" by simp
qed

text {* 
  Definición. [Números pares]
  Un número natural n es par si existe un natural m tal que n=m+m. 
*}

definition par ::  "nat ⇒ bool" where
  "par n ≡ ∃m. n=m+m"

text {* 
  Lema. [Ejemplo de inducción y existenciales]
  Para todo número natural n, se verifica que n*(n+1) par.
*}

lemma 
  fixes n :: "nat"
  shows "par (n*(n+1))"
proof (induct n)
  show "par (0*(0+1))" by (simp add:par_def)
next
  fix n assume "par (n*(n+1))"
  hence "∃m. n*(n+1) = m+m" by (simp add:par_def)
  then obtain m where m: "n*(n+1) = m+m" by (rule exE)
  hence "(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)" by auto
  hence "∃m. (Suc n)*((Suc n)+1) = m+m" by (rule exI)
  thus "par ((Suc n)*((Suc n)+1))" by (simp add:par_def)
qed

text {*
  En Isabelle puede demostrarse de manera más simple un lema equivalente usando
  en lugar de la función "par" la función "even" definida en la teoría Parity.
*}

lemma 
  fixes n :: "nat"
  shows "even (n*(n+1))"
by auto

text {*
  Para completar la demostración basta demostrar la equivalencia de las
  funciones "par" y "even". 
*}

lemma 
  fixes n :: "nat"
  shows "par n = even n"
proof - 
  have "par n = (∃m. n = m+m)" by (simp add:par_def)
  thus "par n = even n" by presburger
qed

text {*
  En la demostración anterior hemos usado la táctica "presburger" que
  corresponde a la aritmética de Presburger.
*}

section {* Inducción estructural *}

text {*
  Inducción estructural]
  · En Isabelle puede hacerse inducción estructural sobre cualquier tipo
    recursivo.
  · La inducción matemática es la inducción estructural sobre el tipo de
    los naturales.
  · El esquema de inducción estructural sobre listas es
    · list.induct: ⟦P []; ⋀x ys. P ys ⟹ P (x # ys)⟧ ⟹ P zs
  · 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 una lista que también tiene la
    propiedad. 

  Concatenación de listas:
  En la teoría List.thy está definida la concatenación de listas (que
  se representa por @) como sigue
    primrec
      append_Nil:  "[]@ys = ys"
      append_Cons: "(x#xs)@ys = x#(xs@ys)"

  Lema. [Ejemplo de inducción sobre listas]
  La concatenación de listas es asociativa.
  
  Demostración automática del lema.
*}

lemma conc_asociativa_1: "xs @ (ys @ zs) = (xs @ ys) @ zs"
by (induct xs) simp_all

text {*
  Demostración estructurada del lema anterior.
*}

lemma conc_asociativa: "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  show "[] @ (ys @ zs) = ([] @ ys) @ zs"
  proof -
    have "[] @ (ys @ zs) = ys @ zs" by simp
    also have "… = ([] @ ys) @ zs" by simp
    finally show ?thesis .
  qed
next
  fix x xs
  assume HI: "xs @ (ys @ zs) = (xs @ ys) @ zs"
  show "(x#xs) @ (ys @ zs) = ((x#xs) @ ys) @ zs"
  proof -
    have "(x#xs) @ (ys @ zs) = x#(xs @ (ys @ zs))" by simp
    also have "… = x#((xs @ ys) @ zs)" using HI by simp
    also have "… = (x#(xs @ ys)) @ zs" by simp
    also have "… = ((x#xs) @ ys) @ zs" by simp
    finally show ?thesis .
  qed
qed

text {* 
  Ejercicio. [Árboles binarios]
  Definir un tipo de dato para los árboles binarios.
*}

datatype 'a arbol = Hoja "'a" 
                  | Nodo "'a" "'a arbol" "'a arbol"

text {* 
  Ejercicio. [Imagen especular]
  Definir la función "espejo" que aplicada a un árbol devuelve su imagen
  especular.  
*}

primrec espejo :: "'a arbol ⇒ 'a arbol" where
  "espejo (Hoja a) = (Hoja a)"
| "espejo (Nodo f x y) = (Nodo f (espejo y) (espejo x))"

text {* 
  Ejercicio. [La imagen especular es involutiva]
  Demostrar que la función "espejo" involutiva; es decir, para cualquier
  árbol t, se tiene que 
     espejo (espejo(t)) = t.
  
  Demostración automática del lema.
*}

lemma espejo_involutiva_1: "espejo(espejo(t)) = t"
by (induct t) auto

text {*
  Demostración estructurada del lema.
*}

lemma espejo_involutiva: "espejo(espejo(t)) = t" (is "?P t")
proof (induct t)
  fix x :: 'a show "?P (Hoja x)" by simp 
next
  fix t1 :: "'a arbol" assume h1: "?P t1"
  fix t2 :: "'a arbol" assume h2: "?P t2"
  fix x :: 'a
  show "?P (Nodo x t1 t2)" 
  proof -
    have "espejo(espejo(Nodo x t1 t2)) = espejo(Nodo x (espejo t2) (espejo t1))"
      by simp
    also have "… = Nodo x (espejo (espejo t1)) (espejo (espejo t2))" by simp
    also have "… = Nodo x t1 t2" using h1 h2 by simp 
    finally show ?thesis .
 qed
qed

text {* 
  Ejercicio. [Aplanamiento de árboles]
  Definir la función "aplana" que aplane los árboles recorriéndolos en
  orden infijo.  
*}

primrec aplana :: "'a arbol ⇒ 'a list" where
  "aplana (Hoja a) = [a]"
| "aplana (Nodo x t1 t2) = (aplana t1)@[x]@(aplana t2)"

text {* 
  Ejercicio. [Aplanamiento de la imagen especular] Demostrar que
     aplana (espejo t) = rev (aplana t)
  
  Demostración automática del lema.
*}

lemma "aplana (espejo t) = rev (aplana t)"
by (induct t) auto

text {* 
  Demostración estructurada del lema anterior.
*}

lemma "aplana (espejo t) = rev (aplana t)" (is "?P t")
proof (induct t)
  fix x :: 'a 
  show "?P (Hoja x)" by simp 
next
  fix t1 :: "'a arbol" assume h1: "?P t1"
  fix t2 :: "'a arbol" assume h2: "?P t2"
  fix x :: 'a
  show "?P (Nodo x t1 t2)" 
  proof -
    have "aplana (espejo (Nodo x t1 t2)) = 
          aplana (Nodo x (espejo t2) (espejo t1))" by simp
    also have "… = (aplana(espejo t2))@[x]@(aplana(espejo t1))" by simp
    also have "… = (rev(aplana t2))@[x]@(rev(aplana t1))" using h1 h2 by simp
    also have "… = rev((aplana t1)@[x]@(aplana t2))" by simp
    also have "… = rev(aplana (Nodo x t1 t2))" by simp
    finally show ?thesis .
 qed
qed

end