LMF2014: Razonamiento por casos y por inducción en Isabelle/HOL

En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado cómo demostrar por casos o por inducción propiedade de programas funcionales con Isabelle/HOL.

La teoría correspondiente es

header {* Tema 14: Razonamiento por casos y por inducción *}

theory T14
imports Main
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 automática es"
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 
  thus "¬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 detallada es"
lemma "length (tl xs) = length xs - 1" 
proof (cases xs)
  assume "xs = []"
  then show "length (tl xs) = length xs - 1" by simp
next
  fix y ys
  assume "xs = y#ys"
  then show "length(tl xs) = length xs - 1" by simp 
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 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 automática es"
lemma "length (tl xs) = length xs - 1" 
by auto

text {*
  Een 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) 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 detallada 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 automática es"
lemma "drop (n + 1) xs = drop n (tl xs)"
by (cases xs) auto

section {* Demostraciones por inducción y patrones *}

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 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

-- "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 {*
  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 automática es"
lemma "suma_impares n = n * n"
by (induct n) auto


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. 
  · En Isabelle el principio de inducción sobre listas está formalizado
    mediante el teorema list.induct que puede verse con 
       thm list.induct
*}

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

text {*
  Lema. [Ejemplo de inducción sobre listas]
  Demostrar que la concatenación de listas es asociativa.
*}

-- "La demostración estructurada es"
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

-- "La demostración automática es"
lemma conc_asociativa_1: "xs @ (ys @ zs) = (xs @ ys) @ zs"
by (induct xs) auto

text {* 
  Ejemplo de definición de tipos recursivos:
  Definir un tipo de dato para los árboles binarios.
*}

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

text {* 
  Ejemplo de definición sobre árboles binarios:
  Definir la función "espejo" que aplicada a un árbol devuelve su imagen
  especular.  
*}

fun espejo :: "'a arbolB ⇒ 'a arbolB" where
  "espejo (Hoja x) = (Hoja x)"
| "espejo (Nodo x i d) = (Nodo x (espejo d) (espejo i))"

value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))"
-- "= Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))"

text {* 
  Ejemplo de demostración sobre árboles binarios:
  Demostrar que la función "espejo" es involutiva; es decir, para
  cualquier árbol a, se tiene que 
     espejo(espejo(a)) = a.
*}

-- "La demostración estructurada es"
lemma espejo_involutiva:
  fixes a :: "'b arbolB" 
  shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (Hoja x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "espejo(espejo(Nodo x i d)) = espejo(Nodo x (espejo d) (espejo i))"
      by simp
    also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" by simp
    also have "… = Nodo x i d" using h1 h2 by simp 
    finally show ?thesis .
 qed
qed

text {*
  Comentarios sobre la demostración anterior:
  · (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario
    cuyos elementos son de tipo b". 
  · (induct a) indica que el método de demostración es por inducción
    en el árbol binario a.
  · Se generan dos casos:
    1. ⋀a. espejo (espejo (Hoja a)) = Hoja a
    2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; 
                   espejo (espejo a3) = a3⟧
                  ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3
*}

-- "La demostración automática es"
lemma espejo_involutiva_1: 
  "espejo (espejo a ) = a"
by (induct a) auto

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

fun aplana :: "'a arbolB ⇒ 'a list" where
  "aplana (Hoja x)     = [x]"
| "aplana (Nodo x i d) = (aplana i) @ [x] @ (aplana d)"

value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))"
-- "= [c, b, d, a, e]"

text {* 
  Ejemplo. [Aplanamiento de la imagen especular] Demostrar que
     aplana (espejo a) = rev (aplana a)
*}

-- "La demostración estructurada es"
lemma 
  fixes a :: "'b arbolB"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (Hoja x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "aplana (espejo (Nodo x i d)) = 
          aplana (Nodo x (espejo d) (espejo i))" by simp
    also have "… = (aplana(espejo d))@[x]@(aplana(espejo i))" by simp
    also have "… = (rev(aplana d))@[x]@(rev(aplana i))" using h1 h2 by simp
    also have "… = rev((aplana i)@[x]@(aplana d))" by simp
    also have "… = rev(aplana (Nodo x i d))" by simp
    finally show ?thesis .
 qed
qed

-- "La demostración automática es"
lemma "aplana (espejo a) = rev (aplana a)"
by (induct a) auto

section {* Heurísticas para la inducción *}

text {*
  Definición. [Definición recursiva de inversa]
  (inversa xs) la inversa de la lista xs. Por ejemplo,
     inversa [a,b,c] = [c,b,a] 
*}

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

value "inversa [a,b,c]"

text {* 
  Definición. [Definición de inversa con acumuladores]
  (inversaAc xs) es la inversa de la lista xs calculada con
  acumuladores. Por ejemplo,
     inversaAc [a,b,c]       = [c,b,a] 
     inversaAcAux [a,b,c] [] = [c,b,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 "inversaAcAux [a,b,c] []"
value "inversaAc [a,b,c]"

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 xs 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
*}

-- "La demostración estructurada es"
lemma inversaAcAux_es_inversa:
  "inversaAcAux xs ys = (inversa xs)@ys"
proof (induct xs arbitrary: ys)
  show "⋀ys. inversaAcAux [] ys = (inversa [])@ys" by simp
next
  fix a xs 
  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

-- "la demostración automática es"
lemma inversaacaux_es_inversa_1:
  "inversaacaux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

text {*
  corolario.  para cualquier lista xs, se tiene que
     inversaac xs = inversa xs
*}

corollary "inversaac xs = inversa xs"
by (simp add: inversaacaux_es_inversa inversaac_def)

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.
*}

lemma "(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 .
qed

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
next
  fix m 
  assume "ack m 1 > 1"
  then show "ack (Suc m) 0 > 0" by simp
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
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

section {* Recursión mutua e inducción *}

text {*
  Nota. [Ejemplo de definición de tipos mediante recursión cruzada]
  · Un árbol de tipo a es una hoja o un nodo de tipo a junto con un
    bosque de tipo a.
  · Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo
    un árbol de tipo a a un bosque de tipo a.
*}

datatype 'a arbol = Hoja | Nodo "'a" "'a bosque"
     and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"

text {*
  Regla de inducción correspondiente a la recursión cruzada:
  La regla de inducción sobre árboles y bosques es arbol_bosque.induct:
     ⟦P1 Hoja; 
      ⋀x b. P2 b ⟹ P1 (Nodo x b); 
      P2 Vacio;
      ⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ 
     ⟹ P1 a ∧ P2 b
*}

text {* 
  Ejemplos de definición por recursión cruzada:
  · aplana_arbol a) es la lista obtenida aplanando el árbol a.   
  · (aplana_bosque b) es la lista obtenida aplanando el bosque b.   
  · (map_arbol a h) es el árbol obtenido aplicando la función h a
    todos los nodos del árbol a.   
  · (map_bosque b h) es el bosque obtenido aplicando la función h a
    todos los nodos del bosque b. 
*}

fun aplana_arbol :: "'a arbol ⇒ 'a list" and 
    aplana_bosque :: "'a bosque ⇒ 'a list" where
  "aplana_arbol Hoja = []"
| "aplana_arbol (Nodo x b) = x#(aplana_bosque b)"
| "aplana_bosque Vacio = []"
| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"

fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and
    map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where
  "map_arbol  f Hoja        = Hoja"
| "map_arbol  f (Nodo x b)  = Nodo (f x) (map_bosque f b)"
| "map_bosque f Vacio       = Vacio"
| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"

text {*
  Ejemplo de demostración por inducción cruzada:
  Demostrar que:
  · aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
  · aplana_bosque (map_bosque f b) = map f (aplana_bosque b)
*}

-- "La demostración detallada es"
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
  show "aplana_arbol (map_arbol f Hoja ) = map f (aplana_arbol Hoja)" 
    by simp
next
  fix x b
  assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_arbol (map_arbol f (Nodo x b)) = 
        aplana_arbol (Nodo (f x) (map_bosque f b))" by simp
  also have "… = (f x)#(aplana_bosque (map_bosque f b))" by simp
  also have "… = (f x)#(map f (aplana_bosque b))" using HI by simp
  also have "… = map f (aplana_arbol (Nodo x b))" by simp
  finally show "aplana_arbol (map_arbol f (Nodo x b))
                = map f (aplana_arbol (Nodo x b))" .
next
  show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" 
    by simp
next
  fix a b
  assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
     and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_bosque (map_bosque f (ConsB a b)) = 
        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp
  also have "… = aplana_arbol(map_arbol f a)@aplana_bosque(map_bosque f b)" 
    by simp
  also have "… = (map f (aplana_arbol a))@(map f (aplana_bosque b))" 
    using HI1 HI2 by simp
  also have "… = map f (aplana_bosque (ConsB a b))" by simp
  finally show "aplana_bosque (map_bosque f (ConsB a b)) 
                = map f (aplana_bosque (ConsB a b))" by simp
qed

text {*
  Comentarios sobre la demostración anterior:
  · (induct_tac a and b) indica que el método de demostración es por
    inducción cruzada sobre a y b.
  · Se generan 4 casos:
    1. aplana_arbol (map_arbol arbol.Hoja h) = map h (aplana_arbol arbol.Hoja)
    2. ⋀a bosque.
          aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹
          aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =
          map h (aplana_arbol (arbol.Nodo a bosque))
    3. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
    4. ⋀arbol bosque.
          ⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);
           aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧
          ⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =
             map h (aplana_bosque (ConsB arbol bosque))
*}

-- "La demostración automática es"
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
by (induct_tac a and b) auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

292

293

294

295

296

297

298

299

300

301

302

303

304

305

306

307

308

309

310

311

312

313

314

315

316

317

318

319

320

321

322

323

324

325

326

327

328

329

330

331

332

333

334

335

336

337

338

339

340

341

342

343

344

345

346

347

348

349

350

351

352

353

354

355

356

357

358

359

360

361

362

363

364

365

366

367

368

369

370

371

372

373

374

375

376

377

378

379

380

381

382

383

384

385

386

387

388

389

390

391

392

393

394

395

396

397

398

399

400

401

402

403

404

405

406

407

408

409

410

411

412

413

414

415

416

417

418

419

420

421

422

423

424

425

426

427

428

429

430

431

432

433

434

435

436

437

438

439

440

441

442

443

444

445

446

447

448

449

450

451

452

453

454

455

456

457

458

459

460

461

462

463

464

465

466

467

468

469

470

471

472

473

474

475

476

477

478

479

480

481

482

483

484

485

486

487

488

489

490

491

492

493

494

495

496

497

498

499

500

501

502

503

504

505

506

507

508

509

510

511

512

513

514

515

516

517

518

519

520

521

522

523

524

525

526

527

528

529

530

531

532

533

534

535

536

537

538

539

540

541

542

543

544

545

546

547

548

549

550

551

552

553

554

555

556

557

558

559

560

561

562

563

564

565

566

567

568

569

570

571

572

573

574

575

576

577

578

579

580

581

582

583

584

585

586

587

588

589

590

591

592

593

594

595

596

597

598

599

600

601

602

603

604

605

606

607

608

609

610

611

612

613

614

615

616

617

618

619

620

621

622

623

624

625

626

627

628

629

630

631

632

633

634

635

636

637

638

639

640

641

642

643

644

645

646

647

648

649

650

651

652

653

654

655

656

657

658

659

660

661

662

663

664

665

666

667

668

669

670

671

672

673

674

675

676

677

678

679

680

681

682

683

684

685

686

687

688

689

690

691

692

693

694

695

696

697

698

699

700

701

702

703

704

705

706

707

708

709

710

711

712

713

714

715

716

717

718

719

720

721

722

723

724

725

726

727

728

729

730

731

732

733

734

header {* Tema 14: Razonamiento por casos y por inducción *}

theory T14

imports Main

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" ..

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 automática es"

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" ..

case False

thus "¬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 detallada es"

lemma "length (tl xs) = length xs - 1"

proof (cases xs)

assume "xs = []"

then show "length (tl xs) = length xs - 1" by simp

fix y ys

assume "xs = y#ys"

then show "length(tl xs) = length xs - 1" by simp

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 simplificada es"

lemma "length (tl xs) = length xs - 1"

proof (cases xs)

case Nil

then show ?thesis by simp

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 automática es"

lemma "length (tl xs) = length xs - 1"

by auto

text {*

Een 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) 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 detallada es"

lemma "drop (n + 1) xs = drop n (tl xs)"

proof (cases xs)

case Nil

then show ?thesis by simp

case Cons

then show ?thesis by simp

qed

-- "La demostración automática es"

lemma "drop (n + 1) xs = drop n (tl xs)"

by (cases xs) auto

section {* Demostraciones por inducción y patrones *}

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 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

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

-- "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

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 {*

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

fix n

assume "?P n"

then show "?P (Suc n)" by simp

qed

-- "La demostración automática es"

lemma "suma_impares n = n * n"

by (induct n) auto

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.

· En Isabelle el principio de inducción sobre listas está formalizado

mediante el teorema list.induct que puede verse con

thm list.induct

text {*

Concatenación de listas:

En la teoría List.thy está definida la concatenación de listas (que

se representa por @) como sigue

append_Nil: "[]@ys = ys"

append_Cons: "(x#xs)@ys = x#(xs@ys)"

text {*

Lema. [Ejemplo de inducción sobre listas]

Demostrar que la concatenación de listas es asociativa.

-- "La demostración estructurada es"

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

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

-- "La demostración automática es"

lemma conc_asociativa_1: "xs @ (ys @ zs) = (xs @ ys) @ zs"

by (induct xs) auto

text {*

Ejemplo de definición de tipos recursivos:

Definir un tipo de dato para los árboles binarios.

datatype 'a arbolB = Hoja "'a"

| Nodo "'a" "'a arbolB" "'a arbolB"

text {*

Ejemplo de definición sobre árboles binarios:

Definir la función "espejo" que aplicada a un árbol devuelve su imagen

especular.

fun espejo :: "'a arbolB ⇒ 'a arbolB" where

"espejo (Hoja x) = (Hoja x)"

| "espejo (Nodo x i d) = (Nodo x (espejo d) (espejo i))"

value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))"

-- "= Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))"

text {*

Ejemplo de demostración sobre árboles binarios:

Demostrar que la función "espejo" es involutiva; es decir, para

cualquier árbol a, se tiene que

espejo(espejo(a)) = a.

-- "La demostración estructurada es"

lemma espejo_involutiva:

fixes a :: "'b arbolB"

shows "espejo (espejo a) = a" (is "?P a")

proof (induct a)

fix x

show "?P (Hoja x)" by simp

fix x

fix i assume h1: "?P i"

fix d assume h2: "?P d"

show "?P (Nodo x i d)"

proof -

have "espejo(espejo(Nodo x i d)) = espejo(Nodo x (espejo d) (espejo i))"

by simp

also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" by simp

also have "… = Nodo x i d" using h1 h2 by simp

finally show ?thesis .

qed

text {*

Comentarios sobre la demostración anterior:

· (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario

cuyos elementos son de tipo b".

· (induct a) indica que el método de demostración es por inducción

en el árbol binario a.

· Se generan dos casos:

1. ⋀a. espejo (espejo (Hoja a)) = Hoja a

2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2;

espejo (espejo a3) = a3⟧

⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3

-- "La demostración automática es"

lemma espejo_involutiva_1:

"espejo (espejo a ) = a"

by (induct a) auto

text {*

Ejemplo. [Aplanamiento de árboles]

Definir la función "aplana" que aplane los árboles recorriéndolos en

orden infijo.

fun aplana :: "'a arbolB ⇒ 'a list" where

"aplana (Hoja x) = [x]"

| "aplana (Nodo x i d) = (aplana i) @ [x] @ (aplana d)"

value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))"

-- "= [c, b, d, a, e]"

text {*

Ejemplo. [Aplanamiento de la imagen especular] Demostrar que

aplana (espejo a) = rev (aplana a)

-- "La demostración estructurada es"

lemma

fixes a :: "'b arbolB"

shows "aplana (espejo a) = rev (aplana a)" (is "?P a")

proof (induct a)

fix x

show "?P (Hoja x)" by simp

fix x

fix i assume h1: "?P i"

fix d assume h2: "?P d"

show "?P (Nodo x i d)"

proof -

have "aplana (espejo (Nodo x i d)) =

aplana (Nodo x (espejo d) (espejo i))" by simp

also have "… = (aplana(espejo d))@[x]@(aplana(espejo i))" by simp

also have "… = (rev(aplana d))@[x]@(rev(aplana i))" using h1 h2 by simp

also have "… = rev((aplana i)@[x]@(aplana d))" by simp

also have "… = rev(aplana (Nodo x i d))" by simp

finally show ?thesis .

qed

-- "La demostración automática es"

lemma "aplana (espejo a) = rev (aplana a)"

by (induct a) auto

section {* Heurísticas para la inducción *}

text {*

Definición. [Definición recursiva de inversa]

(inversa xs) la inversa de la lista xs. Por ejemplo,

inversa [a,b,c] = [c,b,a]

fun inversa :: "'a list ⇒ 'a list" where

"inversa [] = []"

| "inversa (x#xs) = (inversa xs) @ [x]"

value "inversa [a,b,c]"

text {*

Definición. [Definición de inversa con acumuladores]

(inversaAc xs) es la inversa de la lista xs calculada con

acumuladores. Por ejemplo,

inversaAc [a,b,c] = [c,b,a]

inversaAcAux [a,b,c] [] = [c,b,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 "inversaAcAux [a,b,c] []"

value "inversaAc [a,b,c]"

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)

fix a xs 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

-- "La demostración estructurada es"

lemma inversaAcAux_es_inversa:

"inversaAcAux xs ys = (inversa xs)@ys"

proof (induct xs arbitrary: ys)

show "⋀ys. inversaAcAux [] ys = (inversa [])@ys" by simp

fix a xs

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

-- "la demostración automática es"

lemma inversaacaux_es_inversa_1:

"inversaacaux xs ys = (inversa xs)@ys"

by (induct xs arbitrary: ys) auto

text {*

corolario. para cualquier lista xs, se tiene que

inversaac xs = inversa xs

corollary "inversaac xs = inversa xs"

by (simp add: inversaacaux_es_inversa inversaac_def)

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.

lemma "(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 .

qed

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

fix m

assume "ack m 1 > 1"

then show "ack (Suc m) 0 > 0" by simp

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

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

section {* Recursión mutua e inducción *}

text {*

Nota. [Ejemplo de definición de tipos mediante recursión cruzada]

· Un árbol de tipo a es una hoja o un nodo de tipo a junto con un

bosque de tipo a.

· Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo

un árbol de tipo a a un bosque de tipo a.

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

and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"

text {*

Regla de inducción correspondiente a la recursión cruzada:

La regla de inducción sobre árboles y bosques es arbol_bosque.induct:

⟦P1 Hoja;

⋀x b. P2 b ⟹ P1 (Nodo x b);

P2 Vacio;

⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧

⟹ P1 a ∧ P2 b

text {*

Ejemplos de definición por recursión cruzada:

· aplana_arbol a) es la lista obtenida aplanando el árbol a.

· (aplana_bosque b) es la lista obtenida aplanando el bosque b.

· (map_arbol a h) es el árbol obtenido aplicando la función h a

todos los nodos del árbol a.

· (map_bosque b h) es el bosque obtenido aplicando la función h a

todos los nodos del bosque b.

fun aplana_arbol :: "'a arbol ⇒ 'a list" and

aplana_bosque :: "'a bosque ⇒ 'a list" where

"aplana_arbol Hoja = []"

| "aplana_arbol (Nodo x b) = x#(aplana_bosque b)"

| "aplana_bosque Vacio = []"

| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"

fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and

map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where

"map_arbol f Hoja = Hoja"

| "map_arbol f (Nodo x b) = Nodo (f x) (map_bosque f b)"

| "map_bosque f Vacio = Vacio"

| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"

text {*

Ejemplo de demostración por inducción cruzada:

Demostrar que:

· aplana_arbol (map_arbol f a) = map f (aplana_arbol a)

· aplana_bosque (map_bosque f b) = map f (aplana_bosque b)

-- "La demostración detallada es"

lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)

∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"

proof (induct_tac a and b)

show "aplana_arbol (map_arbol f Hoja ) = map f (aplana_arbol Hoja)"

by simp

fix x b

assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"

have "aplana_arbol (map_arbol f (Nodo x b)) =

aplana_arbol (Nodo (f x) (map_bosque f b))" by simp

also have "… = (f x)#(aplana_bosque (map_bosque f b))" by simp

also have "… = (f x)#(map f (aplana_bosque b))" using HI by simp

also have "… = map f (aplana_arbol (Nodo x b))" by simp

finally show "aplana_arbol (map_arbol f (Nodo x b))

= map f (aplana_arbol (Nodo x b))" .

show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)"

by simp

fix a b

assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"

and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"

have "aplana_bosque (map_bosque f (ConsB a b)) =

aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp

also have "… = aplana_arbol(map_arbol f a)@aplana_bosque(map_bosque f b)"

by simp

also have "… = (map f (aplana_arbol a))@(map f (aplana_bosque b))"

using HI1 HI2 by simp

also have "… = map f (aplana_bosque (ConsB a b))" by simp

finally show "aplana_bosque (map_bosque f (ConsB a b))

= map f (aplana_bosque (ConsB a b))" by simp

qed

text {*

Comentarios sobre la demostración anterior:

· (induct_tac a and b) indica que el método de demostración es por

inducción cruzada sobre a y b.

· Se generan 4 casos:

1. aplana_arbol (map_arbol arbol.Hoja h) = map h (aplana_arbol arbol.Hoja)

2. ⋀a bosque.

aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹

aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =

map h (aplana_arbol (arbol.Nodo a bosque))

3. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)

4. ⋀arbol bosque.

⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);

aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧

⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =

map h (aplana_bosque (ConsB arbol bosque))

-- "La demostración automática es"

lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)

∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"

by (induct_tac a and b) auto

end

Se puede imprimir o compartir con