{"id":6832,"date":"2019-11-14T09:51:08","date_gmt":"2019-11-14T08:51:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6832"},"modified":"2019-11-15T09:51:41","modified_gmt":"2019-11-15T08:51:41","slug":"ra2019-razonamiento-sobre-programas-con-isabelle-hol-2-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-razonamiento-sobre-programas-con-isabelle-hol-2-2\/","title":{"rendered":"RA2019: Razonamiento sobre programas con Isabelle\/HOL (2\/2)"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-19\">Razonamiento autom\u00e1tico<\/a> se ha completado el estudio (comenzado en la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-razonamiento-sobre-programas-con-isabelle-hol\/\">clase anterior<\/a>) sobre demostraci\u00f3n de propiedades de programas con Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039Tema 2: Razonamiento sobre programas\u203a\n\ntheory T2_Razonamiento_sobre_programas\nimports Main \nbegin\nsection \u2039Heur\u00edstica de generalizaci\u00f3n\u203a\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 19. Definir la funci\u00f3n\n     inversaAc :: 'a list \u21d2 'a list\n  tal que (inversaAc xs) es a inversa de xs calculada usando\n  acumuladores. Por ejemplo, \n     inversaAc [a,c,b,e] = [e,b,c,a]\n  ------------------------------------------------------------------ \u203a\n\nfun inversaAcAux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\n  \"inversaAcAux [] ys     = ys\"\n| \"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)\"\n\ndefinition inversaAc :: \"'a list \u21d2 'a list\" where\n  \"inversaAc xs = inversaAcAux xs []\"\n\nvalue \"inversaAc [a,c,b,e] = [e,b,c,a]\"\n\ntext \u2039Lema. [Ejemplo de equivalencia entre las definiciones]\n  La inversa de [a,b,c] es lo mismo calculada con la primera definici\u00f3n\n  que con la segunda.\u203a\n\nlemma \"inversaAc [a,b,c] = inversa [a,b,c]\"\n  apply (simp only: inversaAc_def)\n  apply (simp only: inversaAcAux.simps(2))\n  apply (simp only: inversaAcAux.simps(1))\n  apply (simp only: inversa.simps(2))\n  apply (simp only: inversa.simps(1))\n  apply (simp only: append.simps(1))\n  apply (simp only: append.simps(2))\n  apply (simp only: append.simps(1))\n  apply (simp only: append.simps(2))\n  apply (simp only: append.simps(1))\n  done\n\n(* Se puede simplificar la demostraci\u00f3n *)\nlemma \"inversaAc [a,b,c] = inversa [a,b,c]\"\n  by (simp add: inversaAc_def)\n\ntext \u2039Nota. [Ejemplo fallido de demostraci\u00f3n por inducci\u00f3n]\n  El siguiente intento de demostrar que para cualquier lista xs, se\n  tiene que  \"inversaAc xs = inversa xs\" falla.\u203a\n\nlemma \"inversaAc xs = inversa xs\"\n  apply (induct xs)\n   apply (simp only: inversaAc_def)\n   apply (simp only: inversaAcAux.simps(1))\n   apply (simp only: inversa.simps(1))\n  apply (simp only: inversaAc_def) \n  apply (simp only: inversaAcAux.simps(2))\n  apply (simp only: inversa.simps(2))\n  oops\n\ntext \u2039Nota. [Heur\u00edstica de generalizaci\u00f3n]\n  Cuando se use demostraci\u00f3n estructural, cuantificar universalmente las \n  variables libres (o, equivalentemente, considerar las variables libres\n  como variables arbitrarias).\n\n  Lema. [Lema con generalizaci\u00f3n]\n  Para toda lista ys se tiene \n     inversaAcAux xs ys = (inversa xs) @ ys\u203a\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 20. (p. 44) Demostrar que \n     inversaAcAux xs ys = (inversa xs) @ ys\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n aplicativa detallada *)\nlemma \"inversaAcAux xs ys = (inversa xs)@ys\"\n  apply (induct xs arbitrary: ys) \n   apply (simp only: inversaAcAux.simps(1))\n   apply (simp only: inversa.simps(1))\n   apply (simp only: append.simps(1))\n  apply (simp only: inversaAcAux.simps(2))\n  apply (simp only: inversa.simps(2))\n  apply (simp only: append_assoc)\n  apply (simp only: append.simps(2))\n  apply (simp only: append.simps(1))\n  done\n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"inversaAcAux xs ys = (inversa xs)@ys\"\n  apply (induct xs arbitrary: ys) \n   apply simp_all\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma inversaAcAux_es_inversa:\n \"inversaAcAux xs ys = (inversa xs)@ys\"\n  by (induct xs arbitrary: ys) simp_all\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 21. (p. 43) Demostrar que \n     inversaAc xs = inversa xs\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n aplicativa detallada *)\ncorollary \"inversaAc xs = inversa xs\"\n  apply (simp only: inversaAc_def)\n  apply (simp only: inversaAcAux_es_inversa)\n  apply (simp only: append_Nil2)\n  done \n\n(* Nota: El \u00faltimo simplificador se busca con *)  \nfind_theorems \"_ @ [] = _\"  \n\n(* Demostraci\u00f3n aplicativa no detallada *)\ncorollary \"inversaAc xs = inversa xs\"\n  apply (simp add: inversaAcAux_es_inversa inversaAc_def)\n  done \n\n(* Demostraci\u00f3n autom\u00e1tica *)\ncorollary \"inversaAc xs = inversa xs\"\n  by (simp add: inversaAcAux_es_inversa inversaAc_def)\n\nsection \u2039Demostraci\u00f3n por inducci\u00f3n para funciones de orden superior\u203a\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 22. Definir la funci\u00f3n\n     sum :: nat list \u21d2 nat\n  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,\n     sum [3,2,5] = 10\n  ------------------------------------------------------------------ \u203a\n\nfun sum :: \"nat list \u21d2 nat\" where\n  \"sum []     = 0\"\n| \"sum (x#xs) = x + sum xs\"\n\nvalue \"sum [3,2,5] = 10\"\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 23. Definir la funci\u00f3n\n     map :: ('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\n  tal que (map f xs) es la lista obtenida aplicando la funci\u00f3n f a los\n  elementos de xs. Por ejemplo,\n     map (\u03bbx. 2*x) [3::nat,2,5] = [6,4,10]\n     map ((*) 2)   [3::nat,2,5] = [6,4,10]\n     map ((+) 2)   [3::nat,2,5] = [5,4,7]\n  ------------------------------------------------------------------ \u203a\n\nfun map :: \"('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\" where\n  \"map f []     = []\"\n| \"map f (x#xs) = (f x) # map f xs\"\n\nvalue \"map (\u03bbx. 2*x) [3::nat,2,5] = [6,4,10]\"\nvalue \"map ((*) 2) [3::nat,2,5] = [6,4,10]\"\nvalue \"map ((+) 2)   [3::nat,2,5] = [5,4,7]\"\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 24. (p. 45) Demostrar que \n     sum (map ((*) 2) xs) = 2 * (sum xs)\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n aplicativa detallada *)\nlemma \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\n  apply (induct xs) \n    apply (simp only: map.simps(1))\n    apply (simp only: sum.simps(1))\n  apply (simp only: map.simps(2))\n  apply (simp only: sum.simps(2))\n  apply (simp only: add_mult_distrib2)\n  done\n\n(* Nota: El \u00faltimo simplificador se busca con *)  \nfind_theorems \"_ * (_ + _) = _\"\n  \n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\n  apply (induct xs) \n   apply simp_all\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\n  by (induct xs) simp_all\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 25. (p. 48) Demostrar que \n     longitud (map f xs) = longitud xs\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"longitud (map f xs) = longitud xs\"\n  apply (induct xs) \n    apply (simp only: map.simps(1))\n    apply (simp only: longitud.simps(1))\n  apply (simp only: map.simps(2))\n  apply (simp only: longitud.simps(2))\n  done\n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"longitud (map f xs) = longitud xs\"\n  apply (induct xs) \n   apply simp_all\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"longitud (map f xs) = longitud xs\"\n  by (induct xs) simp_all\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha completado el estudio (comenzado en la clase anterior) sobre demostraci\u00f3n de propiedades de programas con Isabelle\/HOL. La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<\/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":[333],"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\/6832"}],"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=6832"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6832\/revisions"}],"predecessor-version":[{"id":6833,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6832\/revisions\/6833"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6832"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6832"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6832"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}