{"id":6314,"date":"2018-11-08T21:07:25","date_gmt":"2018-11-08T20:07:25","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6314"},"modified":"2018-11-16T17:56:52","modified_gmt":"2018-11-16T16:56:52","slug":"ra2018-programacion-funcional-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2018-programacion-funcional-con-isabelle-hol\/","title":{"rendered":"RA2018: Programaci\u00f3n funcional con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-18\">Razonamiento autom\u00e1tico<\/a> se ha presentado la programaci\u00f3n funcional en Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es <a href=\"https:\/\/www.glc.us.es\/~jalonso\/RA2018\/index.php\/Tema_1:_Programaci\u00f3n_funcional_en_Isabelle\">T1_Programacion_funcional_en_Isabelle.thy<\/a>.<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* Tema 1: Programaci\u00f3n funcional en Isabelle *}\n\ntheory T1_Programacion_funcional_en_Isabelle\nimports Main \nbegin\n\nsection {* Introducci\u00f3n *}\n\ntext {* En este tema se presenta el lenguaje funcional que est\u00e1\n  incluido en Isabelle. El lenguaje funcional es muy parecido a\n  Haskell. *}\n\nsection {* N\u00fameros naturales, enteros y booleanos *}\n\ntext {* En Isabelle est\u00e1n definidos los n\u00famero naturales con la sintaxis\n  de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).\n\n  Los n\u00fameros como el 1 son abreviaturas de los correspondientes en la\n  notaci\u00f3n de Peano, en este caso \"Suc 0\". \n\n  El tipo de los n\u00fameros naturales es nat. \n\n  Por ejemplo, el siguiente del 0 es el 1. *}\n\nvalue \"Suc 0\"  \n(* \u219d \"1\" :: \"nat\"*)\n\ntext {* En Isabelle est\u00e1 definida la suma de los n\u00fameros naturales:\n  (x + y) es la suma de x e y.\n\n  Por ejemplo, la suma de los n\u00fameros naturales 1 y 2 es el n\u00famero\n  natural 3. *}\n\nvalue \"(1::nat) + 2\" \n(* \u219d \"3\" :: \"nat\" *)\n\nvalue \"(1::nat) + 2 = 3\"\n(* \u219d \"True\" :: \"bool\" *) \n\ntext {* La notaci\u00f3n del par de dos puntos se usa para asignar un tipo a\n  un t\u00e9rmino (por ejemplo, (1::nat) significa que se considera que 1 es\n  un n\u00famero natural).   \n\n  En Isabelle est\u00e1 definida el producto de los n\u00fameros naturales:\n  (x * y) es el producto de x e y.\n\n  Por ejemplo, el producto de los n\u00fameros naturales 2 y 3 es el n\u00famero\n  natural 6. *}\n\nvalue \"(2::nat) * 3\" \n(* \u219d \"6\" :: \"nat\"*)\n\nvalue \"(2::nat) * 3 = 6\"\n(* \u219d \"True\" :: \"bool\" *) \n\ntext {* En Isabelle est\u00e1 definida la divisi\u00f3n de n\u00fameros naturales: \n  (n div m) es el cociente entero de x entre y.\n\n  Por ejemplo, la divisi\u00f3n natural de 7 entre 3 es 2. *}\n\nvalue \"(7::nat) div 3\"\n(* \u219d \"2\" :: \"nat\" *)\n\nvalue \"(7::nat) div 3 = 2\"\n(* \u219d \"True\" :: \"bool\" *)\n\ntext {* En Isabelle est\u00e1 definida el resto de divisi\u00f3n de n\u00fameros\n  naturales: (n mod m) es el resto de dividir n entre m.\n\n  Por ejemplo, el resto de dividir 7 entre 3 es 1. *}\n\nvalue \"(7::nat) mod 3\"\n(* \u219d \"1\" :: \"nat\" *)\n\ntext {* En Isabelle tambi\u00e9n est\u00e1n definidos los n\u00fameros enteros. El tipo\n  de los enteros se representa por int.\n\n  Por ejemplo, la suma de 1 y -2 es el n\u00famero entero -1. *}\n\nvalue \"(1::int) + -2\"  \n(* \u219d \"- 1\" :: \"int\"*)\n\ntext {* Los numerales est\u00e1n sobrecargados. Por ejemplo, el 1 puede ser\n  un natural o un entero, dependiendo del contexto. \n\n  Isabelle resuelve ambig\u00fcedades mediante inferencia de tipos.\n\n  A veces, es necesario usar declaraciones de tipo para resolver la\n  ambig\u00fcedad.\n\n  En Isabelle est\u00e1n definidos los valores booleanos (True y False), las\n  conectivas (\u00ac, \u2227, \u2228, \u27f6 y \u2194) y los cuantificadores (\u2200 y \u2203). \n\n  El tipo de los booleanos es bool. *}\n\ntext {* La conjunci\u00f3n de dos f\u00f3rmulas verdaderas es verdadera. *}\nvalue \"True \u2227 True\"  \n(* \u219d \"True\" :: \"bool\" *)\n\ntext {* La conjunci\u00f3n de un f\u00f3rmula verdadera y una falsa es falsa. *} \nvalue \"True \u2227 False\"  \n(* \u219d \"False\" :: \"bool\" *)\n\ntext {* La disyunci\u00f3n de una f\u00f3rmula verdadera y una falsa es\n  verdadera. *} \nvalue \"True \u2228 False\" \n(* \u219d \"True\" :: \"bool\" *)\n\ntext {* La disyunci\u00f3n de dos f\u00f3rmulas falsas es falsa. *}\nvalue \"False \u2228 False\" \n(* \u219d \"False\" :: \"bool\"*)\n\ntext {* La negaci\u00f3n de una f\u00f3rmula verdadera es falsa. *}\nvalue \"\u00acTrue\" \n(* \u219d \"False\" :: \"bool\"*)\n\ntext {* Una f\u00f3rmula falsa implica una f\u00f3rmula verdadera. *}\nvalue \"False \u27f6 True\" \n(* \u219d \"True\" :: \"bool\"*)\n\ntext {* Un lema introduce una proposici\u00f3n seguida de una demostraci\u00f3n. \n\n  Isabelle dispone de varios procedimientos autom\u00e1ticos para generar\n  demostraciones, uno de los cuales es el de simplificaci\u00f3n (llamado\n  simp). \n\n  El procedimiento simp aplica un conjunto de reglas de reescritura, que\n  inicialmente contiene un gran n\u00famero de reglas relativas a los objetos\n  definidos. *}\n\ntext {* Ej. de simp: Todo elemento es igual a s\u00ed mismo. *}\nlemma \"\u2200x. x = x\" \nby simp\n\ntext {* Ej. de simp: Existe un elemento igual a 1. *}\nlemma \"\u2203x. x = 1\" \nby simp\n\nsection {* Definiciones no recursivas *}\n\ntext {* La disyunci\u00f3n exclusiva de A y B se verifica si una es verdadera\n  y la otra no lo es. *}\n\ndefinition xor :: \"bool \u21d2 bool \u21d2 bool\" where\n  \"xor A B \u2261 (A \u2227 \u00acB) \u2228 (\u00acA \u2227 B)\"\n  \ntext {* Prop.: La disyunci\u00f3n exclusiva de dos f\u00f3rmulas verdaderas es\n  falsa. \n\n  Dem.: Por simplificaci\u00f3n, usando la definici\u00f3n de la disyunci\u00f3n\n  exclusiva. \n*}\n\nlemma \"xor True True = False\"\nby (simp add: xor_def)\n\ntext {* Se a\u00f1ade la definici\u00f3n de la disyunci\u00f3n exclusiva al conjunto de\n  reglas de simplificaci\u00f3n autom\u00e1ticas. *}\n\ndeclare xor_def [simp]\n\nlemma \"xor True False = True\"\nby simp\n\nsection {* Definiciones locales *}\n\ntext {* Se puede asignar valores a variables locales mediante 'let' y\n  usarlo en las expresiones dentro de 'in'. \n\n  Por ejemplo, si x es el n\u00famero natural 3, entonces \"x*x = 9\". *}\n\nvalue \"let x = 3::nat in x * x\" \n(* \u219d \"9\" :: \"nat\" *)\n\nsection {* Pares *}\n\ntext {* Un par se representa escribiendo los elementos entre par\u00e9ntesis\n  y separados por coma.\n  \n  El tipo de los pares es el producto de los tipos.\n  \n  La funci\u00f3n fst devuelve el primer elemento de un par y la snd el\n  segundo. \n\n  Por ejemplo, si p es el par de n\u00fameros naturales (2,3), entonces la\n  suma del primer elemento de p y 1 es igual al segundo elemento de\n  p. *} \n\nvalue \"let p = (2,3)::nat \u00d7 nat in fst p + 1 = snd p\" \n(* \u219d \"True\" :: \"bool\" *)\n\nsection {* Listas *}\n\ntext {* Una lista se representa escribiendo los elementos entre\n  corchetes y separados por comas.\n  \n  La lista vac\u00eda se representa por [].\n  \n  Todos los elementos de una lista tienen que ser del mismo tipo.\n  \n  El tipo de las listas de elementos del tipo a es (a list).\n  \n  El t\u00e9rmino (x#xs) representa la lista obtenida a\u00f1adiendo el elemento x\n  al principio de la lista xs. \n\n  Por ejemplo, la lista obtenida a\u00f1adiendo sucesivamente a la lista\n  vac\u00eda los elementos z, y y x a es [x,y,z]. *}\n\nvalue \"x#(y#(z#[]))\" \n(* \u219d \"[x, y, z]\" :: \"'a list\" *)\n\nvalue \"(1::int)#(2#(3#[]))\"\n(* \u219d \"[1, 2, 3]\" :: \"int list\" *)\n\ntext {* Funciones de descomposici\u00f3n de listas:\n  \u00b7 (hd xs) es el primer elemento de la lista xs.\n  \u00b7 (tl xs) es el resto de la lista xs.\n\n  Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a\n  y el resto de xs es [b,c]. *} \n\nvalue \"let xs = [a,b,c] in hd xs = a \u2227 tl xs = [b,c]\" \n(* \u219d \"True\" :: \"bool\" *)\n\ntext {* (length xs) es la longitud de la lista xs. Por ejemplo, la\n  longitud de la lista [1,2,5] es 3. *}\n\nvalue \"length [1::nat,2,5]\" \n(* \u219d \"3\" :: \"nat\" *)\n\ntext {* En la p\u00e1gina 10 de \"What's in Main\" \n  <p><a href=\"https:\/\/isabelle.in.tum.de\/dist\/Isabelle2018\/doc\/main.pdf\" target=\"_blank\" rel=\"noopener noreferrer nofollow\">Click to access main.pdf<\/a><\/p>\n  y en la sesi\u00f3n 66 de \"Isabelle\/HOL \u2014 Higher-Order Logic\"\n  <p><a href=\"https:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/HOL\/document.pdf\" target=\"_blank\" rel=\"noopener noreferrer nofollow\">Click to access document.pdf<\/a><\/p>\n  se encuentran m\u00e1s definiciones y propiedades de las listas. *}\n\nsection {* Funciones an\u00f3nimas *}\n\ntext {* En Isabelle pueden definirse funciones an\u00f3nimas.  \n\n  Por ejemplo, el valor de la funci\u00f3n que a un n\u00famero le asigna su doble\n  aplicada a 1 es 2. *}\n\nvalue \"(\u03bbx. x + x) 1::nat\" \n(* \u219d \"2\" :: \"nat\" *)\n\nsection {* Condicionales *}\n\ntext {* El valor absoluto del entero x es x, si \"x \u2265 0\" y es -x en caso \n  contrario. *}\n\ndefinition absoluto :: \"int \u21d2 int\" where\n  \"absoluto x \u2261 (if x \u2265 0 then x else -x)\"\n\ntext {* Ejemplo, el valor absoluto de -3 es 3. *}\n\nvalue \"absoluto(-3)\" \n(* \u219d \"3\" :: \"int\" *)\n\ntext {* Def.: Un n\u00famero natural n es un sucesor si es de la forma \n  (Suc m). *}\n\ndefinition es_sucesor :: \"nat \u21d2 bool\" where\n  \"es_sucesor n \u2261 (case n of \n    0     \u21d2 False \n  | Suc m \u21d2 True)\"\n  \ntext {* Ejemplo, el n\u00famero 3 es sucesor. *}\n\nvalue \"es_sucesor 3\" \n(* \u219d \"True\" :: \"bool\" *)\n\nsection {* Tipos de datos y definiciones recursivas *}\n\ntext {* Una lista de elementos de tipo a es la lista Vacia o se obtiene\n  a\u00f1adiendo, con Cons, un elemento de tipo a a una lista de elementos de\n  tipo a. *} \n\ndatatype 'a Lista = Vacia | Cons 'a \"'a Lista\"\n\ntext {* (conc xs ys) es la concatenaci\u00f3n de las lista xs e ys. Por\n  ejemplo, \n     conc (Cons a (Cons b Vacia)) (Cons c Vacia)\n     = Cons a (Cons b (Cons c Vacia))\n*}\n\nfun conc :: \"'a Lista \u21d2 'a Lista \u21d2 'a Lista\" where\n  \"conc Vacia ys       = ys\"\n| \"conc (Cons x xs) ys = Cons x (conc xs ys)\"\n\nvalue \"conc (Cons a (Cons b Vacia)) (Cons c Vacia)\"\n(* \u219d Lista.Cons a (Lista.Cons b (Lista.Cons c Vacia)) *)\n\ntext {* Se puede declarar que acorte los nombres. *}\n\ndeclare [[names_short]]\n\nvalue \"conc (Cons a (Cons b Vacia)) (Cons c Vacia)\"\n(* \u219d Cons a (Cons b (Cons c Vacia) *)\n\ntext {* (suma n) es la suma de los primeros n n\u00fameros naturales. Por\n  ejemplo,\n     suma 3 = 6\n*}\n\nfun suma :: \"nat \u21d2 nat\" where\n  \"suma 0       = 0\"\n| \"suma (Suc m) = (Suc m) + suma m\"\n\nvalue \"suma 3\" \n(* \u219d \"6\" :: nat *)\n\ntext {* (sumaImpares n) es la suma de los n primeros n\u00fameros impares. \n  Por ejemplo, \n     sumaImpares 3 = 9\n*}\n\nfun sumaImpares :: \"nat \u21d2 nat\" where\n  \"sumaImpares 0       = 0\"\n| \"sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n\"\n\nvalue \"sumaImpares 3\" \n(* \u219d \"9\" :: nat *)\n\nend\n<\/pre>\n<p>Como tarea se propuso la resoluci\u00f3n de los ejercicios de la <a href=\"http:\/\/www.glc.us.es\/~jalonso\/RA2018\/index.php\/R1\">1\u00aa relaci\u00f3n<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha presentado la programaci\u00f3n funcional en Isabelle\/HOL. La teor\u00eda con los ejemplos presentados en la clase es T1_Programacion_funcional_en_Isabelle.thy.<\/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":[322],"tags":[144,323],"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\/6314"}],"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=6314"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6314\/revisions"}],"predecessor-version":[{"id":6349,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6314\/revisions\/6349"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6314"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6314"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6314"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}