{"id":6884,"date":"2019-11-21T15:32:10","date_gmt":"2019-11-21T14:32:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6884"},"modified":"2019-12-06T15:33:16","modified_gmt":"2019-12-06T14:33:16","slug":"ra2019-ejercicios-de-razonamiento-sobre-programas-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-ejercicios-de-razonamiento-sobre-programas-en-isabelle-hol\/","title":{"rendered":"RA2019: Ejercicios de razonamiento sobre programas en Isabelle\/HOL"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-19\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de la 2\u00aa relaci\u00f3n de ejercicios de razonamiento sobre programas. Para cada propiedad se dan dos demostraciones en Isabelle\/HOL: la primera autom\u00e1tica y la segunda aplicativa detallando los pasos.<\/p>\n<p>La teor\u00eda con las soluciones de los ejercicios es la siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039R2: Razonamiento sobre programas\u203a\n\ntheory R2_Razonamiento_sobre_programas_sol\nimports Main \nbegin\n\ndeclare [[names_short]]\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 1.1. Definir la funci\u00f3n\n     sumaImpares :: nat \u21d2 nat\n  tal que (sumaImpares n) es la suma de los n primeros n\u00fameros\n  impares. Por ejemplo,\n     sumaImpares 5  =  25\n  ------------------------------------------------------------------\u203a\n\nfun sumaImpares :: \"nat \u21d2 nat\" where\n  \"sumaImpares 0 = 0\"\n| \"sumaImpares (Suc n) = sumaImpares n + (2*n+1)\"\n\nvalue \"sumaImpares 5 = 25\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 1.2. Demostrar detallamente que \n     sumaImpares n = n*n\n  -------------------------------------------------------------------\u203a\n\nlemma \"sumaImpares n = n*n\"\n  apply (induct n) \n   apply (simp only: sumaImpares.simps(1))\n  apply (simp only: sumaImpares.simps(2))\n  apply simp\n  done\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 1.3. Demostrar autom\u00e1ticamente que \n     sumaImpares n = n*n\n  -------------------------------------------------------------------\u203a\n\nlemma \"sumaImpares n = n*n\"\n  by (induct n) simp_all\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 2.1. Definir la funci\u00f3n\n     sumaPotenciasDeDosMasUno :: nat \u21d2 nat\n  tal que \n     (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. \n  Por ejemplo, \n     sumaPotenciasDeDosMasUno 3  =  16\n  ------------------------------------------------------------------\u203a\n\nfun sumaPotenciasDeDosMasUno :: \"nat \u21d2 nat\" where\n  \"sumaPotenciasDeDosMasUno 0 = 2\"\n| \"sumaPotenciasDeDosMasUno (Suc n) = \n      sumaPotenciasDeDosMasUno n + 2^(n+1)\"\n\nvalue \"sumaPotenciasDeDosMasUno 3 = 16\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 2.2. Demostrar detalladamente que \n     sumaPotenciasDeDosMasUno n = 2^(n+1)\n  -------------------------------------------------------------------\u203a\n\nlemma \"sumaPotenciasDeDosMasUno n = 2^(n+1)\"\n  apply (induct n) \n   apply (simp only: sumaPotenciasDeDosMasUno.simps(1))\n   apply simp  \n  apply (simp only: sumaPotenciasDeDosMasUno.simps(2))\n  apply simp\n  done\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 2.3. Demostrar autom\u00e1ticamente que \n     sumaPotenciasDeDosMasUno n = 2^(n+1)\n  -------------------------------------------------------------------\u203a\n\nlemma \"sumaPotenciasDeDosMasUno n = 2^(n+1)\"\n  by (induct n) simp_all\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 3.1. Definir la funci\u00f3n\n     copia :: nat \u21d2 'a \u21d2 'a list\n  tal que (copia n x) es la lista formado por n copias del elemento\n  x. Por ejemplo, \n     copia 3 x = [x,x,x]\n  ------------------------------------------------------------------\u203a\n\nfun copia :: \"nat \u21d2 'a \u21d2 'a list\" where\n  \"copia 0 x       = []\"\n| \"copia (Suc n) x = x # copia n x\"\n\nvalue \"copia 3 x = [x,x,x]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 3.2. Definir la funci\u00f3n\n     todos :: ('a \u21d2 bool) \u21d2 'a list \u21d2 bool\n  tal que (todos p xs) se verifica si todos los elementos de xs cumplen\n  la propiedad p. Por ejemplo,\n     todos (\u03bbx. x>(1::nat)) [2,6,4] = True\n     todos (\u03bbx. x>(2::nat)) [2,6,4] = False\n  ------------------------------------------------------------------\u203a\n\nfun todos :: \"('a \u21d2 bool) \u21d2 'a list \u21d2 bool\" where\n  \"todos p []     = True\"\n| \"todos p (x#xs) = (p x \u2227 todos p xs)\"\n\nvalue \"todos (\u03bbx. x>(1::nat)) [2,6,4] = True\"\nvalue \"todos (\u03bbx. x>(2::nat)) [2,6,4] = False\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 3.3. Demostrar detalladamente que todos los elementos de \n  (copia n x) son iguales a x. \n  -------------------------------------------------------------------\u203a\n\nlemma \"todos (\u03bby. y=x) (copia n x)\"\n  apply (induct n)\n   apply (simp only: copia.simps(1))\n   apply (simp only:todos.simps(1))\n  apply (simp only: copia.simps(2))\n  apply (simp only:todos.simps(2))\n  done\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 3.4. Demostrar autom\u00e1ticamente que todos los elementos de \n  (copia n x) son iguales a x. \n  -------------------------------------------------------------------\u203a\n\nlemma \"todos (\u03bby. y=x) (copia n x)\"\n  by (induct n) simp_all\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 4.1. Definir, recursivamente y sin usar (@), la funci\u00f3n\n     amplia :: 'a list \u21d2 'a \u21d2 'a list\n  tal que (amplia xs y) es la lista obtenida a\u00f1adiendo el elemento y al\n  final de la lista xs. Por ejemplo,\n     amplia [d,a] t = [d,a,t]\n  ------------------------------------------------------------------\u203a\n\nfun amplia :: \"'a list \u21d2 'a \u21d2 'a list\" where\n  \"amplia []     y = [y]\"\n| \"amplia (x#xs) y = x # amplia xs y\"\n\nvalue \"amplia [d,a] t = [d,a,t]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 4.2. Demostrar detalladamente que \n     amplia xs y = xs @ [y]\n  -------------------------------------------------------------------\u203a\n\nlemma \"amplia xs y = xs @ [y]\"\n  apply (induct xs) \n   apply (simp only: amplia.simps(1))\n   apply (simp only: append.simps(1))\n  apply (simp only: amplia.simps(2))\n  apply (simp only: append.simps(2))\n  done\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 4.3. Demostrar autom\u00e1ticamente que \n     amplia xs y = xs @ [y]\n  -------------------------------------------------------------------\u203a\n\nlemma \"amplia xs y = xs @ [y]\"\n  by (induct xs) simp_all\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se han comentado las soluciones de la 2\u00aa relaci\u00f3n de ejercicios de razonamiento sobre programas. Para cada propiedad se dan dos demostraciones en Isabelle\/HOL: la primera autom\u00e1tica y la segunda aplicativa detallando los pasos. La teor\u00eda con las soluciones de los&#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":[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\/6884"}],"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=6884"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6884\/revisions"}],"predecessor-version":[{"id":6886,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6884\/revisions\/6886"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6884"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6884"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6884"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}