{"id":4609,"date":"2014-11-20T20:24:45","date_gmt":"2014-11-20T19:24:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4609"},"modified":"2014-11-21T20:25:52","modified_gmt":"2014-11-21T19:25:52","slug":"ra2014-ejercicios-de-razonamiento-sobre-cons-inverso-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2014-ejercicios-de-razonamiento-sobre-cons-inverso-en-isabellehol\/","title":{"rendered":"RA2014: Ejercicios de razonamiento sobre cons inverso en Isabelle\/HOL"},"content":{"rendered":"

En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de los ejercicios de la relaci\u00f3n 4 sobre funci\u00f3n snoc (cons inverso) que a\u00f1ade un elemento al final. Lo interesante es el uso de algunas propiedades en la demostraci\u00f3n de otras (como en el ejercicio 5). Las ejercicios y sus soluciones son
\n<\/p>\n

\nheader {* R4: Cons inverso *}\n\ntheory R4\nimports Main \nbegin\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 1. Definir recursivamente la funci\u00f3n \n     snoc :: \"'a list \u21d2 'a \u21d2 'a list\"\n  tal que (snoc xs a) es la lista obtenida al a\u00f1adir el elemento a al\n  final de la lista xs. Por ejemplo, \n     value \"snoc [2,5] (3::int)\" == [2,5,3]\n\n  Nota: No usar @.\n  --------------------------------------------------------------------- \n*}\n\nfun snoc :: \"'a list \u21d2 'a \u21d2 'a list\" where\n  \"snoc [] a = [a]\"\n| \"snoc (x#xs) a = x # (snoc xs a)\"\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 2. Demostrar autom\u00e1ticamente el siguiente teorema \n     snoc xs a = xs @ [a]\n  --------------------------------------------------------------------- \n*}\n\nlemma \"snoc xs a = xs @ [a]\"\nby (induct xs) auto\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 3. Demostrar detalladamente el siguiente teorema \n     snoc xs a = xs @ [a]\n  --------------------------------------------------------------------- \n*}\n\nlemma snoc_append: \"snoc xs a = xs @ [a]\"\nproof (induct \"xs\") \n  show \"snoc [] a = [] @ [a]\"\n  proof -\n    have \"snoc [] a = [a]\" by simp\n    also have \"\u2026 = [] @ [a]\" by simp\n    finally show \"snoc [] a = [] @ [a]\" .\n  qed\nnext\n  fix b xs assume HI: \"snoc xs a = xs @ [a]\"\n  show \"snoc (b # xs) a = (b # xs) @ [a]\"\n  proof -\n    have \"snoc (b # xs) a = b # (snoc xs a)\" by simp\n    also have \"\u2026 = b # (xs @ [a])\" using HI by simp\n    also have \"\u2026 = (b # xs) @ [a]\" by simp\n    finally show \"snoc (b # xs) a = (b # xs) @ [a]\" .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 4. Demostrar autom\u00e1ticamente el siguiente lema\n     rev (x # xs) = snoc (rev xs) x\"\n  --------------------------------------------------------------------- \n*}\n\nlemma \"rev (x # xs) = snoc (rev xs) x\"\nby (auto simp add: snoc_append)\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 5. Demostrar detalladamente el siguiente lema\n     rev (x # xs) = snoc (rev xs) x\"\n  --------------------------------------------------------------------- \n*}\n\ntheorem \"rev (x # xs) = snoc (rev xs) x\"\nproof -\n  have \"rev (x # xs) = (rev xs) @ [x]\" by simp\n  also have \"\u2026 = snoc (rev xs) x\" by (simp add:snoc_append)\n  finally show \"rev (x # xs) = snoc (rev xs) x\" .\nqed\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se han comentado las soluciones de los ejercicios de la relaci\u00f3n 4 sobre funci\u00f3n snoc (cons inverso) que a\u00f1ade un elemento al final. Lo interesante es el uso de algunas propiedades en la demostraci\u00f3n de otras (como en el ejercicio 5)….<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[240],"tags":[144,307],"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\/4609"}],"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=4609"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4609\/revisions"}],"predecessor-version":[{"id":4610,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4609\/revisions\/4610"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4609"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4609"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4609"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}