{"id":6359,"date":"2018-11-22T19:29:21","date_gmt":"2018-11-22T18:29:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6359"},"modified":"2018-11-23T13:30:14","modified_gmt":"2018-11-23T12:30:14","slug":"ra2018-razonamiento-estructurado-sobre-programas-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2018-razonamiento-estructurado-sobre-programas-con-isabelle-hol\/","title":{"rendered":"RA2018: Razonamiento estructurado sobre programas con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-18\">Razonamiento autom\u00e1tico<\/a> se ha presentado c\u00f3mo se puede demostrar propiedades de programas funcionales con Isabelle\/HOL.<\/p>\n<p>Para ello, se ha visto c\u00f3mo representar en Isabelle\/HOL las demostraciones de propiedades de programas estudiadas en el <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-17\/temas\/tema-8.pdf\">tema 8 del curso de Inform\u00e1tica<\/a>.<\/p>\n<p>Los m\u00e9todos de demostraci\u00f3n utilizados son razonamiento ecuacional, inducci\u00f3n sobre los n\u00fameros naturales, inducci\u00f3n sobre listas e inducci\u00f3n sobre esquemas correspondientes a definiciones recursivas.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* Tema 3: Razonamiento estructurado sobre programas *}\n\ntheory T3_Razonamiento_sobre_programas\nimports Main \nbegin\n\ntext {* \n  En este tema se demuestra con Isabelle las propiedades de los\n  programas funcionales como se expone en el tema 2a y se demostraron\n  autom\u00e1ticamente en el tema 2b. A diferencia del tema 2b, ahora\n  nos fijamos no s\u00f3lo en el m\u00e9todo de demostraci\u00f3n sino en la estructura\n  de la prueba resaltando su semejanza con las del tema 2a. *}\n\ndeclare [[names_short]]\n\nsection {* Razonamiento ecuacional *}\n\ntext {* ----------------------------------------------------------------\n  Ejemplo 1. Definir, por recursi\u00f3n, la funci\u00f3n\n     longitud :: 'a list \u21d2 nat\n  tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,\n     longitud [a,c,d] = 3\n  ------------------------------------------------------------------- *}\n\nfun longitud :: \"'a list \u21d2 nat\" where\n  \"longitud []     = 0\"\n| \"longitud (x#xs) = 1 + longitud xs\"\n   \nvalue \"longitud [a,c,d] = 3\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 2. Demostrar que \n     longitud [a,c,d] = 3\n  ------------------------------------------------------------------- *}\n\nlemma \"longitud [a,c,d] = 3\"\nby simp\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 3. Definir la funci\u00f3n\n     fun intercambia :: 'a \u00d7 'b \u21d2 'b \u00d7 'a\n  tal que (intercambia p) es el par obtenido intercambiando las\n  componentes del par p. Por ejemplo,\n     intercambia (u,v) = (v,u)\n  ------------------------------------------------------------------ *}\n\nfun intercambia :: \"'a \u00d7 'b \u21d2 'b \u00d7 'a\" where\n  \"intercambia (x,y) = (y,x)\"\n\nvalue \"intercambia (u,v) = (v,u)\"\n\ntext {*\n  La definici\u00f3n de la funci\u00f3n intercambia genera una regla de\n  simplificaci\u00f3n\n  \u00b7 intercambia.simps: intercambia (x,y) = (y,x)\n  \n  Se puede ver con \n  \u00b7 thm intercambia.simps \n*}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 4. (p.6) Demostrar que \n     intercambia (intercambia (x,y)) = (x,y)\n  ------------------------------------------------------------------- *}\n\n(* Demostraci\u00f3n aplicativa *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  apply (simp only: intercambia.simps)\n  done\n\n(* Demostraci\u00f3n declarativa *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\nproof -\n  have \"intercambia (intercambia (x,y)) = intercambia (y,x)\"  \n    by (simp only: intercambia.simps)\n  also have \"... = (x,y)\" \n    by (simp only: intercambia.simps)\n  finally show \"intercambia (intercambia (x,y)) = (x,y)\" \n    by simp\nqed\n\ntext {*\n  Notas sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"proof\" para iniciar la prueba,\n  \u00b7 \"-\" (despu\u00e9s de \"proof\") para no usar el m\u00e9todo por defecto,\n  \u00b7 \"have\" para establecer un paso,\n  \u00b7 \"by (simp only: intercambia.simps)\" para indicar que s\u00f3lo se usa\n    como regla de escritura la correspondiente a la definici\u00f3n de\n    intercambia,\n  \u00b7 \"also\" para encadenar pasos ecuacionales,\n  \u00b7 \"...\" para representar la derecha de la igualdad anterior en un\n    razonamiento ecuacional,\n  \u00b7 \"finally\" para indicar el \u00faltimo pasa de un razonamiento ecuacional,\n  \u00b7 \"show\" para establecer la conclusi\u00f3n.\n  \u00b7 \"by simp\" para indicar el m\u00e9todo de demostraci\u00f3n por simplificaci\u00f3n y \n  \u00b7 \"qed\" para terminar la pruebas,\n*}\n\n(* Demostraci\u00f3n declarativa simplificada *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\nproof -\n  have \"intercambia (intercambia (x,y)) = intercambia (y,x)\"  by simp\n  also have \"... = (x,y)\" by simp \n  finally show \"intercambia (intercambia (x,y)) = (x,y)\" by simp\nqed\n\ntext {*\n  Nota: La diferencia entre las dos demostraciones es que en los dos\n  primeros pasos no se explicita la regla de simplificaci\u00f3n.\n*}\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  by simp\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 5. Definir, por recursi\u00f3n, la funci\u00f3n\n     inversa :: 'a list \u21d2 'a list\n  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los\n  elementos de xs. Por ejemplo,\n     inversa [a,d,c] = [c,d,a]\n  ------------------------------------------------------------------ *}\n\nfun inversa :: \"'a list \u21d2 'a list\" where\n  \"inversa []     = []\"\n| \"inversa (x#xs) = inversa xs @ [x]\"\n\nvalue \"inversa [a,d,c] = [c,d,a]\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 6. (p. 9) Demostrar que \n     inversa [x] = [x]\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"inversa [x] = [x]\"\n  apply simp\n  done\n\ntext {*\n  En la demostraci\u00f3n anterior se usaron las siguientes reglas:\n  \u00b7 inversa.simps(1): inversa [] = []\n  \u00b7 inversa.simps(2): inversa (x#xs) = inversa xs @ [x]\n  \u00b7 append_Nil:       [] @ ys = ys\n  Vamos a explicitar su aplicaci\u00f3n.\n*}\n  \n(* La demostraci\u00f3n aplicativa detallada es *)\nlemma \"inversa [x] = [x]\"\n  apply (simp only: inversa.simps(2))\n  apply (simp only: inversa.simps(1))\n  apply (simp only: append_Nil)\n  done\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"inversa [x] = [x]\"\nproof -\n  have \"inversa [x] = inversa (x#[])\" by simp\n  also have \"... = (inversa []) @ [x]\" by (simp only: inversa.simps(2))\n  also have \"... = [] @ [x]\" by (simp only: inversa.simps(1))\n  also have \"... = [x]\" by (simp only: append_Nil) \n  finally show \"inversa [x] = [x]\" by simp\nqed\n\n(* La demostraci\u00f3n declarativa simplificada es *)\nlemma \"inversa [x] = [x]\"\nproof -\n  have \"inversa [x] = inversa (x#[])\" by simp\n  also have \"... = (inversa []) @ [x]\" by simp\n  also have \"... = [] @ [x]\" by simp\n  also have \"... = [x]\" by simp \n  finally show \"inversa [x] = [x]\" by simp\nqed\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"inversa [x] = [x]\"\n  by simp\n\nsection {* Razonamiento por inducci\u00f3n sobre los naturales *}\n\ntext {*\n  [Principio de inducci\u00f3n sobre los naturales] Para demostrar una\n  propiedad P para todos los n\u00fameros naturales basta probar que el 0\n  tiene la propiedad P y que si n tiene la propiedad P, entonces n+1\n  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 sobre los naturales est\u00e1\n  formalizado en el teorema nat.induct y puede verse con\n     thm nat.induct\n*}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 7. Definir la funci\u00f3n\n     repite :: nat \u21d2 'a \u21d2 'a list\n  tal que (repite n x) es la lista formada por n copias del elemento\n  x. Por ejemplo, \n     repite 3 a = [a,a,a]\n  ------------------------------------------------------------------ *}\n\nfun repite :: \"nat \u21d2 'a \u21d2 'a list\" where\n  \"repite 0 x       = []\"\n| \"repite (Suc n) x = x # (repite n x)\"\n\nvalue \"repite 3 a = [a,a,a]\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 8. (p. 18) Demostrar que \n     longitud (repite n x) = n\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"longitud (repite n x) = n\"\n  apply (induct n)\n   apply simp_all\n  done\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"longitud (repite n x) = n\"\nproof (induct n)\n  show \"longitud (repite 0 x) = 0\" by simp\nnext \n  fix n\n  assume HI: \"longitud (repite n x) = n\"\n  have \"longitud (repite (Suc n) x) = longitud (x # (repite n x))\" \n    by simp\n  also have \"... = 1 + longitud (repite n x)\" by simp\n  also have \"... = 1 + n\" using HI by simp\n  finally show \"longitud (repite (Suc n) x) = Suc n\" by simp\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 A la derecha de proof se indica el m\u00e9todo de la demostraci\u00f3n.\n  \u00b7 (induct n) indica que la demostraci\u00f3n se har\u00e1 por inducci\u00f3n en n.\n  \u00b7 Se generan dos subobjetivos correspondientes a la base y el paso de\n    inducci\u00f3n:\n    1. longitud (repite 0 x) = 0\n    2. \u22c0n. longitud (repite n x) = n \u27f9 longitud (repite (Suc n) x) = Suc n\n    donde \u22c0n se lee \"para todo n\".  \n  \u00b7 \"next\" indica el siguiente subobjetivo.\n  \u00b7 \"fix n\" indica \"sea n un n\u00famero natural cualquiera\"\n  \u00b7 assume HI: \"longitud (repite n x) = n\" indica \u00absupongamos que \n    \"longitud (repite n x) = n\" y sea HI la etiqueta de este supuesto\u00bb.\n  \u00b7 \"using HI\" usando la propiedad etiquetada con HI. \n*}\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"longitud (repite n x) = n\"\n  by (induct n) auto\n\nsection {* Razonamiento por inducci\u00f3n sobre listas *}\n\ntext {*\n  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\n  una lista que tiene la propiedad se obtiene otra lista que tambi\u00e9n\n  tiene la propiedad. \n\n  En Isabelle el principio de inducci\u00f3n sobre listas est\u00e1 formalizado\n  mediante el teorema list.induct \n     \u27e6P []; \n      \u22c0x xs. P xs \u27f9 P (x#xs)\u27e7 \n     \u27f9 P xs\n*}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 9. Definir la funci\u00f3n\n     conc :: 'a list \u21d2 'a list \u21d2 'a list\n  tal que (conc xs ys) es la concatenci\u00f3n de las listas xs e ys. Por\n  ejemplo, \n     conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]\n  ------------------------------------------------------------------ *}\n\nfun conc :: \"'a list \u21d2 'a list \u21d2 'a list\" where\n  \"conc []     ys = ys\"\n| \"conc (x#xs) ys = x # (conc xs ys)\"\n\nvalue \"conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 10. (p. 24) Demostrar que \n     conc xs (conc ys zs) = (conc xs ys) zs\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\nproof (induct xs)\n  show \"conc [] (conc ys zs) = conc (conc [] ys) zs\" by simp\nnext\n  fix x xs\n  assume HI: \"conc xs (conc ys zs) = conc (conc xs ys) zs\" \n  have \"conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))\" by simp\n  also have \"... = x # (conc (conc xs ys) zs)\" using HI by simp\n  also have \"... = conc (conc (x # xs) ys) zs\" by simp\n  finally show \"conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs\" \n    by simp\nqed\n\ntext {*\n  Comentario sobre la demostraci\u00f3n anterior\n  \u00b7 (induct xs) genera dos subobjetivos:\n    1. conc [] (conc ys zs) = conc (conc [] ys) zs\n    2. \u22c0a xs. conc xs (conc ys zs) = conc (conc xs ys) zs \u27f9\n              conc (a#xs) (conc ys zs) = conc (conc (a#xs) ys) zs\n*}\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\n  by (induct xs) auto\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 11. Refutar que \n     conc xs ys = conc ys xs\n  ------------------------------------------------------------------- *}\n\nlemma \"conc xs ys = conc ys xs\"\n  quickcheck\n  oops\n\ntext {* Encuentra el contraejemplo, \n  xs = [a2]\n  ys = [a1] *}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 12. (p. 28) Demostrar que \n     conc xs [] = xs\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"conc xs [] = xs\"\nproof (induct xs)\n  show \"conc [] [] = []\" by simp\nnext \n  fix x xs\n  assume HI: \"conc xs [] = xs\" \n  have \"conc (x # xs) [] = x # (conc xs [])\" by simp\n  also have \"... = x # xs\" using HI by simp\n  finally show \"conc (x # xs) [] = x # xs\" by simp\nqed\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"conc xs [] = xs\"\n  by (induct xs) simp_all\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 13. (p. 30) Demostrar que \n     longitud (conc xs ys) = longitud xs + longitud ys\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\nproof (induct xs)\n  show \"longitud (conc [] ys) = longitud [] + longitud ys\" by simp\nnext\n  fix x xs\n  assume HI: \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  have \"longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))\" \n    by simp\n  also have \"... = 1 + longitud (conc xs ys)\" by simp\n  also have \"... = 1 + longitud xs + longitud ys\" using HI by simp\n  also have \"... = longitud (x # xs) + longitud ys\" by simp\n  finally show \"longitud (conc (x # xs) ys) = \n                longitud (x # xs) + longitud ys\" by simp\nqed\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  by (induct xs) auto\n\nsection {* Inducci\u00f3n correspondiente a la definici\u00f3n recursiva *}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 14. Definir la funci\u00f3n\n     coge :: nat \u21d2 'a list \u21d2 'a list\n  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por \n  ejemplo, \n     coge 2 [a,c,d,b,e] = [a,c]\n  ------------------------------------------------------------------ *}\n\nfun coge :: \"nat \u21d2 'a list \u21d2 'a list\" where\n  \"coge n []           = []\"\n| \"coge 0 xs           = []\"\n| \"coge (Suc n) (x#xs) = x # (coge n xs)\"\n\nvalue \"coge 2 [a,c,d,b,e] = [a,c]\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 15. Definir la funci\u00f3n\n     elimina :: nat \u21d2 'a list \u21d2 'a list\n  tal que (elimina n xs) es la lista obtenida eliminando los n primeros\n  elementos de xs. Por ejemplo, \n     elimina 2 [a,c,d,b,e] = [d,b,e]\n  ------------------------------------------------------------------ *}\n\nfun elimina :: \"nat \u21d2 'a list \u21d2 'a list\" where\n  \"elimina n []           = []\"\n| \"elimina 0 xs           = xs\"\n| \"elimina (Suc n) (x#xs) = elimina n xs\"\n\nvalue \"elimina 2 [a,c,d,b,e] = [d,b,e]\"\n\ntext {* \n  La definici\u00f3n coge genera el esquema de inducci\u00f3n coge.induct:\n     \u27e6\u22c0n. P n []; \n      \u22c0x xs. P 0 (x#xs); \n      \u22c0n x xs. P n xs \u27f9 P (Suc n) (x#xs)\u27e7\n     \u27f9 P n x\n\n  Puede verse usando \"thm coge.induct\". *}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 16. (p. 35) Demostrar que \n     conc (coge n xs) (elimina n xs) = xs\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\nproof (induct rule: coge.induct)\n  fix n\n  show \"conc (coge n []) (elimina n []) = []\" by simp\nnext\n  fix x xs\n  show \"conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs\" by simp\nnext\n  fix n x xs\n  assume HI: \"conc (coge n xs) (elimina n xs) = xs\"\n  have \"conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = \n        conc (x#(coge n xs)) (elimina n xs)\" by simp\n  also have \"... = x#(conc (coge n xs) (elimina n xs))\" by simp\n  also have \"... = x#xs\" using HI by simp  \n  finally show \"conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = \n                x#xs\"\n    by simp\nqed\n\ntext {*\n  Comentario sobre la demostraci\u00f3n anterior:\n  \u00b7 (induct rule: coge.induct) indica que el m\u00e9todo de demostraci\u00f3n es\n    por el esquema de inducci\u00f3n correspondiente a la definici\u00f3n de la\n    funci\u00f3n coge.\n  \u00b7 Se generan 3 subobjetivos:\n    \u00b7 1. \u22c0n. conc (coge n []) (elimina n []) = []\n    \u00b7 2. \u22c0x xs. conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs\n    \u00b7 3. \u22c0n x xs. \n            conc (coge n xs) (elimina n xs) = xs \u27f9\n            conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs\n*}\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\n  by (induct rule: coge.induct) auto\n\nsection {* Razonamiento por casos *}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 17. Definir la funci\u00f3n\n     esVacia :: 'a list \u21d2 bool\n  tal que (esVacia xs) se verifica si xs es la lista vac\u00eda. Por ejemplo,\n     esVacia []  = True\n     esVacia [1] = False\n  ------------------------------------------------------------------ *}\n\nfun esVacia :: \"'a list \u21d2 bool\" where\n  \"esVacia []     = True\"\n| \"esVacia (x#xs) = False\"\n\nvalue \"esVacia []  = True\"\nvalue \"esVacia [a] = False\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 18 (p. 39) . Demostrar que \n     esVacia xs = esVacia (conc xs xs)\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  assume \"xs = []\"\n  then show \"esVacia xs = esVacia (conc xs xs)\" by simp\nnext\n  fix y ys\n  assume \"xs = y#ys\"\n  then show \"esVacia xs = esVacia (conc xs xs)\" by simp\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"(cases xs)\" es el m\u00e9todo de demostraci\u00f3n por casos seg\u00fan xs.\n  \u00b7 Se generan dos subobjetivos  correspondientes a los dos\n    constructores de listas:\n    \u00b7 1. xs = [] \u27f9 esVacia xs = esVacia (conc xs xs)\n    \u00b7 2. \u22c0y ys. xs = y#ys \u27f9 esVacia xs = esVacia (conc xs xs)\n  \u00b7 \"then\" indica \"usando la propiedad anterior\"\n*}\n\n(* La demostraci\u00f3n estructurada simplificada es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  case Nil\n  then show \"esVacia xs = esVacia (conc xs xs)\" by simp\nnext\n  case Cons\n  then show \"esVacia xs = esVacia (conc xs xs)\" by simp\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"case Nil\" es una abreviatura de \"assume xs = []\"\n  \u00b7 \"case Cons\" es una abreviatura de \"fix y ys assume xs = y#ys\"\n  \u00b7 \"thus\" es una abreviatura de \"then show\".\n*}\n\n(* La demostraci\u00f3n con el patr\u00f3n sugerido es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  case Nil\n  then show ?thesis by simp\nnext\n  case (Cons x xs)\n  then show ?thesis by simp\nqed\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\n  by (cases xs) auto\n\nsection {* Heur\u00edstica de generalizaci\u00f3n *}\n\ntext {* \n  Heur\u00edstica de generalizaci\u00f3n: Cuando se use demostraci\u00f3n estructural,\n  cuantificar universalmente las variables libres (o, equivalentemente,\n  considerar las variables libres como variables arbitrarias). *}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 19. Definir la funci\u00f3n\n     inversaAc :: 'a list \u21d2 'a list\n  tal que (inversaAc xs) es a inversa de xs calculada usando\n  acumuladores. Por ejemplo, \n     inversaAc [a,c,b,e] = [e,b,c,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\nfun inversaAc :: \"'a list \u21d2 'a list\" where\n  \"inversaAc xs = inversaAcAux xs []\"\n\nvalue \"inversaAc [a,c,b,e] = [e,b,c,a]\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 20. (p. 44) Demostrar que \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\" by simp \n    finally show \"inversaAcAux (a#xs) ys = inversa (a#xs)@ys\" by simp\n  qed\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"(induct xs arbitrary: ys)\" es el m\u00e9todo de demostraci\u00f3n por\n    inducci\u00f3n sobre xs usando ys como variable arbitraria.\n  \u00b7 Se generan dos subobjetivos:\n    \u00b7 1. \u22c0ys. inversaAcAux [] ys = inversa [] @ ys\n    \u00b7 2. \u22c0a xs ys. (\u22c0ys. inversaAcAux xs ys = inversa xs @ ys) \u27f9\n                    inversaAcAux (a # xs) ys = inversa (a # xs) @ ys\n  \u00b7 Dentro de una demostraci\u00f3n se pueden incluir otras demostraciones.\n  \u00b7 Para demostrar la propiedad universal \"\u22c0ys. P(ys)\" se elige una\n    lista arbitraria (con \"fix ys\") y se demuestra \"P(ys)\". \n*}\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"inversaAcAux xs ys = (inversa xs)@ys\"\n  by (induct xs arbitrary: ys) auto\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 21. (p. 43) Demostrar que \n     inversaAc xs = inversa xs\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\ncorollary \"inversaAc xs = inversa xs\"\n  by (simp add: inversaAcAux_es_inversa)\n\ntext {*\n  Comentario de la demostraci\u00f3n anterior:\n  \u00b7 \"(simp add: inversaAcAux_es_inversa)\" es el m\u00e9todo de demostraci\u00f3n\n    por simplificaci\u00f3n usando como regla de simplificaci\u00f3n la propiedad\n    inversaAcAux_es_inversa. \n*}\n\nsection {* Demostraci\u00f3n por inducci\u00f3n para funciones de orden superior *}\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 22. Definir la funci\u00f3n\n     sum :: nat list \u21d2 nat\n  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,\n     sum [3,2,5] = 10\n  ------------------------------------------------------------------ *}\n\nfun sum :: \"nat list \u21d2 nat\" where\n  \"sum []     = 0\"\n| \"sum (x#xs) = x + sum xs\"\n\nvalue \"sum [3,2,5] = 10\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 23. Definir la funci\u00f3n\n     map :: ('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\n  tal que (map f xs) es la lista obtenida aplicando la funci\u00f3n f a los\n  elementos de xs. Por ejemplo,\n     map (\u03bbx. 2*x) [3,2,5] = [6,4,10]\n  ------------------------------------------------------------------ *}\n\nfun map :: \"('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\" where\n  \"map f []     = []\"\n| \"map f (x#xs) = (f x) # map f xs\"\n\nvalue \"map (\u03bbx. 2*x) [3::nat,2,5] = [6,4,10]\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 24. (p. 45) Demostrar que \n     sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\nproof (induct xs)\n  show \"sum (map (\u03bbx. 2*x) []) = 2 * (sum [])\" by simp\nnext\n  fix a xs\n  assume HI: \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\n  have \"sum (map (\u03bbx. 2*x) (a#xs)) = sum ((2*a)#(map (\u03bbx. 2*x) xs))\" \n    by simp\n  also have \"... = 2*a + sum (map (\u03bbx. 2*x) xs)\" by simp\n  also have \"... = 2*a + 2*(sum xs)\" using HI by simp\n  also have \"... = 2*(a + sum xs)\" by simp\n  also have \"... = 2*(sum (a#xs))\" by simp\n  finally show \"sum (map (\u03bbx. 2*x) (a#xs)) = 2*(sum (a#xs))\" by simp\nqed\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\n  by (induct xs) auto\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 25. (p. 48) Demostrar que \n     longitud (map f xs) = longitud xs\n  ------------------------------------------------------------------- *}\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"longitud (map f xs) = longitud xs\"\nproof (induct xs)\n  show \"longitud (map f []) = longitud []\" by simp\nnext\n  fix a xs\n  assume HI: \"longitud (map f xs) = longitud xs\"\n  have \"longitud (map f (a#xs)) = longitud (f a # (map f xs))\" by simp\n  also have \"... = 1 + longitud (map f xs)\" by simp\n  also have \"... = 1 + longitud xs\" using HI by simp\n  also have \"... = longitud (a#xs)\" by simp\n  finally show \"longitud (map f (a#xs)) = longitud (a#xs)\" by simp\nqed\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"longitud (map f xs) = longitud xs\"\n  by (induct xs) auto\n\nsection {* Referencias *}\n\ntext {*\n  \u00b7 J.A. Alonso. \"Razonamiento sobre programas\" http:\/\/goo.gl\/R06O3\n  \u00b7 G. Hutton. \"Programming in Haskell\". Cap. 13 \"Reasoning about\n    programms\". \n  \u00b7 S. Thompson. \"Haskell: the Craft of Functional Programming, 3rd\n    Edition. Cap. 8 \"Reasoning about programms\". \n  \u00b7 L. Paulson. \"ML for the Working Programmer, 2nd Edition\". Cap. 6. \n    \"Reasoning about functional programs\". \n*}\n\nend\n<\/pre>\n<p>Como tarea para la pr\u00f3xima clase se propuso la resoluci\u00f3n de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/RA2018\/index.php\/R3\">3\u00aa relaci\u00f3n<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha presentado c\u00f3mo se puede demostrar propiedades de programas funcionales con Isabelle\/HOL. Para ello, se ha visto c\u00f3mo representar en Isabelle\/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Inform\u00e1tica. Los m\u00e9todos de demostraci\u00f3n utilizados son razonamiento ecuacional,&#8230;<\/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":[322],"tags":[144,323],"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\/6359"}],"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=6359"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6359\/revisions"}],"predecessor-version":[{"id":6360,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6359\/revisions\/6360"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6359"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6359"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6359"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}