Razonamiento por casos y por inducci¢n

chapter ‹Tema 7: Razonamiento por casos y por inducción›

theory T7_Razonamiento_por_casos_y_por_induccion
imports Main HOL.Parity
begin

text ‹En este tema se amplían los métodos de demostración por casos y 
  por inducción iniciados en el tema anterior.›

section ‹Razonamiento por distinción de casos›

subsection ‹Distinción de casos booleanos›

text ‹Ejemplo de demostración por distinción de casos booleanos:
  Demostrar "¬A ∨ A".›

― ‹La demostración estructurada es›
lemma "¬A ∨ A" 
proof cases
  assume "A" 
  then show "¬A ∨ A" ..
next
  assume "¬A" 
  then show "¬A ∨ A" ..
qed

text ‹Comentarios de la demostración anterior:
  · "proof cases" indica que el método de demostración será por
    distinción de casos. 
  · Se generan 2 casos:
       1. ?P ⟹ ¬A ∨ A
       2. ¬?P ⟹ ¬A ∨ A
    donde ?P es una variable sobre las fórmulas.
  · (assume "A") indica que se está usando "A" en lugar de la variable
    ?P.
  · "then" indica usando la fórmula anterior.
  · ".." indica usando la regla lógica necesaria (las reglas lógicas se
    estudiarán en los siguientes temas).
  · "next" indica el siguiente caso (se puede observar cómo ha
    sustituido ¬?P por ¬A.›

― ‹La demostración aplicativa es›
lemma "¬A ∨ A" 
  apply cases
   apply simp_all
  done

― ‹La demostración automática es›
lemma "¬A ∨ A" 
  by cases simp_all

lemma "¬A ∨ A"
  by auto

text ‹Ejemplo de demostración por distinción de casos booleanos con 
  nombres: 
  Demostrar "¬A ∨ A".›

― ‹La demostración estructurada es›
lemma "¬A ∨ A" 
proof (cases "A")
  case True 
  then show "¬A ∨ A" ..
next
  case False 
  then show "¬A ∨ A" .. 
qed

text ‹Comentarios sobre la demostración anterior:
  · (cases "A") indica que la demostración se hará por casos según los
    distintos valores de "A".
  · Como "A" es una fórmula, sus posibles valores son verdadero o falso.
  · "case True" indica que se está suponiendo que A es verdadera. Es
    equivalente a "assume A".
  · "case False" indica que se está suponiendo que A es falsa. Es
    equivalente a "assume ¬A".
  · En general, 
    · 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 ‹Ejemplo de distinción de casos sobre listas: 
  Demostrar que la longitud del resto de una lista es la longitud de la
  lista menos 1.›

― ‹La demostración estructurada es›
lemma "length (tl xs) = length xs - 1" 
proof (cases xs)
  assume "xs = []"
  then have "length (tl xs) = 0"
    by simp
  also have "… = 0 - 1"
    by simp
  also have "… = length xs - 1"
    using ‹xs = []›
    by simp
  finally show "length (tl xs) = length xs - 1" 
    by this
next
  fix y ys
  assume "xs = y#ys"
  then have "length (tl xs) = length ys"
    by simp
  also have "… = (1 + length ys) - 1"
    by simp
  also have "… = length (y#ys) - 1"
    by simp 
  also have "… = length xs - 1"
    using ‹xs = y#ys›
    by simp
  finally show "length (tl xs) = length xs - 1" 
    by this
qed

text ‹Comentarios sobre la demostración anterior:
  · "(cases xs)" indica que la demostración se hará por casos sobre los
    posibles valores de xs.
  · Como xs es una lista, sus posibles valores son la lista vacía ([]) o
    una lista no vacía (de la forma (y#ys)).
  · Se generan 2 casos:
       1. xs = [] ⟹ length (tl xs) = length xs - 1
       2. ⋀a list. xs = a # list ⟹ length (tl xs) = length xs - 1›

― ‹La demostración detallada es›
lemma "length (tl xs) = length xs - 1" 
proof (cases xs)
  assume "xs = []"
  then have "length (tl xs) = 0"
    by (simp only: list.sel(2)
                   list.size(3))
  also have "… = 0 - 1"
    by (simp only: natural_zero_minus_one)
  also have "… = length xs - 1"
    using ‹xs = []›
    by (simp only: list.size(3))
  finally show "length (tl xs) = length xs - 1" 
    by this
next
  fix y ys
  assume "xs = y#ys"
  then have "length (tl xs) = length ys"
    by (simp only: list.sel(3))
  also have "… = length (y#ys) - 1"
    by (simp only: length_Cons)
  also have "… = length xs - 1"
    using ‹xs = y#ys›
    by (simp only:)
  finally show "length (tl xs) = length xs - 1" 
    by this
qed

― ‹La demostración simplificada es› 
lemma "length (tl xs) = length xs - 1" 
proof (cases xs)
  case Nil 
  then show ?thesis by simp
next
  case Cons 
  then show ?thesis 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"
  · ?thesis es una abreviatura de la conclusión del lema.›

― ‹La demostración aplicativa es›
lemma "length (tl xs) = length xs - 1" 
  apply (cases xs)
   apply simp_all
  done

― ‹La demostración automática es›
lemma "length (tl xs) = length xs - 1" 
  by (cases xs) simp_all

text ‹En el siguiente ejemplo vamos a demostrar una propiedad de la 
  función drop que está definida en la teoría List de forma que 
  (drop n xs) es la lista obtenida eliminando en xs los n primeros 
  elementos. Su definición es la siguiente   
     drop_Nil:  "drop n []     = []" 
     drop_Cons: "drop n (x#xs) = (case n of 
                                    0 => x#xs | 
                                    Suc(m) => drop m xs)" ›

text ‹Ejemplo de análisis de casos:
  Demostrar que el resultado de eliminar los n+1 primeros elementos de
  xs es el mismo que eliminar los n primeros elementos del resto de xs.›

― ‹La demostración estructurada es›
lemma "drop (n + 1) xs = drop n (tl xs)"
proof (cases xs)
  case Nil 
  then show ?thesis by simp
next
  case Cons 
  then show ?thesis by simp
qed

― ‹La demostración aplicativa es›
lemma "drop (n + 1) xs = drop n (tl xs)"
  apply (cases xs)
   apply simp_all
  done

― ‹La demostración automática es›
lemma "drop (n + 1) xs = drop n (tl xs)"
  by (cases xs) simp_all

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

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

text ‹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. Por ejemplo,
     suma_impares 3  =  9
›

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

value "suma_impares 3"

text ‹  Ejemplo de demostración por inducción matemática:
  Demostrar que la suma de los n primeros números impares es n^2.›

― ‹Demostración estructurada 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
  also have "… = (Suc n) * (Suc n)" 
    by simp
  finally show "suma_impares (Suc n) = (Suc n) * (Suc n)" 
    by this
qed

― ‹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
  also have "… = Suc n * Suc n"
    by simp
  finally show "?P (Suc n)" 
    by this
qed

text ‹Comentario sobre la demostración anterior:
  · Con la expresión
       "suma_impares n = n * n" (is "?P n")
    se abrevia "suma_impares n = n * n" como "?P n". Por tanto, 
       "?P 0"       es una abreviatura de "suma_impares 0 = 0 * 0"
       "?P (Suc n)" es una abreviatura de 
                    "suma_impares (Suc n) = (Suc n) * (Suc n)"
  · En general, cualquier fórmula seguida de (is patrón) equipara el
    patrón con la fórmula. ›

― ‹La demostración usando patrones es›
lemma "suma_impares n = n * n" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix n 
  assume "?P n"
  then show "?P (Suc n)" by simp
qed
  
― ‹La demostración aplicativa es›
lemma "suma_impares n = n * n"
  apply (induct n)
   apply simp_all
  done

― ‹La demostración automática es›
lemma "suma_impares n = n * n"
  by (induct n) simp_all

text ‹Ejemplo de definición con existenciales. 
  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 ‹Ejemplo de inducción y existenciales: 
  Demostrar que para todo número natural n, se verifica que n*(n+1) 
  es par.›

― ‹Demostración estructurada por inducción›
lemma "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))"
  then have "∃m. n*(n+1) = m+m" 
    by (simp add: par_def)
  then obtain m where m: "n*(n+1) = m+m" 
    by (rule exE)
  then have "(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)" 
    by simp
  then have "∃p. (Suc n)*((Suc n)+1) = p+p" 
    by (rule exI)
  then show "par ((Suc n)*((Suc n)+1))" 
    by (simp add: par_def)
qed

― ‹Demostración casi detallada por inducción›
lemma "par (n*(n+1))"
proof (induct n)
  have "(0::nat) = 0 + 0"
    by (simp only: add_0)
  then have "∃m. (0::nat) = m + m"
    by (rule exI)
  then have "par 0"
    by  (simp only: par_def)
  then show "par (0*(0+1))"
    by (simp only: mult_0) 
next
  fix n 
  assume "par (n*(n+1))"
  then have "∃m. n*(n+1) = m+m" 
    by (simp only: par_def)
  then obtain m where m: "n*(n+1) = m+m" 
    by (rule exE)
  then have "(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)" 
    by simp
  then have "∃p. (Suc n)*((Suc n)+1) = p+p" 
    by (rule exI)
  then show "par ((Suc n)*((Suc n)+1))" 
    by (simp only: par_def)
qed

― ‹Demostración aplicativa por inducción›
lemma "par (n*(n+1))"
  apply (induct n)
   apply (simp add: par_def)
  apply (simp add: par_def)
  apply arith
  done

― ‹Demostración automática›
lemma "par (n*(n+1))"
  by (induct n) (auto simp add: par_def, arith)

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 por
     even x ⟷ x mod 2 = 0 ›

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

text ‹Comentarios sobre la demostración anterior:
  · Para poder usar la función "even" de la librería Parity es necesario
    importar dicha librería. Por ello, antes del inicio de la teoría
    aparece 
       imports Main HOL.Parity 
›

text ‹Para completar la demostración basta demostrar la equivalencia de 
  las funciones "par" y "even".›

lemma "par n = even n"
proof - 
  have "par n = (∃m. n = m+m)" 
    by (simp only: par_def)
  then show "par n = even n" 
    (* try *) 
    by presburger
qed

text ‹Comentarios sobre la demostración anterior:
  · "by presburger" indica que se use como método de demostración el
    algoritmo de decisión de la aritmética de Presburger.›

― ‹Demostración declarativa›
lemma "par n = even n"
  apply (unfold par_def)
  apply presburger
  done

― ‹Demostración automática›
lemma "par n = even n"
  by (simp only: par_def, presburger)

section ‹Recursión general. La función de Ackermann›

text ‹El objetivo de esta sección es mostrar el uso de las definiciones
  recursivas generales y sus esquemas de inducción. Como ejemplo se usa 
  la función de Ackermann (se puede consultar información sobre dicha 
  función en http://en.wikipedia.org/wiki/Ackermann_function).

  Definición.  La función de Ackermann se define por
    A(m,n) = n+1,             si m=0,
             A(m-1,1),        si m>0 y n=0,
             A(m-1,A(m,n-1)), si m>0 y n>0
  para todo los números naturales. 

  La función de Ackermann es recursiva, pero no es primitiva recursiva.›

fun ack :: "nat ⇒ nat ⇒ nat" where
  "ack 0       n       = n+1" 
| "ack (Suc m) 0       = ack m 1" 
| "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"

― ‹Ejemplo de evaluación›
value "ack 2 3" (* devuelve 9 *)

text ‹Esquema de inducción correspondiente a una función:
  · Al definir una función recursiva general se genera una regla de
    inducción. En la definición anterior, la regla generada es
    ack.induct: 
       ⟦⋀n. P 0 n; 
        ⋀m. P m 1 ⟹ P (Suc m) 0;
        ⋀m n. ⟦P (Suc m) n; P m (ack (Suc m) n)⟧ ⟹ P (Suc m) (Suc n)⟧
       ⟹ P a b
›

text ‹Ejemplo de demostración por la inducción correspondiente a una 
  función:
  Demostrar que para todos m y n, A(m,n) > n.› 

― ‹La demostración detallada es›
lemma "ack m n > n"
proof (induct m n rule: ack.induct)
  fix n
  show "ack 0 n > n" 
    by (simp only: ack.simps(1))
next
  fix m 
  assume "ack m 1 > 1"
  then show "ack (Suc m) 0 > 0" 
    by (simp only: ack.simps(2))
next  
  fix m n
  assume "n < ack (Suc m) n" 
     and "ack (Suc m) n < ack m (ack (Suc m) n)"
  then show "Suc n < ack (Suc m) (Suc n)" 
    by (simp only: ack.simps(3))
qed

text ‹Comentarios sobre la demostración anterior:
  · (induct m n rule: ack.induct) indica que el método de demostración
    es el esquema de recursión correspondiente a la definición de 
    (ack m n).
  · Se generan 3 casos:
    1. ⋀n. n < ack 0 n
    2. ⋀m. 1 < ack m 1 ⟹ 0 < ack (Suc m) 0
    3. ⋀m n. ⟦n < ack (Suc m) n; 
              ack (Suc m) n < ack m (ack (Suc m) n)⟧
             ⟹ Suc n < ack (Suc m) (Suc n)
›

― ‹La demostración automática es›
lemma "ack m n > n"
  by (induct m n rule: ack.induct) auto

end