{"id":3366,"date":"2013-05-23T16:28:25","date_gmt":"2013-05-23T16:28:25","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3366"},"modified":"2013-05-24T10:28:53","modified_gmt":"2013-05-24T10:28:53","slug":"ra2012-recursion-e-induccion-cruzada-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2012-recursion-e-induccion-cruzada-en-isabellehol\/","title":{"rendered":"RA2012: Recursi\u00f3n e inducci\u00f3n cruzada en Isabelle\/HOL"},"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\">Razonamiento autom\u00e1tico<\/a> se ha presentado c\u00f3mo definir tipos de datos mutamente recursivos y c\u00f3mo demostrar propiedades por inducci\u00f3n cruzada sobre dichos tipos.<\/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\ntheory T6\r\nimports Main\r\nbegin\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\n     and 'a bosque = Vacio | ConsB \"'a arbol\" \"'a bosque\"\r\n\r\ntext {*\r\n  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\r\ntext {* \r\n  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  Ejemplo de dempstraci\u00f3n por 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\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\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\n-- \"La demostraci\u00f3n detallada es\"\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)\" \r\n    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<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha presentado c\u00f3mo definir tipos de datos mutamente recursivos y c\u00f3mo demostrar propiedades por inducci\u00f3n cruzada sobre dichos tipos. 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\/3366"}],"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=3366"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3366\/revisions"}],"predecessor-version":[{"id":3367,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3366\/revisions\/3367"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3366"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3366"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3366"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}