{"id":1341,"date":"2011-03-10T14:22:22","date_gmt":"2011-03-10T14:22:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1341"},"modified":"2011-04-28T08:43:47","modified_gmt":"2011-04-28T08:43:47","slug":"dao2011-razonamiento-sobre-programas-con-isabelle","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/dao2011-razonamiento-sobre-programas-con-isabelle\/","title":{"rendered":"DAO2011: Razonamiento sobre programas con Isabelle"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAO2011\">Demostraci\u00f3n asistida por ordenador (DAO2011)<\/a> se ha estudiado c\u00f3mo demostrar con Isabelle propiedades de programas funcionales.<\/p>\n<p>La teor\u00eda correspondiente a la clase es <a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAO2011\/index.php5\/Tema_2:_Razonamiento_sobre_programas\">Tema_2.thy<\/a> cuyo contenido se muestra a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Razonamiento sobre programas en Isabelle *}\r\n\r\ntheory Tema_2\r\nimports Main Efficient_Nat\r\nbegin\r\n\r\ntext {* \r\n  En este tema se demuestra con Isabelle las propiedades de los\r\n  programas funcionales como se expone en el tema 8 del curso\r\n  \"Inform\u00e1tica\" que puede leerse en\r\n  <p><a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/temas\/tema-8t.pdf\" target=\"_blank\" rel=\"noopener noreferrer nofollow\">Click to access tema-8t.pdf<\/a><\/p>\r\n*}\r\n\r\ntext {* ----------------------------------------------------------------\r\n  Ejercicio 1. Definir, por recursi\u00f3n, la funci\u00f3n\r\n     longitud :: \"'a list \u21d2 nat\" where\r\n  tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,\r\n     longitud [4,2,5] = 3\r\n  ------------------------------------------------------------------- *}\r\n\r\nfun longitud :: \"'a list \u21d2 nat\" where\r\n  \"longitud []     = 0\"\r\n| \"longitud (x#xs) = 1 + longitud xs\"\r\n   \r\nvalue \"longitud [4,2,5]\" -- \"= 3\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 2. Demostrar que \r\n     longitud [4,2,5] = 3\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"longitud [4,2,5] = 3\"\r\nby simp\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 3. Definir la funci\u00f3n\r\n     fun intercambia :: \"'a \u00d7 'b \u21d2 'b \u00d7 'a\"\r\n  tal que (intercambia p) es el par obtenido intercambiando las\r\n  componentes del par p. Por ejemplo,\r\n     \"intercambia (2,3) = (3,2)\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun intercambia :: \"'a \u00d7 'b \u21d2 'b \u00d7 'a\" where\r\n  \"intercambia (x,y) = (y,x)\"\r\n\r\nvalue \"intercambia (2,3)\" -- \"= (3,2)\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 4. Demostrar que \r\n     intercambia (intercambia (x,y)) = (x,y)\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\r\nby simp\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 5. Definir, por recursi\u00f3n, la funci\u00f3n\r\n     inversa :: \"'a list \u21d2 'a list\"\r\n  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los\r\n  elementos de xs. Por ejemplo,\r\n     inversa [3,2,5] = [5,2,3]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun inversa :: \"'a list \u21d2 'a list\" where\r\n  \"inversa [] = []\"\r\n| \"inversa (x#xs) = inversa xs @ [x]\"\r\n\r\nvalue \"inversa [3,2,5]\" -- \"= [5,2,3]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 6. Demostrar que \r\n     inversa [x] = [x]\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"inversa [x] = [x]\"\r\nby simp\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 7. Definir la funci\u00f3n\r\n     repite :: \"nat \u21d2 'a \u21d2 'a list\" where\r\n  tal que . Por ejemplo,\r\n     repite 3 5 = [5,5,5]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun repite :: \"nat \u21d2 'a \u21d2 'a list\" where\r\n  \"repite 0 x = []\"\r\n| \"repite (Suc n) x = x # (repite n x)\"\r\n\r\nvalue \"repite 3 5\" -- \"= [5,5,5]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 8. Demostrar que \r\n     longitud (repite n x) = n\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"longitud (repite n x) = n\"\r\nby (induct n) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 9. Definir la funci\u00f3n\r\n     fun conc :: \"'a list \u21d2 'a list \u21d2 'a list\"\r\n  tal que . Por ejemplo,\r\n     conc [2,3] [4,3,5] = [2,3,4,3,5]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun conc :: \"'a list \u21d2 'a list \u21d2 'a list\" where\r\n  \"conc []     ys = ys\"\r\n| \"conc (x#xs) ys = x # (conc xs ys)\"\r\n\r\nvalue \"conc [2,3] [4,3,5]\" -- \"= [2,3,4,3,5]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 10. Demostrar que \r\n     conc xs (conc ys zs) = (conc xs ys) zs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 11. Refutar que \r\n     conc xs ys = conc ys xs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"conc xs ys = conc ys xs\"\r\nquickcheck\r\noops\r\n\r\ntext {* Encuentra el contraejemplo, \r\n  xs = [a\\<^isub>2]\r\n  ys = [a\\<^isub>1] *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 12. Demostrar que \r\n     conc xs [] = xs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"conc xs [] = xs\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 13. Demostrar que \r\n     longitud (conc xs ys) = longitud xs + longitud ys\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 14. Definir la funci\u00f3n\r\n     coge :: \"nat \u21d2 'a list \u21d2 'a list\"\r\n  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por\r\n  ejemplo, \r\n     coge 2 [3,7,5,4] = [3,7]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun coge :: \"nat \u21d2 'a list \u21d2 'a list\" where\r\n  \"coge n [] = []\"\r\n| \"coge 0 xs = []\"\r\n| \"coge (Suc n) (x#xs) = x # (coge n xs)\"\r\n\r\nvalue \"coge 2 [3,7,5,4]\" -- \"= [3,7]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 15. Definir la funci\u00f3n\r\n     elimina :: \"nat \u21d2 'a list \u21d2 'a list\"\r\n  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por\r\n  ejemplo, \r\n     elimina 2 [3,7,5,4] = [5,4]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun elimina :: \"nat \u21d2 'a list \u21d2 'a list\" where\r\n  \"elimina n [] = []\"\r\n| \"elimina 0 xs = xs\"\r\n| \"elimina (Suc n) (x#xs) = elimina n xs\"\r\n\r\nvalue \"elimina 2 [3,7,5,4]\" -- \"= [5,4]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 16. Demostrar que \r\n     conc (coge n xs) (elimina n xs) = xs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\r\nby (induct rule: coge.induct) auto\r\n\r\ntext {* coge.induct es el esquema de inducci\u00f3n asociado a la definici\u00f3n\r\n  de la funci\u00f3n coge. Puede verse como sigue: *}\r\n\r\nthm coge.induct\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 17. Definir la funci\u00f3n\r\n     esVacia :: \"'a list \u21d2 bool\"\r\n  tal que (esVacia xs) se verifica si xs es la lista vac\u00eda. Por ejemplo, \r\n     esVacia []  = True\r\n     esVacia [1] = False\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun esVacia :: \"'a list \u21d2 bool\" where\r\n  \"esVacia []     = True\"\r\n| \"esVacia (x#xs) = False\"\r\n\r\nvalue \"esVacia []\"  -- \"= True\"\r\nvalue \"esVacia [1]\" -- \"= False\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 18. Demostrar que \r\n     esVacia xs = esVacia (conc xs xs)\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"esVacia xs = esVacia (conc xs xs)\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 19. Definir la funci\u00f3n\r\n     inversaAc :: \"'a list \u21d2 'a list\"\r\n  tal que (inversaAc xs) es a inversa de xs calculada usando\r\n  acumuladores. Por ejemplo, \r\n     inversaAc [3,2,5] = [5,2,3]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun inversaAcAux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\r\n  \"inversaAcAux [] ys = ys\"\r\n| \"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)\"\r\n\r\nfun inversaAc :: \"'a list \u21d2 'a list\" where\r\n  \"inversaAc xs = inversaAcAux xs []\"\r\n\r\nvalue \"inversaAc [3,2,5]\" -- \"= [5,2,3]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 20. Demostrar que \r\n     inversaAcAux xs ys = (inversa xs)@ys\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma inversaAcAux_es_inversa:\r\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\r\nby (induct xs arbitrary: ys) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 21. Demostrar que \r\n     inversaAc xs = inversa xs\r\n  ------------------------------------------------------------------- *}\r\n\r\ncorollary \"inversaAc xs = inversa xs\"\r\nby (simp add: inversaAcAux_es_inversa)\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 22. Definir la funci\u00f3n\r\n     sum :: \"int list \u21d2 int\" \r\n  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,\r\n     sum [3,2,5] = 10\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun sum :: \"int list \u21d2 int\" where\r\n  \"sum []     = 0\"\r\n| \"sum (x#xs) = x + sum xs\"\r\n\r\nvalue \"sum [3,2,5]\" -- \"= 10\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 23. Definir la funci\u00f3n\r\n     map :: ('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\r\n  tal que (map f xs) es la lista obtenida aplicando la funci\u00f3n f a los\r\n  elementos de xs. Por ejemplo,\r\n     map (\u03bbx. 2*x) [3,2,5] = [6,4,10]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun map :: \"('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\" where\r\n  \"map f []     = []\"\r\n| \"map f (x#xs) = (f x) # map f xs\"\r\n\r\nvalue \"map (\u03bbx. 2*x) [3::int,2,5]\" -- \"= [6,4,10]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 24. Demostrar que \r\n     sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 25. Demostrar que \r\n     longitud (map f xs) = longitud xs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"longitud (map f xs) = longitud xs\"\r\nby (induct xs) auto\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Demostraci\u00f3n asistida por ordenador (DAO2011) se ha estudiado c\u00f3mo demostrar con Isabelle propiedades de programas funcionales. La teor\u00eda correspondiente a la clase es Tema_2.thy cuyo contenido se muestra a continuaci\u00f3n<\/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":[165],"tags":[289],"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\/1341"}],"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=1341"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1341\/revisions"}],"predecessor-version":[{"id":1352,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1341\/revisions\/1352"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1341"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1341"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1341"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}