{"id":4331,"date":"2014-05-22T19:53:26","date_gmt":"2014-05-22T17:53:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4331"},"modified":"2014-05-23T09:55:15","modified_gmt":"2014-05-23T07:55:15","slug":"lmf2014-razonamiento-por-casos-y-por-induccion-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2014-razonamiento-por-casos-y-por-induccion-en-isabellehol\/","title":{"rendered":"LMF2014: Razonamiento por casos y por inducci\u00f3n en Isabelle\/HOL"},"content":{"rendered":"<p>En la  clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-13\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado c\u00f3mo demostrar por casos o por inducci\u00f3n propiedade de programas funcionales con Isabelle\/HOL.<\/p>\n<p>La teor\u00eda correspondiente es<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* Tema 14: Razonamiento por casos y por inducci\u00f3n *}\n\ntheory T14\nimports Main\nbegin\n\ntext {*\n  En este tema se ampl\u00edan los m\u00e9todos de demostraci\u00f3n por casos y por\n  inducci\u00f3n iniciados en el tema anterior.\n*}\n\nsection {* Razonamiento por distinci\u00f3n de casos *}\n\nsubsection {* Distinci\u00f3n de casos booleanos *}\n\ntext {*\n  Ejemplo de demostraci\u00f3n por distinci\u00f3n de casos booleanos:\n  Demostrar \"\u00acA \u2228 A\".\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"\u00acA \u2228 A\" \nproof cases\n  assume \"A\" \n  then show \"\u00acA \u2228 A\" ..\nnext\n  assume \"\u00acA\" \n  then show \"\u00acA \u2228 A\" ..\nqed\n\ntext {*\n  Comentarios de la demostraci\u00f3n anterior:\n  \u00b7 \"proof cases\" indica que el m\u00e9todo de demostraci\u00f3n ser\u00e1 por distinci\u00f3n de \n    casos. \n  \u00b7 Se generan 2 casos:\n       1. ?P \u27f9 \u00acA \u2228 A\n       2. \u00ac?P \u27f9 \u00acA \u2228 A\n    donde ?P es una variable sobre las f\u00f3rmulas.\n  \u00b7 (assume \"A\") indica que se est\u00e1 usando \"A\" en lugar de la variable\n    ?P.\n  \u00b7 \"then\" indica usando la f\u00f3rmula anterior.\n  \u00b7 \"..\" indica usando la regla l\u00f3gica necesaria (las reglas l\u00f3gicas se\n    estudiar\u00e1n en los siguientes temas).\n  \u00b7 \"next\" indica el siguiente caso (se puede observar c\u00f3mo ha\n    sustituido \u00ac?P por \u00acA.\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"\u00acA \u2228 A\" \nby auto\n\ntext {*\n  Ejemplo de demostraci\u00f3n por distinci\u00f3n de casos booleanos con nombres: \n  Demostrar \"\u00acA \u2228 A\".\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"\u00acA \u2228 A\" \nproof (cases \"A\")\n  case True \n  then show \"\u00acA \u2228 A\" ..\nnext\n  case False \n  thus \"\u00acA \u2228 A\" .. \nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (cases \"A\") indica que la demostraci\u00f3n se har\u00e1 por casos seg\u00fan los\n    distintos valores de \"A\".\n  \u00b7 Como \"A\" es una f\u00f3rmula, sus posibles valores son verdadero o falso.\n  \u00b7 \"case True\" indica que se est\u00e1 suponiendo que A es verdadera. Es\n    equivalente a \"assume A\".\n  \u00b7 \"case False\" indica que se est\u00e1 suponiendo que A es falsa. Es\n    equivalente a \"assume \u00acA\".\n  \u00b7 En general, \n    \u00b7 el m\u00e9todo (cases F) es una abreviatura de la aplicaci\u00f3n de la regla\n         \u27e6F \u27f9 Q; \u00acF \u27f9 Q\u27e7 \u27f9 Q  \n    \u00b7 La expresi\u00f3n \"case True\" es una abreviatura de F.\n    \u00b7 La expresi\u00f3n \"case False\" es una abreviatura de \u00acF.\n  \u00b7 Ventajas de \"cases\" con nombre: \n    \u00b7 reduce la escritura de la f\u00f3rmula y\n    \u00b7 es independiente del orden de los casos.\n*}\n\nsubsection {* Distinci\u00f3n de casos sobre otros tipos de datos *}\n\ntext {*\n  Ejemplo de distinci\u00f3n de casos sobre listas: \n  Demostrar que la longitud del resto de una lista es la longitud de la\n  lista menos 1. \n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"length (tl xs) = length xs - 1\" \nproof (cases xs)\n  assume \"xs = []\"\n  then show \"length (tl xs) = length xs - 1\" by simp\nnext\n  fix y ys\n  assume \"xs = y#ys\"\n  then show \"length(tl xs) = length xs - 1\" by simp \nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"(cases xs)\" indica que la demostraci\u00f3n se har\u00e1 por casos sobre los\n    posibles valores de xs.\n  \u00b7 Como xs es una lista, sus posibles valores son la lista vac\u00eda ([]) o\n    una lista no vac\u00eda (de la forma (y#ys)).\n  \u00b7 Se generan 2 casos:\n       1. xs = [] \u27f9 length (tl xs) = length xs - 1\n       2. \u22c0a list. xs = a # list \u27f9 length (tl xs) = length xs - 1\n*}\n\n-- \"La demostraci\u00f3n simplificada es\"\nlemma \"length (tl xs) = length xs - 1\" \nproof (cases xs)\n  case Nil \n  then show ?thesis by simp\nnext\n  case Cons \n  then show ?thesis by simp \nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"case Nil\" es una abreviatura de \n       \"assume xs =[]\".\n  \u00b7 \"case Cons\" es una abreviatura de \n       \"fix y ys assume xs = y#ys\"\n  \u00b7 ?thesis es una abreviatura de la conclusi\u00f3n del lema.\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"length (tl xs) = length xs - 1\" \nby auto\n\ntext {*\n  Een el siguiente ejemplo vamos a demostrar una propiedad de la funci\u00f3n\n  drop que est\u00e1 definida en la teor\u00eda List de forma que (drop n xs) la\n  lista obtenida eliminando en xs} los n primeros elementos. Su\n  definici\u00f3n es la siguiente   \n     drop_Nil:  \"drop n []     = []\" \n     drop_Cons: \"drop n (x#xs) = (case n of \n                                    0 => x#xs | \n                                    Suc(m) => drop m xs)\"\n*}\n\ntext {*\n  Ejemplo de an\u00e1lisis de casos:\n  Demostrar que el resultado de eliminar los n+1 primeros elementos de\n  xs es el mismo que eliminar los n primeros elementos del resto de xs.  \n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\nproof (cases xs)\n  case Nil \n  then show ?thesis by simp\nnext\n  case Cons \n  then show ?thesis by simp\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\nby (cases xs) auto\n\nsection {* Demostraciones por inducci\u00f3n y patrones *}\n\ntext {*\n  [Principio de inducci\u00f3n matem\u00e1tica]\n  Para demostrar una propiedad P para todos los n\u00fameros naturales basta\n  probar que el 0 tiene la propiedad P y que si n tiene la propiedad P,\n  entonces n+1 tambi\u00e9n la tiene. \n     \u27e6P 0; \u22c0n. P n \u27f9 P (Suc n)\u27e7 \u27f9 P m\n\n  En Isabelle el principio de inducci\u00f3n matem\u00e1tica est\u00e1 formalizado en\n  el teorema nat.induct y puede verse con\n     thm nat.induct\n*}\n\ntext {*  \n  Ejemplo de demostraci\u00f3n por inducci\u00f3n: Usaremos el principio de\n  inducci\u00f3n matem\u00e1tica para demostrar que \n     1 + 3 + ... + (2n-1) = n^2\n\n  Definici\u00f3n. [Suma de los primeros impares] \n  (suma_impares n) la suma de los n n\u00fameros impares. Por ejemplo,\n     suma_impares 3  =  9\n*}\n\nfun suma_impares :: \"nat \u21d2 nat\" where\n  \"suma_impares 0 = 0\" \n| \"suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n\"\n\nvalue \"suma_impares 3\"\n\ntext {*\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n matem\u00e1tica:\n  Demostrar que la suma de los n primeros n\u00fameros impares es n^2.\n*}\n\n-- \"Demostraci\u00f3n del lema anterior por inducci\u00f3n y razonamiento ecuacional\"\nlemma \"suma_impares n = n * n\"\nproof (induct n)\n  show \"suma_impares 0 = 0 * 0\" by simp\nnext\n  fix n assume HI: \"suma_impares n = n * n\"\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" by simp\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\n  finally show \"suma_impares (Suc n) = (Suc n) * (Suc n)\" by simp\nqed\n\n-- \"Demostraci\u00f3n del lema anterior con patrones y razonamiento ecuacional\"\nlemma \"suma_impares n = n * n\" (is \"?P n\")\nproof (induct n)\n  show \"?P 0\" by simp\nnext\n  fix n \n  assume HI: \"?P n\"\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" by simp\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\n  finally show \"?P (Suc n)\" by simp\nqed\n\ntext {*\n  Comentario sobre la demostraci\u00f3n anterior:\n  \u00b7 Con la expresi\u00f3n\n       \"suma_impares n = n * n\" (is \"?P n\")\n    se abrevia \"suma_impares n = n * n\" como \"?P n\". Por tanto, \n       \"?P 0\"       es una abreviatura de \"suma_impares 0 = 0 * 0\"\n       \"?P (Suc n)\" es una abreviatura de \"suma_impares (Suc n) = (Suc n) * (Suc n)\"\n  \u00b7 En general, cualquier f\u00f3rmula seguida de (is patr\u00f3n) equipara el\n    patr\u00f3n con la f\u00f3rmula. \n*}\n\n-- \"La demostraci\u00f3n usando patrones es\"\nlemma \"suma_impares n = n * n\" (is \"?P n\")\nproof (induct n)\n  show \"?P 0\" by simp\nnext\n  fix n \n  assume \"?P n\"\n  then show \"?P (Suc n)\" by simp\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"suma_impares n = n * n\"\nby (induct n) auto\n\n\nsection {* Inducci\u00f3n estructural *}\n\ntext {*\n  Inducci\u00f3n estructural:\n  \u00b7 En Isabelle puede hacerse inducci\u00f3n estructural sobre cualquier tipo\n    recursivo.\n  \u00b7 La inducci\u00f3n matem\u00e1tica es la inducci\u00f3n estructural sobre el tipo de\n    los naturales.\n  \u00b7 El esquema de inducci\u00f3n estructural sobre listas es\n    \u00b7 list.induct: \u27e6P []; \u22c0x ys. P ys \u27f9 P (x # ys)\u27e7 \u27f9 P zs\n  \u00b7 Para demostrar una propiedad para todas las listas basta demostrar\n    que la lista vac\u00eda tiene la propiedad y que al a\u00f1adir un elemento a una\n    lista que tiene la propiedad se obtiene una lista que tambi\u00e9n tiene la\n    propiedad. \n  \u00b7 En Isabelle el principio de inducci\u00f3n sobre listas est\u00e1 formalizado\n    mediante el teorema list.induct que puede verse con \n       thm list.induct\n*}\n\ntext {*\n  Concatenaci\u00f3n de listas:\n  En la teor\u00eda List.thy est\u00e1 definida la concatenaci\u00f3n de listas (que\n  se representa por @) como sigue\n     append_Nil:  \"[]@ys     = ys\"\n     append_Cons: \"(x#xs)@ys = x#(xs@ys)\"\n*}\n\ntext {*\n  Lema. [Ejemplo de inducci\u00f3n sobre listas]\n  Demostrar que la concatenaci\u00f3n de listas es asociativa.\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma conc_asociativa: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\nproof (induct xs)\n  show \"[] @ (ys @ zs) = ([] @ ys) @ zs\"\n  proof -\n    have \"[] @ (ys @ zs) = ys @ zs\" by simp\n    also have \"\u2026 = ([] @ ys) @ zs\" by simp\n    finally show ?thesis .\n  qed\nnext\n  fix x xs\n  assume HI: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\n  show \"(x#xs) @ (ys @ zs) = ((x#xs) @ ys) @ zs\"\n  proof -\n    have \"(x#xs) @ (ys @ zs) = x#(xs @ (ys @ zs))\" by simp\n    also have \"\u2026 = x#((xs @ ys) @ zs)\" using HI by simp\n    also have \"\u2026 = (x#(xs @ ys)) @ zs\" by simp\n    also have \"\u2026 = ((x#xs) @ ys) @ zs\" by simp\n    finally show ?thesis .\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma conc_asociativa_1: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\nby (induct xs) auto\n\ntext {* \n  Ejemplo de definici\u00f3n de tipos recursivos:\n  Definir un tipo de dato para los \u00e1rboles binarios.\n*}\n\ndatatype 'a arbolB = Hoja \"'a\" \n                   | Nodo \"'a\" \"'a arbolB\" \"'a arbolB\"\n\ntext {* \n  Ejemplo de definici\u00f3n sobre \u00e1rboles binarios:\n  Definir la funci\u00f3n \"espejo\" que aplicada a un \u00e1rbol devuelve su imagen\n  especular.  \n*}\n\nfun espejo :: \"'a arbolB \u21d2 'a arbolB\" where\n  \"espejo (Hoja x) = (Hoja x)\"\n| \"espejo (Nodo x i d) = (Nodo x (espejo d) (espejo i))\"\n\nvalue \"espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))\"\n-- \"= Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))\"\n\ntext {* \n  Ejemplo de demostraci\u00f3n sobre \u00e1rboles binarios:\n  Demostrar que la funci\u00f3n \"espejo\" es involutiva; es decir, para\n  cualquier \u00e1rbol a, se tiene que \n     espejo(espejo(a)) = a.\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma espejo_involutiva:\n  fixes a :: \"'b arbolB\" \n  shows \"espejo (espejo a) = a\" (is \"?P a\")\nproof (induct a)\n  fix x \n  show \"?P (Hoja x)\" by simp \nnext\n  fix x\n  fix i assume h1: \"?P i\"\n  fix d assume h2: \"?P d\"\n  show \"?P (Nodo x i d)\" \n  proof -\n    have \"espejo(espejo(Nodo x i d)) = espejo(Nodo x (espejo d) (espejo i))\"\n      by simp\n    also have \"\u2026 = Nodo x (espejo (espejo i)) (espejo (espejo d))\" by simp\n    also have \"\u2026 = Nodo x i d\" using h1 h2 by simp \n    finally show ?thesis .\n qed\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (fixes a :: \"'b arbolB\") es una abreviatura de \"sea a1 un \u00e1rbol binario\n    cuyos elementos son de tipo b\". \n  \u00b7 (induct a) indica que el m\u00e9todo de demostraci\u00f3n es por inducci\u00f3n\n    en el \u00e1rbol binario a.\n  \u00b7 Se generan dos casos:\n    1. \u22c0a. espejo (espejo (Hoja a)) = Hoja a\n    2. \u22c0a1 a2 a3. \u27e6espejo (espejo a2) = a2; \n                   espejo (espejo a3) = a3\u27e7\n                  \u27f9 espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma espejo_involutiva_1: \n  \"espejo (espejo a ) = a\"\nby (induct a) auto\n\ntext {* \n  Ejemplo. [Aplanamiento de \u00e1rboles]\n  Definir la funci\u00f3n \"aplana\" que aplane los \u00e1rboles recorri\u00e9ndolos en\n  orden infijo.  \n*}\n\nfun aplana :: \"'a arbolB \u21d2 'a list\" where\n  \"aplana (Hoja x)     = [x]\"\n| \"aplana (Nodo x i d) = (aplana i) @ [x] @ (aplana d)\"\n\nvalue \"aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))\"\n-- \"= [c, b, d, a, e]\"\n\ntext {* \n  Ejemplo. [Aplanamiento de la imagen especular] Demostrar que\n     aplana (espejo a) = rev (aplana a)\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \n  fixes a :: \"'b arbolB\"\n  shows \"aplana (espejo a) = rev (aplana a)\" (is \"?P a\")\nproof (induct a)\n  fix x\n  show \"?P (Hoja x)\" by simp \nnext\n  fix x \n  fix i assume h1: \"?P i\"\n  fix d assume h2: \"?P d\"\n  show \"?P (Nodo x i d)\" \n  proof -\n    have \"aplana (espejo (Nodo x i d)) = \n          aplana (Nodo x (espejo d) (espejo i))\" by simp\n    also have \"\u2026 = (aplana(espejo d))@[x]@(aplana(espejo i))\" by simp\n    also have \"\u2026 = (rev(aplana d))@[x]@(rev(aplana i))\" using h1 h2 by simp\n    also have \"\u2026 = rev((aplana i)@[x]@(aplana d))\" by simp\n    also have \"\u2026 = rev(aplana (Nodo x i d))\" by simp\n    finally show ?thesis .\n qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"aplana (espejo a) = rev (aplana a)\"\nby (induct a) auto\n\nsection {* Heur\u00edsticas para la inducci\u00f3n *}\n\ntext {*\n  Definici\u00f3n. [Definici\u00f3n recursiva de inversa]\n  (inversa xs) la inversa de la lista xs. Por ejemplo,\n     inversa [a,b,c] = [c,b,a] \n*}\n\nfun inversa :: \"'a list \u21d2 'a list\" where\n  \"inversa [] = []\" \n| \"inversa (x#xs) = (inversa xs) @ [x]\"\n\nvalue \"inversa [a,b,c]\"\n\ntext {* \n  Definici\u00f3n. [Definici\u00f3n de inversa con acumuladores]\n  (inversaAc xs) es la inversa de la lista xs calculada con\n  acumuladores. Por ejemplo,\n     inversaAc [a,b,c]       = [c,b,a] \n     inversaAcAux [a,b,c] [] = [c,b,a] \n*}\n\nfun inversaAcAux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\n  \"inversaAcAux [] ys     = ys\" \n| \"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)\"\n\ndefinition inversaAc :: \"'a list \u21d2 'a list\" where\n  \"inversaAc xs \u2261 inversaAcAux xs []\"\n\nvalue \"inversaAcAux [a,b,c] []\"\nvalue \"inversaAc [a,b,c]\"\n\ntext {* \n  Lema. [Ejemplo de equivalencia entre las definiciones]\n  La inversa de [a,b,c] es lo mismo calculada con la primera definici\u00f3n\n  que con la segunda.\n*}\n\nlemma \"inversaAc [a,b,c] = inversa [a,b,c]\"\nby (simp add: inversaAc_def)\n\ntext {*\n  Nota. [Ejemplo fallido de demostraci\u00f3n por inducci\u00f3n]\n  El siguiente intento de demostrar que para cualquier lista xs, se\n  tiene que  \"inversaAc xs = inversa xs\" falla.\n*}\n\nlemma \"inversaAc xs = inversa xs\"\nproof (induct xs)\n  show \"inversaAc [] = inversa []\" by (simp add: inversaAc_def)\nnext\n  fix a xs assume HI: \"inversaAc xs = inversa xs\"\n  have \"inversaAc (a#xs) = inversaAcAux (a#xs) []\" by (simp add: inversaAc_def)\n  also have \"\u2026 = inversaAcAux xs [a]\" by simp\n  also have \"\u2026 = inversa (a#xs)\"\n  -- \"Problema: la hip\u00f3tesis de inducci\u00f3n no es aplicable.\"\noops\n\ntext {* \n  Nota. [Heur\u00edstica de generalizaci\u00f3n]\n  Cuando se use demostraci\u00f3n estructural, cuantificar universalmente las \n  variables libres (o, equivalentemente, considerar las variables libres\n  como variables arbitrarias).\n\n  Lema. [Lema con generalizaci\u00f3n]\n  Para toda lista ys se tiene \n     inversaAcAux xs ys = (inversa xs) @ ys\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma inversaAcAux_es_inversa:\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\nproof (induct xs arbitrary: ys)\n  show \"\u22c0ys. inversaAcAux [] ys = (inversa [])@ys\" by simp\nnext\n  fix a xs \n  assume HI: \"\u22c0ys. inversaAcAux xs ys = inversa xs@ys\"\n  show \"\u22c0ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys\"\n  proof -\n    fix ys\n    have \"inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)\" by simp\n    also have \"\u2026 = inversa xs@(a#ys)\" using HI by simp\n    also have \"\u2026 = inversa (a#xs)@ys\" using [[simp_trace]] by simp \n    finally show \"inversaacaux (a#xs) ys = inversa (a#xs)@ys\" by simp\n  qed\nqed\n\n-- \"la demostraci\u00f3n autom\u00e1tica es\"\nlemma inversaacaux_es_inversa_1:\n  \"inversaacaux xs ys = (inversa xs)@ys\"\nby (induct xs arbitrary: ys) auto\n\ntext {*\n  corolario.  para cualquier lista xs, se tiene que\n     inversaac xs = inversa xs\n*}\n\ncorollary \"inversaac xs = inversa xs\"\nby (simp add: inversaacaux_es_inversa inversaac_def)\n\ntext {*\n  nota. en el paso \"inversa xs@(a#ys) = inversa (a#xs)@ys\" se usan\n  lemas de la teor\u00eda list. se puede observar, insertano \n     using [[simp_trace]]\n  entre la igualdad y by simp, que los lemas usados son \n  \u00b7 List.append_simps_1: []@ys = ys\n  \u00b7 List.append_simps_2: (x#xs)@ys = x#(xs@ys)\n  \u00b7 List.append_assoc:   (xs @ ys) @ zs = xs @ (ys @ zs)\n  Las dos primeras son las ecuaciones de la definici\u00f3n de append.\n\n  En la siguiente demostraci\u00f3n se detallan los lemas utilizados.\n*}\n\nlemma \"(inversa xs)@(a#ys) = (inversa (a#xs))@ys\"\nproof -\n  have \"(inversa xs)@(a#ys) = (inversa xs)@(a#([]@ys))\" \n    by (simp only: append.simps(1))\n  also have \"\u2026 = (inversa xs)@([a]@ys)\" by (simp only: append.simps(2))\n  also have \"\u2026 = ((inversa xs)@[a])@ys\" by (simp only: append_assoc)\n  also have \"\u2026 = (inversa (a#xs))@ys\" by (simp only: inversa.simps(2))\n  finally show ?thesis .\nqed\n\nsection {* Recursi\u00f3n general. La funci\u00f3n de Ackermann *}\n\ntext {* \n  El objetivo de esta secci\u00f3n es mostrar el uso de las definiciones\n  recursivas generales y sus esquemas de inducci\u00f3n. Como ejemplo se usa la\n  funci\u00f3n de Ackermann (se puede consultar informaci\u00f3n sobre dicha funci\u00f3n en\n  http:\/\/en.wikipedia.org\/wiki\/Ackermann_function).\n\n  Definici\u00f3n.  La funci\u00f3n de Ackermann se define por\n    A(m,n) = n+1,             si m=0,\n             A(m-1,1),        si m>0 y n=0,\n             A(m-1,A(m,n-1)), si m>0 y n>0\n  para todo los n\u00fameros naturales. \n\n  La funci\u00f3n de Ackermann es recursiva, pero no es primitiva recursiva. \n*}\n\nfun ack :: \"nat \u21d2 nat \u21d2 nat\" where\n  \"ack 0       n       = n+1\" \n| \"ack (Suc m) 0       = ack m 1\" \n| \"ack (Suc m) (Suc n) = ack m (ack (Suc m) n)\"\n\n-- \"Ejemplo de evaluaci\u00f3n\"\nvalue \"ack 2 3\" (* devuelve 9 *)\n\ntext {*\n  Esquema de inducci\u00f3n correspondiente a una funci\u00f3n:\n  \u00b7 Al definir una funci\u00f3n recursiva general se genera una regla de\n    inducci\u00f3n. En la definici\u00f3n anterior, la regla generada es\n    ack.induct: \n       \u27e6\u22c0n. P 0 n; \n        \u22c0m. P m 1 \u27f9 P (Suc m) 0;\n        \u22c0m n. \u27e6P (Suc m) n; P m (ack (Suc m) n)\u27e7 \u27f9 P (Suc m) (Suc n)\u27e7\n       \u27f9 P a b\n*}\n\ntext {*\n  Ejemplo de demostraci\u00f3n por la inducci\u00f3n correspondiente a una funci\u00f3n:\n  Demostrar que para todos m y n, A(m,n) > n.\n*} \n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"ack m n > n\"\nproof (induct m n rule: ack.induct)\n  fix n\n  show \"ack 0 n > n\" by simp\nnext\n  fix m \n  assume \"ack m 1 > 1\"\n  then show \"ack (Suc m) 0 > 0\" by simp\nnext  \n  fix m n\n  assume \"n < ack (Suc m) n\" and \n         \"ack (Suc m) n < ack m (ack (Suc m) n)\"\n  then show \"Suc n < ack (Suc m) (Suc n)\" by simp\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (induct m n rule: ack.induct) indica que el m\u00e9todo de demostraci\u00f3n\n    es el esquema de recursi\u00f3n correspondiente a la definici\u00f3n de \n    (ack m n).\n  \u00b7 Se generan 3 casos:\n    1. \u22c0n. n < ack 0 n\n    2. \u22c0m. 1 < ack m 1 \u27f9 0 < ack (Suc m) 0\n    3. \u22c0m n. \u27e6n < ack (Suc m) n; \n              ack (Suc m) n < ack m (ack (Suc m) n)\u27e7\n             \u27f9 Suc n < ack (Suc m) (Suc n)\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"ack m n > n\"\nby (induct m n rule: ack.induct) auto\n\nsection {* Recursi\u00f3n mutua e inducci\u00f3n *}\n\ntext {*\n  Nota. [Ejemplo de definici\u00f3n de tipos mediante recursi\u00f3n cruzada]\n  \u00b7 Un \u00e1rbol de tipo a es una hoja o un nodo de tipo a junto con un\n    bosque de tipo a.\n  \u00b7 Un bosque de tipo a es el boque vac\u00edo o un bosque contruido a\u00f1adiendo\n    un \u00e1rbol de tipo a a un bosque de tipo a.\n*}\n\ndatatype 'a arbol = Hoja | Nodo \"'a\" \"'a bosque\"\n     and 'a bosque = Vacio | ConsB \"'a arbol\" \"'a bosque\"\n\ntext {*\n  Regla de inducci\u00f3n correspondiente a la recursi\u00f3n cruzada:\n  La regla de inducci\u00f3n sobre \u00e1rboles y bosques es arbol_bosque.induct:\n     \u27e6P1 Hoja; \n      \u22c0x b. P2 b \u27f9 P1 (Nodo x b); \n      P2 Vacio;\n      \u22c0a b. \u27e6P1 a; P2 b\u27e7 \u27f9 P2 (ConsB a b)\u27e7 \n     \u27f9 P1 a \u2227 P2 b\n*}\n\ntext {* \n  Ejemplos de definici\u00f3n por recursi\u00f3n cruzada:\n  \u00b7 aplana_arbol a) es la lista obtenida aplanando el \u00e1rbol a.   \n  \u00b7 (aplana_bosque b) es la lista obtenida aplanando el bosque b.   \n  \u00b7 (map_arbol a h) es el \u00e1rbol obtenido aplicando la funci\u00f3n h a\n    todos los nodos del \u00e1rbol a.   \n  \u00b7 (map_bosque b h) es el bosque obtenido aplicando la funci\u00f3n h a\n    todos los nodos del bosque b. \n*}\n\nfun aplana_arbol :: \"'a arbol \u21d2 'a list\" and \n    aplana_bosque :: \"'a bosque \u21d2 'a list\" where\n  \"aplana_arbol Hoja = []\"\n| \"aplana_arbol (Nodo x b) = x#(aplana_bosque b)\"\n| \"aplana_bosque Vacio = []\"\n| \"aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)\"\n\nfun map_arbol :: \"('a \u21d2 'b) \u21d2 'a arbol \u21d2 'b arbol\" and\n    map_bosque :: \"('a \u21d2 'b) \u21d2 'a bosque \u21d2 'b bosque\" where\n  \"map_arbol  f Hoja        = Hoja\"\n| \"map_arbol  f (Nodo x b)  = Nodo (f x) (map_bosque f b)\"\n| \"map_bosque f Vacio       = Vacio\"\n| \"map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)\"\n\ntext {*\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n cruzada:\n  Demostrar que:\n  \u00b7 aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)\n  \u00b7 aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)\n     \u2227 aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\"\nproof (induct_tac a and b)\n  show \"aplana_arbol (map_arbol f Hoja ) = map f (aplana_arbol Hoja)\" \n    by simp\nnext\n  fix x b\n  assume HI: \"aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\"\n  have \"aplana_arbol (map_arbol f (Nodo x b)) = \n        aplana_arbol (Nodo (f x) (map_bosque f b))\" by simp\n  also have \"\u2026 = (f x)#(aplana_bosque (map_bosque f b))\" by simp\n  also have \"\u2026 = (f x)#(map f (aplana_bosque b))\" using HI by simp\n  also have \"\u2026 = map f (aplana_arbol (Nodo x b))\" by simp\n  finally show \"aplana_arbol (map_arbol f (Nodo x b))\n                = map f (aplana_arbol (Nodo x b))\" .\nnext\n  show \"aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)\" \n    by simp\nnext\n  fix a b\n  assume HI1: \"aplana_arbol (map_arbol f a) = map f (aplana_arbol a)\"\n     and HI2: \"aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\"\n  have \"aplana_bosque (map_bosque f (ConsB a b)) = \n        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))\" by simp\n  also have \"\u2026 = aplana_arbol(map_arbol f a)@aplana_bosque(map_bosque f b)\" \n    by simp\n  also have \"\u2026 = (map f (aplana_arbol a))@(map f (aplana_bosque b))\" \n    using HI1 HI2 by simp\n  also have \"\u2026 = map f (aplana_bosque (ConsB a b))\" by simp\n  finally show \"aplana_bosque (map_bosque f (ConsB a b)) \n                = map f (aplana_bosque (ConsB a b))\" by simp\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (induct_tac a and b) indica que el m\u00e9todo de demostraci\u00f3n es por\n    inducci\u00f3n cruzada sobre a y b.\n  \u00b7 Se generan 4 casos:\n    1. aplana_arbol (map_arbol arbol.Hoja h) = map h (aplana_arbol arbol.Hoja)\n    2. \u22c0a bosque.\n          aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) \u27f9\n          aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =\n          map h (aplana_arbol (arbol.Nodo a bosque))\n    3. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)\n    4. \u22c0arbol bosque.\n          \u27e6aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);\n           aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)\u27e7\n          \u27f9 aplana_bosque (map_bosque (ConsB arbol bosque) h) =\n             map h (aplana_bosque (ConsB arbol bosque))\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)\n     \u2227 aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\"\nby (induct_tac a and b) auto\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado c\u00f3mo demostrar por casos o por inducci\u00f3n propiedade de programas funcionales con Isabelle\/HOL. La teor\u00eda correspondiente es<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[234],"tags":[144,303],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4331"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4331"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4331\/revisions"}],"predecessor-version":[{"id":4333,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4331\/revisions\/4333"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4331"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4331"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4331"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}