{"id":1888,"date":"2012-02-16T18:47:38","date_gmt":"2012-02-16T18:47:38","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1888"},"modified":"2013-03-08T05:48:55","modified_gmt":"2013-03-08T05:48:55","slug":"ra2011-demostraciones-por-induccion-en-isabelle","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2011-demostraciones-por-induccion-en-isabelle\/","title":{"rendered":"RA2011: Demostraciones por inducci\u00f3n en Isabelle"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-11\">Razonamiento autom\u00e1tico<\/a> se ha ampliado el estudio de las demostraciones por inducci\u00f3n en Isabelle. Se ha estudiados: <\/p>\n<ul>\n<li>c\u00f3mo a veces es necesario generalizar las propiedades para poderla demostrar por inducci\u00f3n y cuantificar universalmente las variables libres,\n<li>c\u00f3mo definir funciones recursivas que no son primitivas recursivas y c\u00f3mo demostrar propiedades de dichas funciones usando el esquema de inducci\u00f3n generado por su definici\u00f3n y\n<li>c\u00f3mo definir y demostrar propiedades de funciones definidas por recursi\u00f3n cruzada.\n<\/ul>\n<p>La clase se ha basado en la siguiente teor\u00eda Isabelle<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 10: Heur\u00edsticas para la inducci\u00f3n y recursi\u00f3n general *}\r\n\r\ntheory Tema_10\r\nimports Main Tema_7 Efficient_Nat\r\nbegin\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 [2,5,3] = [3,5,2] \r\n*}\r\n\r\nprimrec inversa :: \"'a list \u21d2 'a list\" where\r\n\"inversa [] = []\" |\r\n\"inversa (x#xs) = (inversa xs) @ [x]\"\r\n\r\nvalue \"inversa [2::nat,5,3]\"\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 [2,5,3] = [3,5,2] \r\n     inversaAcAux [2,5,3] [] = [3,5,2] \r\n*}\r\n\r\nprimrec 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 [2::nat,5,3] []\"\r\nvalue \"inversaAc [2::nat,5,3]\"\r\n\r\ntext {* \r\n  Lema. [Ejemplo de equivalencia entre las definiciones]\r\n  La inversa de [1,2,3] es lo mismo calculada con la primera definici\u00f3n que\r\n  con la segunda.\r\n*}\r\n\r\nlemma \"inversaAc [1,2,3] = inversa [1,2,3]\"\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 tiene que\r\n  \"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 como\r\n  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\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\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\ntext {*\r\n  Nota. [Ejemplo de c\u00e1lculo]\r\n  El c\u00e1lculo del valor de la funci\u00f3n de Ackermann para 2 y 3 se realiza\r\n  mediante \"value\"\r\n*}\r\n\r\nvalue \"ack 2 3\" (* devuelve 9 *)\r\n\r\ntext {*\r\n  Nota. [Definiciones recursivas generales]\r\n  \u00b7 Las definiciones recursivas generales se identifican mediante \"fun\".\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  Lema. Para todos m y n, A(m,n) > n.\r\n*} \r\n\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  El lema anterior se puede demostrar autom\u00e1ticamente, como sigue.\r\n*}\r\n\r\nlemma \"ack m n > n\"\r\nby (induct m n rule: ack.induct) simp_all\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 inductiva\r\n  correspondiente a la definici\u00f3n recursiva de la funci\u00f3n f m n es\r\n     proof (induct m n rule:f.induct) \r\n*}\r\n\r\nsection {* Recursi\u00f3n mutua e inducci\u00f3n *}\r\n\r\ntext {*\r\n  Nota. [Ejemplo de definici\u00f3n de tipos mediante recursi\u00f3n cruzada]\r\n  \u00b7 Un \u00e1rbol de tipo a es una hoja o un nodo de tipo a junto con un\r\n    bosque de tipo a.\r\n  \u00b7 Un bosque de tipo a es el boque vac\u00edo o un bosque contruido a\u00f1adiendo\r\n    un \u00e1rbol de tipo a a un bosque de tipo a.\r\n*}\r\n\r\ndatatype 'a arbol = Hoja | Nodo \"'a\" \"'a bosque\"\r\nand      'a bosque = Vacio | ConsB \"'a arbol\" \"'a bosque\"\r\n\r\ntext {*\r\n  Nota. [Regla de inducci\u00f3n correspondiente a la recursi\u00f3n cruzada]\r\n  La regla de inducci\u00f3n sobre \u00e1rboles y bosques es arbol_bosque.induct:\r\n     \u27e6P1 Hoja; \r\n      \u22c0x b. P2 b \u27f9 P1 (Nodo x b); \r\n      P2 Vacio;\r\n      \u22c0a b. \u27e6P1 a; P2 b\u27e7 \u27f9 P2 (ConsB a b)\u27e7 \r\n     \u27f9 P1 a \u2227 P2 b\r\n \r\n  Nota. [Ejemplos de definici\u00f3n por recursi\u00f3n cruzada]\r\n  \u00b7 aplana_arbol a) es la lista obtenida aplanando el \u00e1rbol a.   \r\n  \u00b7 (aplana_bosque b) es la lista obtenida aplanando el bosque b.   \r\n  \u00b7 (map_arbol a h) es el \u00e1rbol obtenido aplicando la funci\u00f3n h a\r\n    todos los nodos del \u00e1rbol a.   \r\n  \u00b7 (map_bosque b h) es el bosque obtenido aplicando la funci\u00f3n h a\r\n    todos los nodos del bosque b. \r\n*}\r\n\r\nfun\r\n  aplana_arbol :: \"'a arbol \u21d2 'a list\" and \r\n  aplana_bosque :: \"'a bosque \u21d2 'a list\" where\r\n  \"aplana_arbol Hoja = []\"\r\n| \"aplana_arbol (Nodo x b) = x#(aplana_bosque b)\"\r\n| \"aplana_bosque Vacio = []\"\r\n| \"aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)\"\r\n\r\nfun\r\n  map_arbol :: \"'a arbol \u21d2 ('a \u21d2 'b) \u21d2 'b arbol\" and\r\n  map_bosque :: \"'a bosque \u21d2 ('a \u21d2 'b) \u21d2 'b bosque\" where\r\n  \"map_arbol Hoja h = Hoja\"\r\n| \"map_arbol (Nodo x b) h = Nodo (h x) (map_bosque b h)\"\r\n| \"map_bosque Vacio h = Vacio\"\r\n| \"map_bosque (ConsB a b) h = ConsB (map_arbol a h) (map_bosque b h)\"\r\n\r\ntext {*\r\n  Lema. [Ejemplo de inducci\u00f3n cruzada]\r\n  \u00b7 aplana_arbol (map_arbol a h) = map h (aplana_arbol a)\r\n  \u00b7 aplana_bosque (map_bosque b h) = map h (aplana_bosque b)\r\n*}\r\n\r\nlemma \"aplana_arbol (map_arbol a h) = map h (aplana_arbol a)\r\n     \u2227 aplana_bosque (map_bosque b h) = map h (aplana_bosque b)\"\r\nproof (induct_tac a and b)\r\n  show \"aplana_arbol (map_arbol Hoja h) = map h (aplana_arbol Hoja)\" by simp\r\nnext\r\n  fix x b\r\n  assume HI: \"aplana_bosque (map_bosque b h) = map h (aplana_bosque b)\"\r\n  have \"aplana_arbol (map_arbol (Nodo x b) h) \r\n        = aplana_arbol (Nodo (h x) (map_bosque b h))\" by simp\r\n  also have \"\u2026 = (h x)#(aplana_bosque (map_bosque b h))\" by simp\r\n  also have \"\u2026 = (h x)#(map h (aplana_bosque b))\" using HI by simp\r\n  also have \"\u2026 = map h (aplana_arbol (Nodo x b))\" by simp\r\n  finally show \"aplana_arbol (map_arbol (Nodo x b) h)\r\n                = map h (aplana_arbol (Nodo x b))\" .\r\nnext\r\n  show \"aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)\" by simp\r\nnext\r\n  fix a b\r\n  assume HI1: \"aplana_arbol (map_arbol a h) = map h (aplana_arbol a)\"\r\n     and HI2: \"aplana_bosque (map_bosque b h) = map h (aplana_bosque b)\"\r\n  have \"aplana_bosque (map_bosque (ConsB a b) h)\r\n        = aplana_bosque (ConsB (map_arbol a h) (map_bosque b h))\" by simp\r\n  also have \"\u2026 = aplana_arbol(map_arbol a h)@aplana_bosque(map_bosque b h)\" \r\n    by simp\r\n  also have \"\u2026 = (map h (aplana_arbol a))@(map h (aplana_bosque b))\" \r\n    using HI1 HI2 by simp\r\n  also have \"\u2026 = map h (aplana_bosque (ConsB a b))\" by simp\r\n  finally show \"aplana_bosque (map_bosque (ConsB a b) h) \r\n                = map h (aplana_bosque (ConsB a b))\" by simp\r\nqed\r\n\r\nlemma \"aplana_arbol (map_arbol a h) = map h (aplana_arbol a)\r\n     \u2227 aplana_bosque (map_bosque b h) = map h (aplana_bosque b)\"\r\nby (induct_tac a and b) auto\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha ampliado el estudio de las demostraciones por inducci\u00f3n en Isabelle. Se ha estudiados: c\u00f3mo a veces es necesario generalizar las propiedades para poderla demostrar por inducci\u00f3n y cuantificar universalmente las variables libres, c\u00f3mo definir funciones recursivas que no son&#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":[187],"tags":[296],"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\/1888"}],"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=1888"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1888\/revisions"}],"predecessor-version":[{"id":2854,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1888\/revisions\/2854"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1888"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1888"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1888"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}