{"id":3307,"date":"2013-05-02T19:49:21","date_gmt":"2013-05-02T19:49:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3307"},"modified":"2013-05-05T09:50:06","modified_gmt":"2013-05-05T09:50:06","slug":"ra2012-verificacion-de-propiedades-de-la-sustitucion-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2012-verificacion-de-propiedades-de-la-sustitucion-en-isabellehol\/","title":{"rendered":"RA2012: Verificaci\u00f3n de propiedades de la sustituci\u00f3n en Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a> se ha resuelto de manera colaborativa ejercicios sobre la demostraci\u00f3n de propiedades de la funci\u00f3n de sustituci\u00f3n con Isabelle\/HOL. Su objetivo es ilustrar el uso del razonamiento por inducci\u00f3n y por casos en Isabelle. Para ca propiedad se presentan distintas demostraciones desde las autom\u00e1ticas a las detalladas. <\/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 R11\r\nimports Main \r\nbegin\r\n\r\ntext {* \r\n  --------------------------------------------------------------------- \r\n  Ejercicio 1. Definir la funci\u00f3n \r\n     sust :: \"'a \u21d2 'a \u21d2 'a list \u21d2 'a list\"\r\n  tal que (sust x y zs) es la lista obtenida sustituyendo cada\r\n  occurrencia de x por y en la lista zs. Por ejemplo,\r\n     sust (1::nat) 2 [1,2,3,4,1,2,3,4] = [2,2,3,4,2,2,3,4]\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\nfun sust :: \"'a \u21d2 'a \u21d2 'a list \u21d2 'a list\" where\r\n  \"sust x y [] = []\"\r\n| \"sust x y (z#zs) = (if z=x then y else z)#(sust x y zs)\"\r\n\r\nvalue \"sust (1::nat) 2 [1,2,3,4,1,2,3,4]\" -- \"= [2,2,3,4,2,2,3,4]\"\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 2. Demostrar o refutar: \r\n     sust x y (xs@ys) = (sust x y xs)@(sust x y ys)\"\r\n  ---------------------------------------------------------------------  \r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma sust_append: \r\n  \"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)\"\r\nby (induct xs) auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma sust_append_2: \r\n  \"sust x y (xs @ ys) = (sust x y xs)@(sust x y ys)\"\r\nproof (induct xs)\r\n  show \"sust x y ([]@ys) = (sust x y [])@(sust x y ys)\" by simp\r\nnext\r\n  fix a xs \r\n  assume HI: \"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)\"\r\n  show \"sust x y ((a#xs)@ys) = (sust x y (a#xs))@(sust x y ys)\"\r\n  proof (cases)\r\n    assume \"x=a\"\r\n    thus \"sust x y ((a#xs)@ys) = (sust x y (a#xs))@(sust x y ys)\" \r\n      using HI by auto\r\n  next\r\n    assume \"x\u2260a\"\r\n    thus \"sust x y ((a#xs)@ys) = (sust x y (a#xs))@(sust x y ys)\"\r\n      using HI by auto\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma sust_append_3: \r\n  \"sust x y (xs @ ys) = (sust x y xs)@(sust x y ys)\"\r\nproof (induct xs)\r\n  show \"sust x y ([]@ys) = (sust x y [])@(sust x y ys)\" by simp\r\nnext\r\n  fix a xs \r\n  assume HI: \"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)\"\r\n  show \"sust x y ((a#xs)@ys) = (sust x y (a#xs))@(sust x y ys)\"\r\n  proof (cases)\r\n    assume \"x=a\"\r\n    hence \"sust x y ((a#xs)@ys) = sust x y (a#(xs@ys))\" by simp\r\n    also have \"\u2026 = y#(sust x y (xs@ys))\" using `x=a` by simp\r\n    also have \"\u2026 = y#((sust x y xs)@(sust x y ys))\" using HI by simp\r\n    also have \"\u2026 = (y#(sust x y xs))@(sust x y ys)\" by simp\r\n    also have \"\u2026 = (sust x y (a#xs))@(sust x y ys)\" using `x=a` by simp\r\n    finally show \"sust x y ((a#xs)@ys) = (sust x y (a#xs))@(sust x y ys)\" .\r\n  next\r\n    assume \"x\u2260a\"\r\n    hence \"sust x y ((a#xs)@ys) = sust x y (a#(xs@ys))\" by simp\r\n    also have \"\u2026 = a#(sust x y (xs@ys))\" using `x\u2260a` by simp\r\n    also have \"\u2026 = a#((sust x y xs)@(sust x y ys))\" using HI by simp\r\n    also have \"\u2026 = (a#(sust x y xs))@(sust x y ys)\" by simp\r\n    also have \"\u2026 = (sust x y (a#xs))@(sust x y ys)\" using `x\u2260a` by simp\r\n    finally show \"sust x y ((a#xs)@ys) = (sust x y (a#xs))@(sust x y ys)\" .\r\n  qed\r\nqed\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 3. Demostrar o refutar: \r\n     rev (sust x y zs) = sust x y (rev zs)\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma rev_sust: \r\n  \"rev(sust x y zs) = sust x y (rev zs)\"\r\nby (induct zs) (simp_all add: sust_append)\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma rev_sust_2: \r\n  \"rev (sust x y zs) = sust x y (rev zs)\"\r\nproof (induct zs)\r\n  show \"rev (sust x y []) = sust x y (rev [])\" by simp\r\nnext\r\n  fix a zs \r\n  assume HI: \"rev (sust x y zs) = sust x y (rev zs)\"\r\n  show \"rev (sust x y (a#zs)) = sust x y (rev (a#zs))\"\r\n    using HI by (auto simp add: sust_append)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma rev_sust_3: \r\n  \"rev (sust x y zs) = sust x y (rev zs)\"\r\nproof (induct zs)\r\n  show \"rev (sust x y []) = sust x y (rev [])\" by simp\r\nnext\r\n  fix a zs \r\n  assume HI: \"rev (sust x y zs) = sust x y (rev zs)\"\r\n  show \"rev (sust x y (a#zs)) = sust x y (rev (a#zs))\"\r\n  proof -\r\n    have \"rev (sust x y (a#zs)) = rev ((if x=a then y else a)#(sust x y zs))\"\r\n      by simp\r\n    also have \"\u2026 = (rev (sust x y zs))@[if x=a then y else a]\" by simp\r\n    also have \"\u2026 = (sust x y (rev zs))@[if x=a then y else a]\" using HI by simp\r\n    also have \"\u2026 = (sust x y (rev zs))@(sust x y [a])\" by simp\r\n    also have \"\u2026 = sust x y ((rev zs)@[a])\" by (simp add: sust_append)\r\n    also have \"\u2026 = sust x y (rev (a#zs))\" by simp\r\n    finally show \"rev (sust x y (a#zs)) = sust x y (rev (a#zs))\" .\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es con casos es\"\r\nlemma rev_sust_4: \r\n  \"rev (sust x y zs) = sust x y (rev zs)\"\r\nproof (induct zs)\r\n  show \"rev (sust x y []) = sust x y (rev [])\" by simp\r\nnext\r\n  fix a zs \r\n  assume HI: \"rev (sust x y zs) = sust x y (rev zs)\"\r\n  show \"rev (sust x y (a#zs)) = sust x y (rev (a#zs))\"\r\n  proof (cases \"x=a\")\r\n    assume \"x=a\"\r\n    hence \"rev (sust x y (a#zs)) = rev (y # (sust x y zs))\" by simp\r\n    also have \"... = (rev (sust x y zs)) @ [y]\" by simp\r\n    also have \"... = (sust x y (rev zs)) @ [y]\" using HI by simp\r\n    also have \"... = (sust x y (rev zs)) @ (sust x y [a])\"\r\n      using `x=a` by simp\r\n    also have \"... = sust x y ((rev zs) @ [a])\" \r\n      by (simp add: sust_append)\r\n    also have \"... = sust x y (rev (a#zs))\" by simp\r\n    finally show \"rev (sust x y (a#zs)) = sust x y (rev (a#zs))\"\r\n      by simp\r\n  next\r\n    assume \"x\u2260a\"\r\n    hence \"rev (sust x y (a#zs)) = rev (a # (sust x y zs))\" by simp\r\n    also have \"... = (rev (sust x y zs)) @ [a]\" by simp\r\n    also have \"... = (sust x y (rev zs)) @ [a]\" using HI by simp\r\n    also have \"... = (sust x y (rev zs)) @ (sust x y [a])\"\r\n      using `x\u2260a` by simp\r\n    also have \"... = sust x y ((rev zs) @ [a])\" \r\n      by (simp add: sust_append)\r\n    also have \"... = sust x y (rev (a#zs))\" by simp\r\n    finally show \"rev (sust x y (a#zs)) = sust x y (rev (a#zs))\"\r\n      by simp\r\n  qed\r\nqed\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 4. Demostrar o refutar:\r\n     sust x y (sust u v zs) = sust u v (sust x y zs)\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\nlemma \"sust x y (sust u v zs) = sust u v (sust x y zs)\"\r\nquickcheck\r\noops\r\n\r\ntext {*\r\n  El contraejemplo encontrado es:\r\n   u = -1\r\n   v = 0\r\n   x = -1\r\n   y = 1\r\n   zs = [-1]  \r\n  Efectivamente,\r\n   sust (-1) 1 (sust (-1) 0 [(-1)]) = [0]\r\n   sust (-1) 0 (sust (-1) 1 [(-1)]) = [1]\r\n*}\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 5. Demostrar o refutar:\r\n     sust y z (sust x y zs) = sust x z zs\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\nlemma \"sust y z (sust x y zs) = sust x z zs\"\r\nquickcheck\r\noops\r\n\r\ntext {*\r\n  El contraejemplo encontrado es:\r\n  x = 0\r\n  y = 1\r\n  z = 0\r\n  zs = [1]\r\n  En efecto,\r\n  sust 1 0 (sust 0 1 [1]) = [0]\r\n  sust 0 0 [1] = [1]\r\n*}\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha resuelto de manera colaborativa ejercicios sobre la demostraci\u00f3n de propiedades de la funci\u00f3n de sustituci\u00f3n con Isabelle\/HOL. Su objetivo es ilustrar el uso del razonamiento por inducci\u00f3n y por casos en Isabelle. Para ca propiedad se presentan distintas demostraciones desde las autom\u00e1ticas a&#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":[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\/3307"}],"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=3307"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3307\/revisions"}],"predecessor-version":[{"id":3308,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3307\/revisions\/3308"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3307"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3307"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3307"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}