{"id":5657,"date":"2016-12-15T18:55:28","date_gmt":"2016-12-15T17:55:28","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5657"},"modified":"2016-12-19T18:56:53","modified_gmt":"2016-12-19T17:56:53","slug":"ra2016-verificacion-de-propiedades-de-recorridos-en-arboles-binarios-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2016-verificacion-de-propiedades-de-recorridos-en-arboles-binarios-con-isabellehol\/","title":{"rendered":"RA2016: Verificaci\u00f3n de propiedades de recorridos en \u00e1rboles binarios con Isabelle\/HOL"},"content":{"rendered":"<p>En tercera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-16\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de los ejercicios de la relaci\u00f3n 6. En dicha relaci\u00f3n se definen funciones para recorrer \u00e1rboles binarios y se demuestran con Isabelle\/HOL algunas de sus propiedades.<\/p>\n<p>Los ejercicios y sus soluciones se muestran a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* R6: Recorridos de \u00e1rboles *}\n\ntheory R6_Recorridos_de_arboles_sol\nimports Main \nbegin \n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 1. Definir el tipo de datos arbol para representar los\n  \u00e1rboles binarios que tiene informaci\u00f3n en los nodos y en las hojas. \n  Por ejemplo, el \u00e1rbol\n          e\n         \/ \\\n        \/   \\\n       c     g\n      \/ \\   \/ \\\n     a   d f   h \n  se representa por \"N e (N c (H a) (H d)) (N g (H f) (H h))\".\n  --------------------------------------------------------------------- \n*}\n\ndatatype 'a arbol = H \"'a\" | N \"'a\" \"'a arbol\" \"'a arbol\"\n\nvalue \"N e (N c (H a) (H d)) (N g (H f) (H h))\" \n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n \n     preOrden :: \"'a arbol \u21d2 'a list\"\n  tal que (preOrden a) es el recorrido pre orden del \u00e1rbol a. Por\n  ejemplo, \n     preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))\n     = [e,c,a,d,g,f,h] \n  --------------------------------------------------------------------- \n*}\n\nfun preOrden :: \"'a arbol \u21d2 'a list\" where\n  \"preOrden (H x)     = [x]\"\n| \"preOrden (N x i d) = x#(preOrden i @ preOrden d)\"\n\nvalue \"preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))\" \n-- \"= [e,c,a,d,g,f,h]\" \n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 3. Definir la funci\u00f3n \n     postOrden :: \"'a arbol \u21d2 'a list\"\n  tal que (postOrden a) es el recorrido post orden del \u00e1rbol a. Por\n  ejemplo, \n     postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))\n     = [a,d,c,f,h,g,e] \n  --------------------------------------------------------------------- \n*}\n\nfun postOrden :: \"'a arbol \u21d2 'a list\" where\n  \"postOrden (H x)     = [x]\"\n| \"postOrden (N x i d) = (postOrden i)@(postOrden d)@[x]\"\n\nvalue \"postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))\" \n-- \"[a,d,c,f,h,g,e]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 4. Definir la funci\u00f3n \n     inOrden :: \"'a arbol \u21d2 'a list\"\n  tal que (inOrden a) es el recorrido in orden del \u00e1rbol a. Por\n  ejemplo, \n     inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))\n     = [a,c,d,e,f,g,h]\n  --------------------------------------------------------------------- \n*}\n\nfun inOrden :: \"'a arbol \u21d2 'a list\" where\n  \"inOrden (H x)     = [x]\"\n| \"inOrden (N x i d) = (inOrden i)@[x]@(inOrden d)\"\n\nvalue \"inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))\" \n-- \"[a,c,d,e,f,g,h]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 5. Definir la funci\u00f3n \n     espejo :: \"'a arbol \u21d2 'a arbol\"\n  tal que (espejo a) es la imagen especular del \u00e1rbol a. Por ejemplo, \n     espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))\n     = N e (N g (H h) (H f)) (N c (H d) (H a))\n  --------------------------------------------------------------------- \n*}\n\nfun espejo :: \"'a arbol \u21d2 'a arbol\" where\n  \"espejo (H x)     = (H x)\"\n| \"espejo (N x i d) = N x (espejo d) (espejo i)\"\n\nvalue \"espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))\" \n-- \"N e (N g (H h) (H f)) (N c (H d) (H a))\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 6. Demostrar que\n     preOrden (espejo a) = rev (postOrden a)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma  \"preOrden (espejo a) = rev (postOrden a)\"\nby (induct a) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma  \"preOrden (espejo a) = rev (postOrden a)\" (is \"?P a\")\nproof (induct a)\n  fix x\n  show \"?P (H x)\" by simp\nnext\n  fix x i d\n  assume HI1: \"?P i\"\n  assume HI2: \"?P d\"\n  show \"?P (N x i d)\"\n  proof -\n    have \"preOrden (espejo (N x i d)) = \n          preOrden (N x (espejo d) (espejo i))\" by simp\n    also have \"\u2026 = x # (preOrden (espejo d) @ preOrden (espejo i))\" by simp\n    also have \"\u2026 = x # (rev (postOrden d) @ rev (postOrden i))\" \n       using HI1 HI2 by simp \n    also have \"\u2026 = x # rev (postOrden i @ postOrden d)\" by simp\n    also have \"\u2026 = rev ((postOrden i) @ (postOrden d) @ [x])\" by simp\n    also have \"\u2026 = rev (postOrden (N x i d))\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 7. Demostrar que\n     postOrden (espejo a) = rev (preOrden a)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"postOrden (espejo a) = rev (preOrden a)\"\nby (induct a) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"postOrden (espejo a) = rev (preOrden a)\" (is \"?P a\")\nproof (induct a)\n  fix x\n  show \"?P (H x)\" by simp\nnext\n  fix x i d\n  assume HI1: \"?P i\"\n  assume HI2: \"?P d\"\n  show \"?P (N x i d)\"\n  proof -\n    have \"postOrden (espejo (N x i d)) = \n          postOrden (N x (espejo d) (espejo i))\" by simp\n    also have \"\u2026 = postOrden (espejo d) @ postOrden (espejo i) @ [x]\" by simp\n    also have \"\u2026 = rev (preOrden d) @ rev (preOrden i) @ [x]\" \n       using HI1 HI2 by simp\n    also have \"\u2026 = rev (preOrden i @ preOrden d) @ [x]\" by simp\n    also have \"\u2026 = rev ([x] @ preOrden i @ preOrden d)\" by simp\n    also have \"\u2026 = rev (preOrden (N x i d))\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 8. Demostrar que\n     inOrden (espejo a) = rev (inOrden a)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\ntheorem \"inOrden (espejo a) = rev (inOrden a)\"\nby (induct a) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\ntheorem \"inOrden (espejo a) = rev (inOrden a)\" (is \"?P a\")\nproof (induct a)\n  fix x\n  show \"?P (H x)\" by simp\nnext\n  fix x i d\n  assume HI1: \"?P i\"\n  assume HI2: \"?P d\"\n  show \"?P (N x i d)\"\n  proof -\n    have \"inOrden (espejo (N x i d)) = \n          inOrden (N x (espejo d) (espejo i))\" by simp\n    also have \"\u2026 = inOrden (espejo d) @ [x] @ inOrden (espejo i)\" by simp\n    also have \"\u2026 = rev (inOrden d) @ [x] @ rev (inOrden i)\" \n       using HI1 HI2 by simp\n    also have \"\u2026 = rev (inOrden i @ [x] @ inOrden d)\" by simp\n    also have \"\u2026 = rev (inOrden (N x i d))\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 9. Definir la funci\u00f3n \n     raiz :: \"'a arbol \u21d2 'a\"\n  tal que (raiz a) es la raiz del \u00e1rbol a. Por ejemplo, \n     raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e\n  --------------------------------------------------------------------- \n*}\n\nfun raiz :: \"'a arbol \u21d2 'a\" where\n  \"raiz (H x)     = x\"\n| \"raiz (N x i d) = x\"\n\nvalue \"raiz (N e (N c (H a) (H d)) (N g (H f) (H h)))\" -- \"= e\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 10. Definir la funci\u00f3n \n     extremo_izquierda :: \"'a arbol \u21d2 'a\"\n  tal que (extremo_izquierda a) es el nodo m\u00e1s a la izquierda del \u00e1rbol\n  a. Por ejemplo,  \n     extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a\n  --------------------------------------------------------------------- \n*}\n\nfun extremo_izquierda :: \"'a arbol \u21d2 'a\" where\n  \"extremo_izquierda (H x)      = x\"\n| \"extremo_izquierda (N x i d) = extremo_izquierda i\"\n\nvalue \"extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h)))\" -- \"= a\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 11. Definir la funci\u00f3n \n     extremo_derecha :: \"'a arbol \u21d2 'a\"\n  tal que (extremo_derecha a) es el nodo m\u00e1s a la derecha del \u00e1rbol\n  a. Por ejemplo,  \n     extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h\n  --------------------------------------------------------------------- \n*}\n\nfun extremo_derecha :: \"'a arbol \u21d2 'a\" where\n  \"extremo_derecha (H x)     = x\"\n| \"extremo_derecha (N x i d) = extremo_derecha d\"\n\nvalue \"extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h)))\" -- \"= h\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 12. Demostrar o refutar\n     last (inOrden a) = extremo_derecha a\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica, basada en un lema, es\"\nlemma inOrdenNoVacio: \"inOrden a \u2260 []\"\nby (induct a) auto\n\ntheorem \"last (inOrden a) = extremo_derecha a\"\nby (induct a) (auto simp add: inOrdenNoVacio)\n\n-- \"La demostraci\u00f3n estructurada es\"\ntheorem \"last (inOrden a) = extremo_derecha a\" (is \"?P a\")\nproof (induct a)\n  fix x\n  show \"?P (H x)\" by simp\nnext\n  fix x i d\n  assume HI: \"?P d\"\n  show \"?P (N x i d)\"\n  proof -  \n    have \"last (inOrden (N x i d)) = \n          last (inOrden d @ [x] @ inOrden d)\" by simp\n    also have \"\u2026 = last (inOrden d)\"  by (simp add: inOrdenNoVacio)\n    also have \"\u2026 = extremo_derecha d\" using HI by simp\n    also have \"\u2026 =  extremo_derecha (N x i d)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 13. Demostrar o refutar\n     hd (inOrden a) = extremo_izquierda a\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\ntheorem \"hd (inOrden a) = extremo_izquierda a\"\nby (induct a) (auto simp add: inOrdenNoVacio)\n\n-- \"La demostraci\u00f3n estructurada es\"\ntheorem \"hd (inOrden a) = extremo_izquierda a\" (is \"?P a\")\nproof (induct a)\n  fix x\n  show \"?P (H x)\" by simp\nnext\n  fix x i d\n  assume HI: \"?P i\"\n  show \"?P (N x i d)\"\n  proof - \n    have \"hd (inOrden (N x i d)) = \n          hd (inOrden i @ [x] @ inOrden d)\" by simp\n    also have \"\u2026 = hd (inOrden i)\"  by (simp add: inOrdenNoVacio)\n    also have \"\u2026 = extremo_izquierda i\" using HI by simp\n    also have \"\u2026 = extremo_izquierda (N x i d)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 14. Demostrar o refutar\n     hd (preOrden a) = last (postOrden a)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\ntheorem \"hd (preOrden a) = last (postOrden a)\"\nby (cases a) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\ntheorem \"hd (preOrden a) = last (postOrden a)\"(is \"?P a\")\nproof (cases a)\n  fix x\n  assume \"a = H x\"\n  then show \"?P a\" by simp\nnext\n  fix x i d\n  assume H: \"a = N x i d\"\n  show \"?P a\"\n  proof - \n    have \"hd (preOrden a) = hd (preOrden (N x i d))\" using H by simp\n    also have \"\u2026 = hd (x # (preOrden i @ preOrden d))\" by simp\n    also have \"\u2026 = x\" by simp\n    also have \"\u2026 = last (postOrden i @ postOrden d @ [x])\" by simp\n    also have \"\u2026 = last (postOrden (N x i d))\" by simp\n    also have \"\u2026 = last (postOrden a)\" using H by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 15. Demostrar o refutar\n     hd (preOrden a) = raiz a\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\ntheorem \"hd (preOrden a) = raiz a\"\nby (cases a) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\ntheorem \"hd (preOrden a) = raiz a\" (is \"?P a\")\nproof (cases a)\n  fix x\n  assume \"a = H x\"\n  then show \"?P a\" by simp\nnext\n  fix x i d\n  assume H: \"a = N x i d\"\n  show \"?P a\"\n  proof -\n    have \"hd (preOrden a) = hd (preOrden (N x i d))\" using H by simp\n    also have \"\u2026 = hd (x#(preOrden i @ preOrden d))\" by simp\n    also have \"\u2026 = x\" by simp\n    also have \"\u2026 = raiz (N x i d)\" by simp\n    also have \"\u2026 = raiz a\" using H by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 16. Demostrar o refutar\n     hd (inOrden a) = raiz a\n  --------------------------------------------------------------------- \n*}\n\ntheorem \"hd (inOrden a) = raiz a\"\nquickcheck\noops\n\ntext {*\n  Quickcheck found a counterexample:\n  a = N a1 (H a2) (H a1)\n  \n  Evaluated terms:\n  hd (inOrden a) = a2\n  raiz a = a1\n*}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 17. Demostrar o refutar\n     last (postOrden a) = raiz a\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\ntheorem \"last (postOrden a) = raiz a\"\nby (cases a) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\ntheorem \"last (postOrden a) = raiz a\" (is \"?P a\")\nproof (cases a)\n  fix x\n  assume \"a = H x\"\n  then show \"?P a\" by simp\nnext\n  fix x i d\n  assume H: \"a = N x i d\"\n  show \"?P a\"\n  proof -\n    have \"last (postOrden a) = last (postOrden (N x i d))\" using H by simp\n    also have \"\u2026 = last (postOrden i @ preOrden d @ [x])\" by simp\n    also have \"\u2026 = x\" by simp\n    also have \"\u2026 = raiz a\" using H by simp\n    finally show ?thesis .\n  qed\nqed\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En tercera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se han comentado las soluciones de los ejercicios de la relaci\u00f3n 6. En dicha relaci\u00f3n se definen funciones para recorrer \u00e1rboles binarios y se demuestran con Isabelle\/HOL algunas de sus propiedades. Los ejercicios y sus soluciones se muestran a continuaci\u00f3n<\/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":[261],"tags":[144,314],"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\/5657"}],"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=5657"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5657\/revisions"}],"predecessor-version":[{"id":5659,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5657\/revisions\/5659"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5657"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5657"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5657"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}