{"id":3263,"date":"2013-04-25T17:30:14","date_gmt":"2013-04-25T17:30:14","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3263"},"modified":"2013-04-26T12:21:39","modified_gmt":"2013-04-26T12:21:39","slug":"ra2012-razonamiento-por-casos-y-por-induccion-en-isabellehol-1","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2012-razonamiento-por-casos-y-por-induccion-en-isabellehol-1\/","title":{"rendered":"RA2012: Razonamiento por casos y por inducci\u00f3n en Isabelle\/HOL (1)"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a> se ha presentado los m\u00e9todos de demostraci\u00f3n por casos y por inducci\u00f3n iniciados en Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 6: Razonamiento por casos y por inducci\u00f3n *}\r\n\r\ntheory T6\r\nimports Main Parity\r\nbegin\r\n\r\ntext {*\r\n  En este tema se ampl\u00edan los m\u00e9todos de demostraci\u00f3n por casos y por\r\n  inducci\u00f3n iniciados en el tema anterior.\r\n*}\r\n\r\nsection {* Razonamiento por distinci\u00f3n de casos *}\r\n\r\nsubsection {* Distinci\u00f3n de casos booleanos *}\r\n\r\ntext {*\r\n  Ejemplo de demostraci\u00f3n por distinci\u00f3n de casos booleanos:\r\n     \u00acA \u2228 A\r\n*}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"\u00acA \u2228 A\" \r\nproof cases\r\n  assume \"A\" \r\n  thus ?thesis ..\r\nnext\r\n  assume \"\u00acA\" \r\n  thus ?thesis ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"\u00acA \u2228 A\" \r\nproof cases\r\n  assume \"A\" \r\n  thus ?thesis by (rule disjI2)\r\nnext\r\n  assume \"\u00acA\" \r\n  thus ?thesis by (rule disjI1)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"\u00acA \u2228 A\" \r\nby auto\r\n\r\ntext {*\r\n  Ejemplo de demostraci\u00f3n por distinci\u00f3n de casos booleanos nominados: \r\n     \u00acA \u2228 A\r\n*}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"\u00acA \u2228 A\" \r\nproof (cases \"A\")\r\n  case True \r\n  thus ?thesis ..\r\nnext\r\n  case False \r\n  thus ?thesis .. \r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"\u00acA \u2228 A\" \r\nproof (cases \"A\")\r\n  case True \r\n  thus ?thesis by (rule disjI2)\r\nnext\r\n  case False \r\n  thus ?thesis by (rule disjI1)\r\nqed\r\n\r\ntext {*\r\n  El m\u00e9todo \"cases\" sobre una f\u00f3rmula:\r\n  \u00b7 El m\u00e9todo (cases F) es una abreviatura de la aplicaci\u00f3n de la regla\r\n       \u27e6F \u27f9 Q; \u00acF \u27f9 Q\u27e7 \u27f9 Q  \r\n  \u00b7 La expresi\u00f3n \"case True\" es una abreviatura de F.\r\n  \u00b7 La expresi\u00f3n \"case False\" es una abreviatura de \u00acF.\r\n  \u00b7 Ventajas de \"cases\" con nombre: \r\n    \u00b7 reduce la escritura de la f\u00f3rmula y\r\n    \u00b7 es independiente del orden de los casos.\r\n*}\r\n\r\nsubsection {* Distinci\u00f3n de casos sobre otros tipos de datos *}\r\n\r\ntext {*\r\n  Ejemplo de distinci\u00f3n de casos sobre listas: \r\n  La longitud del resto de una lista es la longitud de la lista menos 1.\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"length(tl xs) = length xs - 1\" \r\nproof (cases xs)\r\n  case Nil thus ?thesis by simp\r\nnext\r\n  case Cons thus ?thesis by simp \r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"length(tl xs) = length xs - 1\" \r\nby auto\r\n\r\ntext {*\r\n  Distinci\u00f3n de casos sobre listas:\r\n  \u00b7 El m\u00e9todo de distinci\u00f3n de casos se activa con (cases xs) donde xs\r\n    es del tipo lista. \r\n  \u00b7 \"case Nil\" es una abreviatura de \r\n       \"assume Nil: xs =[]\".\r\n  \u00b7 \"case Cons\" es una abreviatura de \r\n       \"fix ? ?? assume Cons: xs = ? # ??\"\r\n    donde ? y ?? son variables an\u00f3nimas. \r\n*}\r\n\r\ntext {*\r\n  Ejemplo de an\u00e1lisis de casos:\r\n  El resultado de eliminar los n+1 primeros elementos de xs es el mismo\r\n  que eliminar los n primeros elementos del resto de xs.  \r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\r\nproof (cases xs)\r\n  case Nil thus \"drop (n + 1) xs = drop n (tl xs)\" by simp\r\nnext\r\n  case Cons thus \"drop (n + 1) xs = drop n (tl xs)\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\r\nby (cases xs) auto\r\n\r\ntext {*\r\n  La funci\u00f3n drop est\u00e1 definida en la teor\u00eda List de forma que\r\n  (drop n xs) la lista obtenida eliminando en xs} los n primeros\r\n  elementos. Su definici\u00f3n es la siguiente  \r\n     drop_Nil:  \"drop n [] = []\" |\r\n     drop_Cons: \"drop n (x#xs) = (case n of \r\n                                    0 => x#xs | \r\n                                    Suc(m) => drop m xs)\"\r\n*}\r\n\r\nsection {* Inducci\u00f3n matem\u00e1tica *}\r\n\r\ntext {*\r\n  [Principio de inducci\u00f3n matem\u00e1tica]\r\n  Para demostrar una propiedad P para todos los n\u00fameros naturales basta\r\n  probar que el 0 tiene la propiedad P y que si n tiene la propiedad P,\r\n  entonces n+1 tambi\u00e9n la tiene. \r\n     \u27e6P 0; \u22c0n. P n \u27f9 P (Suc n)\u27e7 \u27f9 P m\r\n\r\n  En Isabelle el principio de inducci\u00f3n matem\u00e1tica est\u00e1 formalizado en\r\n  el teorema nat.induct y puede verse con\r\n     thm nat.induct\r\n*}\r\n\r\ntext {*  \r\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n: Usaremos el principio de\r\n  inducci\u00f3n matem\u00e1tica para demostrar que \r\n     1 + 3 + ... + (2n-1) = n^2\r\n\r\n  Definici\u00f3n. [Suma de los primeros impares] \r\n  (suma_impares n) la suma de los n n\u00fameros impares. Por ejemplo,\r\n     suma_impares 3  =  9\r\n*}\r\n\r\nfun suma_impares :: \"nat \u21d2 nat\" where\r\n  \"suma_impares 0 = 0\" \r\n| \"suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n\"\r\n\r\nvalue \"suma_impares 3\"\r\n\r\ntext {*\r\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n matem\u00e1tica:\r\n  La suma de los n primeros n\u00fameros impares es n^2.\r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"suma_impares n = n * n\"\r\nby (induct n) simp_all\r\n\r\n-- \"La demostraci\u00f3n usando patrones es\"\r\nlemma \"suma_impares n = n * n\" (is \"?P n\")\r\nproof (induct n)\r\n  show \"?P 0\" by simp\r\nnext\r\n  fix n assume \"?P n\"\r\n  thus \"?P (Suc n)\" by simp\r\nqed\r\n\r\ntext {*\r\n  Patrones: Cualquier f\u00f3rmula seguida de (is patr\u00f3n) equipara el patr\u00f3n\r\n  con la f\u00f3rmula.\r\n*}\r\n\r\n-- \"Demostraci\u00f3n del lema anterior con patrones y razonamiento ecuacional\"\r\nlemma \"suma_impares n = n * n\" (is \"?P n\")\r\nproof (induct n)\r\n  show \"?P 0\" by simp\r\nnext\r\n  fix n assume HI: \"?P n\"\r\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" by simp\r\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\r\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\r\n  finally show \"?P (Suc n)\" by simp\r\nqed\r\n\r\n-- \"Demostraci\u00f3n del lema anterior por inducci\u00f3n y razonamiento ecuacional\"\r\nlemma \"suma_impares n = n * n\"\r\nproof (induct n)\r\n  show \"suma_impares 0 = 0 * 0\" by simp\r\nnext\r\n  fix n assume HI: \"suma_impares n = n * n\"\r\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" by simp\r\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\r\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\r\n  finally show \"suma_impares (Suc n) = (Suc n) * (Suc n)\" by simp\r\nqed\r\n\r\ntext {* \r\n  Ejemplo de definici\u00f3n con existenciales. \r\n  Un n\u00famero natural n es par si existe un natural m tal que n=m+m.   \r\n*}\r\n\r\ndefinition par :: \"nat \u21d2 bool\" where\r\n  \"par n \u2261 \u2203m. n=m+m\"\r\n\r\ntext {* \r\n  [Ejemplo de inducci\u00f3n y existenciales] Para todo n\u00famero natural\r\n  n, se verifica que n*(n+1) par. \r\n*}\r\n\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"par (n*(n+1))\"\r\nproof (induct n)\r\n  show \"par (0*(0+1))\" by (simp add: par_def)\r\nnext\r\n  fix n assume \"par (n*(n+1))\"\r\n  hence \"\u2203m. n*(n+1) = m+m\" by (simp add:par_def)\r\n  then obtain m where m: \"n*(n+1) = m+m\" by (rule exE)\r\n  hence \"(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)\" by auto\r\n  hence \"\u2203m. (Suc n)*((Suc n)+1) = m+m\" by (rule exI)\r\n  thus \"par ((Suc n)*((Suc n)+1))\" by (simp add:par_def)\r\nqed\r\n\r\ntext {*\r\n  En Isabelle puede demostrarse de manera m\u00e1s simple un lema equivalente\r\n  usando en lugar de la funci\u00f3n \"par\" la funci\u00f3n \"even\" definida en la\r\n  teor\u00eda Parity por\r\n     even x \u27f7 x mod 2 = 0\"\r\n*}\r\n\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"even (n*(n+1))\"\r\nby auto\r\n\r\ntext {*\r\n  Para completar la demostraci\u00f3n basta demostrar la equivalencia de las\r\n  funciones \"par\" y \"even\". \r\n*}\r\n\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"par n = even n\"\r\nproof - \r\n  have \"par n = (\u2203m. n = m+m)\" by (simp add:par_def)\r\n  thus \"par n = even n\" by presburger\r\nqed\r\n\r\ntext {*\r\n  En la demostraci\u00f3n anterior hemos usado la t\u00e1ctica \"presburger\" que\r\n  corresponde a la aritm\u00e9tica de Presburger.\r\n*}\r\n\r\nsection {* Inducci\u00f3n estructural *}\r\n\r\ntext {*\r\n  Inducci\u00f3n estructural:\r\n  \u00b7 En Isabelle puede hacerse inducci\u00f3n estructural sobre cualquier tipo\r\n    recursivo.\r\n  \u00b7 La inducci\u00f3n matem\u00e1tica es la inducci\u00f3n estructural sobre el tipo de\r\n    los naturales.\r\n  \u00b7 El esquema de inducci\u00f3n estructural sobre listas es\r\n    \u00b7 list.induct: \u27e6P []; \u22c0x ys. P ys \u27f9 P (x # ys)\u27e7 \u27f9 P zs\r\n  \u00b7 Para demostrar una propiedad para todas las listas basta demostrar\r\n    que la lista vac\u00eda tiene la propiedad y que al a\u00f1adir un elemento a una\r\n    lista que tiene la propiedad se obtiene una lista que tambi\u00e9n tiene la\r\n    propiedad. \r\n  \u00b7 En Isabelle el principio de inducci\u00f3n sobre listas est\u00e1 formalizado\r\n    mediante el teorema list.induct que puede verse con \r\n       thm list.induct\r\n*}\r\n\r\ntext {*\r\n  Concatenaci\u00f3n de listas:\r\n  En la teor\u00eda List.thy est\u00e1 definida la concatenaci\u00f3n de listas (que\r\n  se representa por @) como sigue\r\n     append_Nil:  \"[]@ys = ys\"\r\n     append_Cons: \"(x#xs)@ys = x#(xs@ys)\"\r\n*}\r\n\r\ntext {*\r\n  Lema. [Ejemplo de inducci\u00f3n sobre listas]\r\n  La concatenaci\u00f3n de listas es asociativa.\r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma conc_asociativa_1: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\nby (induct xs) simp_all\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma conc_asociativa: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\nproof (induct xs)\r\n  show \"[] @ (ys @ zs) = ([] @ ys) @ zs\"\r\n  proof -\r\n    have \"[] @ (ys @ zs) = ys @ zs\" by simp\r\n    also have \"\u2026 = ([] @ ys) @ zs\" by simp\r\n    finally show ?thesis .\r\n  qed\r\nnext\r\n  fix x xs\r\n  assume HI: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\n  show \"(x#xs) @ (ys @ zs) = ((x#xs) @ ys) @ zs\"\r\n  proof -\r\n    have \"(x#xs) @ (ys @ zs) = x#(xs @ (ys @ zs))\" by simp\r\n    also have \"\u2026 = x#((xs @ ys) @ zs)\" using HI by simp\r\n    also have \"\u2026 = (x#(xs @ ys)) @ zs\" by simp\r\n    also have \"\u2026 = ((x#xs) @ ys) @ zs\" by simp\r\n    finally show ?thesis .\r\n  qed\r\nqed\r\n\r\ntext {* \r\n  Ejemplo de definici\u00f3n de tipos recursivos:\r\n  Definir un tipo de dato para los \u00e1rboles binarios.\r\n*}\r\n\r\ndatatype 'a arbolB = Hoja \"'a\" \r\n                   | Nodo \"'a\" \"'a arbolB\" \"'a arbolB\"\r\n\r\ntext {* \r\n  Ejemplo de definici\u00f3n sobre \u00e1rboles binarios:\r\n  Definir la funci\u00f3n \"espejo\" que aplicada a un \u00e1rbol devuelve su imagen\r\n  especular.  \r\n*}\r\n\r\nfun espejo :: \"'a arbolB \u21d2 'a arbolB\" where\r\n  \"espejo (Hoja a) = (Hoja a)\"\r\n| \"espejo (Nodo f x y) = (Nodo f (espejo y) (espejo x))\"\r\n\r\ntext {* \r\n  Ejemplo de demostraci\u00f3n sobre \u00e1rboles binarios:\r\n  Demostrar que la funci\u00f3n \"espejo\" es involutiva; es decir, para\r\n  cualquier \u00e1rbol t, se tiene que \r\n     espejo (espejo(t)) = t.\r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma espejo_involutiva_1: \r\n  \"espejo(espejo(t)) = t\"\r\nby (induct t) auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma espejo_involutiva: \r\n  \"espejo(espejo(t)) = t\" (is \"?P t\")\r\nproof (induct t)\r\n  fix x :: 'a show \"?P (Hoja x)\" by simp \r\nnext\r\n  fix t1 :: \"'a arbolB\" assume h1: \"?P t1\"\r\n  fix t2 :: \"'a arbolB\" assume h2: \"?P t2\"\r\n  fix x :: 'a\r\n  show \"?P (Nodo x t1 t2)\" \r\n  proof -\r\n    have \"espejo(espejo(Nodo x t1 t2)) = espejo(Nodo x (espejo t2) (espejo t1))\"\r\n      by simp\r\n    also have \"\u2026 = Nodo x (espejo (espejo t1)) (espejo (espejo t2))\" by simp\r\n    also have \"\u2026 = Nodo x t1 t2\" using h1 h2 by simp \r\n    finally show ?thesis .\r\n qed\r\nqed\r\n\r\ntext {* \r\n  Ejemplo. [Aplanamiento de \u00e1rboles]\r\n  Definir la funci\u00f3n \"aplana\" que aplane los \u00e1rboles recorri\u00e9ndolos en\r\n  orden infijo.  \r\n*}\r\n\r\nfun aplana :: \"'a arbolB \u21d2 'a list\" where\r\n  \"aplana (Hoja a) = [a]\"\r\n| \"aplana (Nodo x t1 t2) = (aplana t1)@[x]@(aplana t2)\"\r\n\r\ntext {* \r\n  Ejemplo. [Aplanamiento de la imagen especular] Demostrar que\r\n     aplana (espejo t) = rev (aplana t)\r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"aplana (espejo t) = rev (aplana t)\"\r\nby (induct t) auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"aplana (espejo t) = rev (aplana t)\" (is \"?P t\")\r\nproof (induct t)\r\n  fix x :: 'a \r\n  show \"?P (Hoja x)\" by simp \r\nnext\r\n  fix t1 :: \"'a arbolB\" assume h1: \"?P t1\"\r\n  fix t2 :: \"'a arbolB\" assume h2: \"?P t2\"\r\n  fix x :: 'a\r\n  show \"?P (Nodo x t1 t2)\" \r\n  proof -\r\n    have \"aplana (espejo (Nodo x t1 t2)) = \r\n          aplana (Nodo x (espejo t2) (espejo t1))\" by simp\r\n    also have \"\u2026 = (aplana(espejo t2))@[x]@(aplana(espejo t1))\" by simp\r\n    also have \"\u2026 = (rev(aplana t2))@[x]@(rev(aplana t1))\" using h1 h2 by simp\r\n    also have \"\u2026 = rev((aplana t1)@[x]@(aplana t2))\" by simp\r\n    also have \"\u2026 = rev(aplana (Nodo x t1 t2))\" by simp\r\n    finally show ?thesis .\r\n qed\r\nqed\r\n\r\nsection {* Heur\u00edsticas para la inducci\u00f3n *}\r\n\r\ntext {*\r\n  Definici\u00f3n. [Definici\u00f3n recursiva de inversa]\r\n  (inversa xs) la inversa de la lista xs. Por ejemplo,\r\n     inversa [a,b,c] = [c,b,a] \r\n*}\r\n\r\nfun inversa :: \"'a list \u21d2 'a list\" where\r\n  \"inversa [] = []\" \r\n| \"inversa (x#xs) = (inversa xs) @ [x]\"\r\n\r\nvalue \"inversa [a,b,c]\"\r\n\r\ntext {* \r\n  Definici\u00f3n. [Definici\u00f3n de inversa con acumuladores]\r\n  (inversaAc xs) es la inversa de la lista xs calculada con\r\n  acumuladores. Por ejemplo,\r\n     inversaAc [a,b,c]       = [c,b,a] \r\n     inversaAcAux [a,b,c] [] = [c,b,a] \r\n*}\r\n\r\nfun inversaAcAux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\r\n  \"inversaAcAux [] ys = ys\" \r\n| \"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)\"\r\n\r\ndefinition inversaAc :: \"'a list \u21d2 'a list\" where\r\n  \"inversaAc xs \u2261 inversaAcAux xs []\"\r\n\r\nvalue \"inversaAcAux [a,b,c] []\"\r\nvalue \"inversaAc [a,b,c]\"\r\n\r\ntext {* \r\n  Lema. [Ejemplo de equivalencia entre las definiciones]\r\n  La inversa de [a,b,c] es lo mismo calculada con la primera definici\u00f3n\r\n  que con la segunda.\r\n*}\r\n\r\nlemma \"inversaAc [a,b,c] = inversa [a,b,c]\"\r\nby (simp add: inversaAc_def)\r\n\r\ntext {*\r\n  Nota. [Ejemplo fallido de demostraci\u00f3n por inducci\u00f3n]\r\n  El siguiente intento de demostrar que para cualquier lista xs, se\r\n  tiene que  \"inversaAc xs = inversa xs\" falla.\r\n*}\r\n\r\nlemma \"inversaAc xs = inversa xs\"\r\nproof (induct xs)\r\n  show \"inversaAc [] = inversa []\" by (simp add: inversaAc_def)\r\nnext\r\n  fix a xs assume HI: \"inversaAc xs = inversa xs\"\r\n  have \"inversaAc (a#xs) = inversaAcAux (a#xs) []\" by (simp add: inversaAc_def)\r\n  also have \"\u2026 = inversaAcAux xs [a]\" by simp\r\n  also have \"\u2026 = inversa (a#xs)\"\r\n  -- \"Problema: la hip\u00f3tesis de inducci\u00f3n no es aplicable.\"\r\noops\r\n\r\ntext {* \r\n  Nota. [Heur\u00edstica de generalizaci\u00f3n]\r\n  Cuando se use demostraci\u00f3n estructural, cuantificar universalmente las \r\n  variables libres (o, equivalentemente, considerar las variables libres\r\n  como variables arbitrarias).\r\n\r\n  Lema. [Lema con generalizaci\u00f3n]\r\n  Para toda lista ys se tiene \r\n     inversaAcAux xs ys = (inversa xs) @ ys\r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma inversaAcAux_es_inversa_1:\r\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\r\nby (induct xs arbitrary: ys) auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma inversaAcAux_es_inversa:\r\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\r\nproof (induct xs arbitrary: ys)\r\n  show \"\u22c0ys. inversaAcAux [] ys = (inversa [])@ys\" by simp\r\nnext\r\n  fix a xs \r\n  assume HI: \"\u22c0ys. inversaAcAux xs ys = inversa xs@ys\"\r\n  show \"\u22c0ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys\"\r\n  proof -\r\n    fix ys\r\n    have \"inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)\" by simp\r\n    also have \"\u2026 = inversa xs@(a#ys)\" using HI by simp\r\n    also have \"\u2026 = inversa (a#xs)@ys\" by simp \r\n    finally show \"inversaAcAux (a#xs) ys = inversa (a#xs)@ys\" by simp\r\n  qed\r\nqed\r\n\r\ntext {*\r\n  Corolario.  Para cualquier lista xs, se tiene que\r\n     inversaAc xs = inversa xs\r\n*}\r\n\r\ncorollary \"inversaAc xs = inversa xs\"\r\nby (simp add: inversaAcAux_es_inversa inversaAc_def)\r\n\r\ntext {*\r\n  Nota. En el paso \"inversa xs@(a#ys) = inversa (a#xs)@ys\" se usan\r\n  lemas de la teor\u00eda List. Se puede observar, activando \"Trace\r\n  Simplifier\" y D\"|Trace Rules\", que los lemas usados son \r\n  \u00b7 append_assoc:       (xs @ ys) @ zs = xs @ (ys @ zs)\r\n  \u00b7 append.append_Cons: (x#xs)@ys = x#(xs@ys)\r\n  \u00b7 append.append_Nil:  []@ys = ys\r\n  Los dos \u00faltimos son las ecuaciones de la definici\u00f3n de append.\r\n\r\n  En la siguiente demostraci\u00f3n se detallan los lemas utilizados.\r\n*}\r\n\r\nlemma \"(inversa xs)@(a#ys) = (inversa (a#xs))@ys\"\r\nproof -\r\n  have \"(inversa xs)@(a#ys) = (inversa xs)@(a#([]@ys))\" \r\n    by (simp only:append.append_Nil)\r\n  also have \"\u2026 = (inversa xs)@([a]@ys)\" by (simp only:append.append_Cons)\r\n  also have \"\u2026 = ((inversa xs)@[a])@ys\" by (simp only:append_assoc)\r\n  also have \"\u2026 = (inversa (a#xs))@ys\" by (simp only:inversa.simps(2))\r\n  finally show ?thesis .\r\nqed\r\n\r\nsection {* Recursi\u00f3n general. La funci\u00f3n de Ackermann *}\r\n\r\ntext {* \r\n  El objetivo de esta secci\u00f3n es mostrar el uso de las definiciones\r\n  recursivas generales y sus esquemas de inducci\u00f3n. Como ejemplo se usa la\r\n  funci\u00f3n de Ackermann (se puede consultar informaci\u00f3n sobre dicha funci\u00f3n en\r\n  http:\/\/en.wikipedia.org\/wiki\/Ackermann_function).\r\n\r\n  Definici\u00f3n.  La funci\u00f3n de Ackermann se define por\r\n    A(m,n) = n+1,             si m=0,\r\n             A(m-1,1),        si m>0 y n=0,\r\n             A(m-1,A(m,n-1)), si m>0 y n>0\r\n  para todo los n\u00fameros naturales. \r\n\r\n  La funci\u00f3n de Ackermann es recursiva, pero no es primitiva recursiva. \r\n*}\r\n\r\nfun ack :: \"nat \u21d2 nat \u21d2 nat\" where\r\n  \"ack 0 n = n+1\" \r\n| \"ack (Suc m) 0 = ack m 1\" \r\n| \"ack (Suc m) (Suc n) = ack m (ack (Suc m) n)\"\r\n\r\n-- \"Ejemplo de evaluaci\u00f3n\"\r\nvalue \"ack 2 3\" (* devuelve 9 *)\r\n\r\ntext {*\r\n  Esquema de inducci\u00f3n correspondiente a una funci\u00f3n:\r\n  \u00b7 Al definir una funci\u00f3n recursiva general se genera una regla de\r\n    inducci\u00f3n. En la definici\u00f3n anterior, la regla generada es\r\n    ack.induct: \r\n       \u27e6\u22c0n. P 0 n; \r\n        \u22c0m. P m 1 \u27f9 P (Suc m) 0;\r\n        \u22c0m n. \u27e6P (Suc m) n; P m (ack (Suc m) n)\u27e7 \u27f9 P (Suc m) (Suc n)\u27e7\r\n       \u27f9 P a b\r\n*}\r\n\r\ntext {*\r\n  Ejemplo de demostraci\u00f3n por la inducci\u00f3n correspondiente a una funci\u00f3n:\r\n  Para todos m y n, A(m,n) > n.\r\n*} \r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"ack m n > n\"\r\nby (induct m n rule: ack.induct) simp_all\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"ack m n > n\"\r\nproof (induct m n rule: ack.induct)\r\n  fix n :: \"nat\"\r\n  show \"ack 0 n > n\" by simp\r\nnext\r\n  fix m assume \"ack m 1 > 1\"\r\n  thus \"ack (Suc m) 0 > 0\" by simp\r\nnext  \r\n  fix m n\r\n  assume \"n < ack (Suc m) n\" and \r\n         \"ack (Suc m) n < ack m (ack (Suc m) n)\"\r\n  thus \"Suc n < ack (Suc m) (Suc n)\" by simp\r\nqed\r\n\r\ntext {*\r\n  Nota. [Inducci\u00f3n sobre recursi\u00f3n]\r\n  El formato para iniciar una demostraci\u00f3n por inducci\u00f3n en la regla\r\n  inductiva correspondiente a la definici\u00f3n recursiva de la funci\u00f3n f m\r\n  n es \r\n     proof (induct m n rule:f.induct) \r\n*}\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha presentado los m\u00e9todos de demostraci\u00f3n por casos y por inducci\u00f3n iniciados en Isabelle\/HOL. La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[1],"tags":[144,203],"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\/3263"}],"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=3263"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3263\/revisions"}],"predecessor-version":[{"id":3264,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3263\/revisions\/3264"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3263"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3263"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3263"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}