{"id":7175,"date":"2020-05-14T12:40:58","date_gmt":"2020-05-14T10:40:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7175"},"modified":"2020-05-14T12:40:58","modified_gmt":"2020-05-14T10:40:58","slug":"lmf2019-razonamiento-sobre-arboles-y-bosques-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2019-razonamiento-sobre-arboles-y-bosques-en-isabelle-hol\/","title":{"rendered":"LMF2019: Razonamiento sobre \u00e1rboles y bosques en Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\">L\u00f3gica matem\u00e1tica y fundamentos<\/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 clase se ha dado mediante videoconferencia y los v\u00eddeos correspondientes son:<\/p>\n<ul>\n<li>Primera parte: Razonamiento sobre \u00e1rboles binarios<\/li>\n<\/ul>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/0ZiCWOIgMMc\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<ul>\n<li>Segunda parte: \u00c1rboles y bosques: Recursi\u00f3n mutua e inducci\u00f3n<\/li>\n<\/ul>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/uytQp1w2Y8I\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>La teor\u00eda utilizada es la siguiente<br \/>\n<!- more --><\/p>\n<pre lang=\"isabelle\">\nchapter \u2039Tema 8: Razonamiento sobre \u00e1rboles\u203a\n\ntheory T8_Razonamiento_sobre_arboles\nimports Main \nbegin\n\ntext \u2039En 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.\u203a\n\nsection \u2039Razonamiento sobre \u00e1rboles binarios\u203a\n\ntext \u2039Ejemplo de definici\u00f3n de tipos recursivos:\n  Definir un tipo de dato para los \u00e1rboles binarios.\u203a\n\ndatatype 'a arbolB = Hoja \"'a\" \n                   | Nodo \"'a\" \"'a arbolB\" \"'a arbolB\"\n\ntext \u2039Regla de inducci\u00f3n correspondiente a los \u00e1rboles binarios:\n  La regla de inducci\u00f3n sobre \u00e1rboles binarios es arbolB.induct:\n  \u27e6 \u22c0x. P (Hoja x);\n    \u22c0x i d. \u27e6P i; P d\u27e7 \u27f9 P (Nodo x i d)\u27e7 \n  \u27f9 P a\n\u203a\n\nthm arbolB.induct\n\ntext \u2039Ejemplo de definici\u00f3n sobre \u00e1rboles binarios:\n  Definir la funci\u00f3n \"espejo\" que aplicada a un \u00e1rbol devuelve su imagen\n  especular.\u203a\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 \u2039Ejemplo 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.\u203a\n\n\u2015 \u2039La demostraci\u00f3n declarativa es\u203a\nlemma \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)\"  \n    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))\" \n      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\" \n      using h1 h2 by simp \n    finally show \"?P (Nodo x i d)\" \n      by this\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n declarativa detallada es\u203a\nlemma \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)\"  \n    by (simp only: espejo.simps(1)) \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))\" \n      by (simp only: espejo.simps(2))\n    also have \"\u2026 = Nodo x (espejo (espejo i)) (espejo (espejo d))\" \n      by (simp only: espejo.simps(2))\n    also have \"\u2026 = Nodo x i d\" \n      using h1 h2\n      by (simp only:) \n    finally show ?thesis \n      by this\n  qed\nqed\n\ntext \u2039Comentarios 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\u203a\n\n\u2015 \u2039La demostraci\u00f3n aplicativa es\u203a\nlemma  \n  \"espejo (espejo a) = a\"\n  apply (induct a)\n   apply simp\n  apply simp\n  done\n\n\u2015 \u2039La demostraci\u00f3n aplicativa detallada es\u203a\nlemma  \n  \"espejo (espejo a) = a\"\n  apply (induct a)\n   apply (simp only: espejo.simps(1))\n  apply (simp only: espejo.simps(2))\n  done\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma  \n  \"espejo (espejo a) = a\"\n  by (induct a) simp+ \n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica detallada es\u203a\nlemma  \n  \"espejo (espejo a) = a\"\n  by (induct a) (simp only: espejo.simps)+  \n\ntext \u2039Ejemplo. [Aplanamiento de \u00e1rboles]\n  Definir la funci\u00f3n \"aplana\" que aplane los \u00e1rboles recorri\u00e9ndolos en\n  orden infijo.\u203a\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 \u2039Ejemplo. [Aplanamiento de la imagen especular] Demostrar que\n     aplana (espejo a) = rev (aplana a)\u203a\n\n\u2015 \u2039La demostraci\u00f3n declarativa 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)\" \n    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))\" \n      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))\" \n      by simp\n    also have \"\u2026 = rev (aplana (Nodo x i d))\" \n      by simp\n    finally show \"?P (Nodo x i d)\" \n      by this\n  qed\nqed\n\n\u2015 \u2039Lema auxiliar para la demostraci\u00f3n declarativa detallada\u203a\nlemma rev_unit: \"rev [x] = [x]\"\nproof -\n  have \"rev [x] = rev [] @ [x]\" \n    by (simp only: rev.simps(2))\n  also have \"\u2026 = [] @ [x]\"\n    by (simp only: rev.simps(1))\n  also have \"\u2026 = [x]\"\n    by (simp only: append.simps(1))\n  finally show ?thesis\n    by this\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada y detallada 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 :: 'b\n  have \"aplana (espejo (Hoja x)) = aplana (Hoja x)\"\n    by (simp only: espejo.simps(1))\n  also have \"\u2026 = [x]\"\n    by (simp only: aplana.simps(1))\n  also have \"\u2026 = rev [x]\"\n    by (simp only: rev_unit)\n  also have \"\u2026 = rev (aplana (Hoja x))\"\n    by (simp only: aplana.simps(1))\n  finally show \"?P (Hoja x)\" \n    by this \nnext\n  fix x :: 'b\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))\" \n      by (simp only: espejo.simps(2))\n    also have \"\u2026 = (aplana (espejo d)) @ [x] @ (aplana (espejo i))\" \n      by (simp only: aplana.simps(2))\n    also have \"\u2026 = (rev (aplana d)) @ [x] @ (rev (aplana i))\" \n      by (simp only: h1 h2)\n    also have \"\u2026 = rev ((aplana i) @ [x] @ (aplana d))\"\n      (* find_theorems \"rev (_ @ _)\" *)\n      by (simp only: rev_append rev_unit append_assoc)\n    also have \"\u2026 = rev (aplana (Nodo x i d))\" \n      by (simp only: aplana.simps(2))\n    finally show ?thesis \n      by this\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n aplicativa es\u203a\nlemma \"aplana (espejo a) = rev (aplana a)\"\n  apply (induct a)\n   apply simp\n  apply simp\n  done\n\n\u2015 \u2039La demostraci\u00f3n aplicativa detallada es\u203a\nlemma \"aplana (espejo a) = rev (aplana a)\"\n  apply (induct a)\n   apply (simp only: espejo.simps(1) aplana.simps(1))\n   apply (simp only: rev_unit)\n  apply (simp only: espejo.simps(2) aplana.simps(2))\n  apply (simp only: rev_append)\n  apply (simp only: rev_unit)\n  apply (simp only: append_assoc)\n  done\n\n\u2015 \u2039La demostraci\u00f3n aplicativa detallada compacta es\u203a\nlemma \"aplana (espejo a) = rev (aplana a)\"\n  apply (induct a)\n   apply (simp only: \n      espejo.simps(1) \n      aplana.simps(1)\n      rev_unit\n      espejo.simps(2) \n      aplana.simps(2)\n      rev_append\n      append_assoc)+\n  done\n\n\u2015 \u2039La demostraci\u00f3n aplicativa detallada m\u00e1s compacta es\u203a\nlemma \"aplana (espejo a) = rev (aplana a)\"\n  apply (induct a)\n   apply (simp only: \n      espejo.simps\n      aplana.simps\n      rev_unit\n      rev_append\n      append_assoc)+\n  done\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \"aplana (espejo a) = rev (aplana a)\"\n  by (induct a) simp_all\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica detallada es\u203a\nlemma \"aplana (espejo a) = rev (aplana a)\"\n  by (induct a)\n     (simp only: \n      espejo.simps\n      aplana.simps\n      rev_unit\n      rev_append\n      append_assoc)+\n\nsection \u2039\u00c1rboles y bosques. Recursi\u00f3n mutua e inducci\u00f3n\u203a\n\ntext \u2039Nota. [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.\u203a\n\ndatatype 'a arbol = Nodo \"'a\" \"'a bosque\"\n     and 'a bosque = Vacio | ConsB \"'a arbol\" \"'a bosque\"\n\ntext \u2039Regla de inducci\u00f3n correspondiente a la recursi\u00f3n cruzada:\n  La regla de inducci\u00f3n sobre \u00e1rboles y bosques es arbol_bosque.induct:\n     \u27e6\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\u203a\n\nthm arbol_bosque.induct\n\ntext \u2039Ejemplos 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. \u203a\n\nfun aplana_arbol :: \"'a arbol \u21d2 'a list\" and \n    aplana_bosque :: \"'a bosque \u21d2 'a list\" where\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 (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 \u2039Ejemplo 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)\u203a\n\ndeclare [[names_short]] \n\n\u2015 \u2039La demostraci\u00f3n declarativa 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  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))\" \n    by simp\n  also have \"\u2026 = (f x) # (aplana_bosque (map_bosque f b))\" \n    by simp\n  also have \"\u2026 = (f x) # (map f (aplana_bosque b))\" \n    using HI by simp\n  also have \"\u2026 = map f (aplana_arbol (Nodo x b))\" \n    by simp\n  finally show \"aplana_arbol (map_arbol f (Nodo x b)) =\n                map f (aplana_arbol (Nodo x b))\" \n    by this\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))\" \n    by this\nqed\n\n\u2015 \u2039La demostraci\u00f3n declarativa 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  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))\" \n    by (simp only: map_arbol.simps(1))\n  also have \"\u2026 = (f x) # (aplana_bosque (map_bosque f b))\" \n    by (simp only: aplana_arbol.simps(1))\n  also have \"\u2026 = (f x) # (map f (aplana_bosque b))\"\n    using HI\n    by (simp only:)\n  also have \"\u2026 = map f (aplana_arbol (Nodo x b))\" \n    (* find_theorems \"map _ (_ # _)\" *)\n    by (simp only: list.map aplana_arbol.simps(1))\n  finally show \"aplana_arbol (map_arbol f (Nodo x b)) =\n                map f (aplana_arbol (Nodo x b))\" \n    by this\nnext\n  show \"aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)\" \n    by (simp only: aplana_bosque.simps(1)\n                   map_bosque.simps(1)\n                   list.map)\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))\" \n    by (simp only: map_bosque.simps(2))\n  also have \"\u2026 = aplana_arbol (map_arbol f a) @ \n                  aplana_bosque (map_bosque f b)\" \n    by (simp only: aplana_bosque.simps(2))\n  also have \"\u2026 = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))\" \n    by (simp only: HI1 HI2)\n  also have \"\u2026 = map f (aplana_arbol a @ aplana_bosque b)\"\n    (* find_theorems \"map _ (_ @ _)\" *)\n    by (simp only: map_append)\n  also have \"\u2026 = map f (aplana_bosque (ConsB a b))\" \n    by (simp only: aplana_bosque.simps(2))\n  finally show \"aplana_bosque (map_bosque f (ConsB a b)) =\n                map f (aplana_bosque (ConsB a b))\" \n    by this\nqed\n\ntext \u2039Comentarios 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 3 casos:\n    1. \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    2. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)\n    3. \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))\u203a\n\n\u2015 \u2039La demostraci\u00f3n aplicativa 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)\"\n  apply (induct_tac a and b)\n    apply simp+\n  done\n\n\u2015 \u2039La demostraci\u00f3n aplicativa 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)\"\n  apply (induct_tac a and b)\n    apply (simp only: map_arbol.simps aplana_arbol.simps)\n    apply (simp only: list.map(2))\n   apply (simp only: map_bosque.simps(1) aplana_bosque.simps(1))\n   apply (simp only: list.map(1))\n  apply (simp only: map_bosque.simps(2) aplana_bosque.simps(2))\n  apply (simp only: map_append)\n  done\n\n\u2015 \u2039La demostraci\u00f3n aplicativa detallada compacta 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)\"\n  apply (induct_tac a and b)\n    apply (simp only: \n      map_arbol.simps \n      aplana_arbol.simps\n      list.map(2)\n      map_bosque.simps(1) \n      aplana_bosque.simps(1)\n      list.map(1)\n      map_bosque.simps(2) \n      aplana_bosque.simps(2)\n      map_append)+\n  done\n\n\u2015 \u2039La demostraci\u00f3n aplicativa detallada m\u00e1s compacta 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)\"\n  apply (induct_tac a and b)\n    apply (simp only: \n      map_arbol.simps \n      map_bosque.simps\n      aplana_arbol.simps\n      aplana_bosque.simps\n      list.map\n      map_append)+\n  done\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)\"\n  by (induct_tac a and b) simp+\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica 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)\"\n  by (induct_tac a and b) \n     (simp only: \n      map_arbol.simps \n      map_bosque.simps\n      aplana_arbol.simps\n      aplana_bosque.simps\n      list.map\n      map_append)+\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos 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 clase se ha dado&#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":[334],"tags":[],"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\/7175"}],"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=7175"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7175\/revisions"}],"predecessor-version":[{"id":7176,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7175\/revisions\/7176"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7175"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7175"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7175"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}