{"id":6403,"date":"2018-12-13T19:34:18","date_gmt":"2018-12-13T18:34:18","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6403"},"modified":"2018-12-15T19:39:53","modified_gmt":"2018-12-15T18:39:53","slug":"ra2018-razonamiento-sobre-arboles-y-bosques-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2018-razonamiento-sobre-arboles-y-bosques-en-isabelle-hol\/","title":{"rendered":"RA2018: Razonamiento sobre \u00e1rboles y bosques 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-18\">Razonamiento autom\u00e1tico<\/a> se ha estudiado c\u00f3mo definir y razonar en Isabelle\/HOL tipos de datos recursivos como \u00e1rboles binarios, \u00e1rboles generales y bosques. En su definici\u00f3n se usa recursi\u00f3n cruzada y en la demostraci\u00f3n de sus propiedades se usa inducci\u00f3n doble.<\/p>\n<p>La teor\u00eda utilizada es la siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* Tema 5: Razonamiento sobre \u00e1rboles *}\n\ntheory T5_Razonamiento_sobre_arboles\nimports Main HOL.Parity\nbegin\n\ntext {*\n  En este tema se estudia razonamiento sobre otras estructuras\n  recursivas como \u00e1rboles binarios, \u00e1rboles generales y bosques.\n  \n  Tambi\u00e9n se muestra c\u00f3mo definir tipos de datos por recursi\u00f3n cruzada y\n  la demostraci\u00f3n de sus propiedades por inducci\u00f3n.\n*}\n\nsection {* Razonamiento sobre \u00e1rboles binarios *}\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\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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)) = \n          espejo (Nodo x (espejo d) (espejo i))\" by simp\n    also have \"\u2026 = Nodo x (espejo (espejo i)) (espejo (espejo d))\" \n      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\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\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\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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))\" \n      by simp\n    also have \"\u2026 = (rev (aplana d)) @ [x] @ (rev (aplana i))\" \n      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\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \"aplana (espejo a) = rev (aplana a)\"\nby (induct a) auto\n\nsection {* \u00c1rboles y bosques. 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 f a) es el \u00e1rbol obtenido aplicando la funci\u00f3n f a\n    todos los nodos del \u00e1rbol a.   \n  \u00b7 (map_bosque f b) es el bosque obtenido aplicando la funci\u00f3n f 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\ndeclare [[names_short]]\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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) @ \n                  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\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\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<p>En la segunda parte se coment\u00f3 el contenido de las teor\u00edas de <a href=\"https:\/\/isabelle.in.tum.de\/dist\/Isabelle2018\/doc\/main.pdf\">Main<\/a> y de <a href=\"https:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/HOL\/document.pdf\">HOL<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo definir y razonar en Isabelle\/HOL tipos de datos recursivos como \u00e1rboles binarios, \u00e1rboles generales y bosques. En su definici\u00f3n se usa recursi\u00f3n cruzada y en la demostraci\u00f3n de sus propiedades se usa inducci\u00f3n doble. La teor\u00eda utilizada&#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\/6403"}],"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=6403"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6403\/revisions"}],"predecessor-version":[{"id":6405,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6403\/revisions\/6405"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6403"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6403"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6403"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}