{"id":6812,"date":"2019-10-31T11:23:40","date_gmt":"2019-10-31T10:23:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6812"},"modified":"2019-11-01T11:24:54","modified_gmt":"2019-11-01T10:24:54","slug":"ra2019-programacion-funcional-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-programacion-funcional-con-isabelle-hol\/","title":{"rendered":"RA2019: 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-19\">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\/RA2019\/index.php\/Tema_1:_Programaci\u00f3n_funcional_en_Isabelle\">T1_Programacion_funcional_en_Isabelle.thy<\/a>.<\/p>\n<pre lang=\"isabelle\">\nchapter \u2039 Tema 1: Programaci\u00f3n funcional en Isabelle \u203a\n\ntheory T1_Programacion_funcional_en_Isabelle\nimports Main \nbegin\n\nsection \u2039 Introducci\u00f3n \u203a\n\ntext \u2039 En este tema se presenta el lenguaje funcional que est\u00e1\n  incluido en Isabelle. El lenguaje funcional es muy parecido a\n  Haskell. \u203a\n\nsection \u2039 N\u00fameros naturales, enteros y booleanos \u203a\n\ntext \u2039 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. \u203a\n\nvalue \"Suc 0\"  \n(* \u219d \"1\" :: \"nat\"*)\n\ntext \u2039 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. \u203a\n\nvalue \"(1::nat) + 2\" \n(* \u219d \"3\" :: \"nat\" *)\n\nvalue \"(1::nat) + 2 = 3\"\n(* \u219d \"True\" :: \"bool\" *) \n\ntext \u2039 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. \u203a\n\nvalue \"(2::nat) * 3\" \n(* \u219d \"6\" :: \"nat\"*)\n\nvalue \"(2::nat) * 3 = 6\"\n(* \u219d \"True\" :: \"bool\" *) \n\ntext \u2039 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. \u203a\n\nvalue \"(7::nat) div 3\"\n(* \u219d \"2\" :: \"nat\" *)\n\nvalue \"(7::nat) div 3 = 2\"\n(* \u219d \"True\" :: \"bool\" *)\n\ntext \u2039 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. \u203a\n\nvalue \"(7::nat) mod 3\"\n(* \u219d \"1\" :: \"nat\" *)\n\ntext \u2039 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. \u203a\n\nvalue \"(1::int) + -2\"  \n(* \u219d \"- 1\" :: \"int\"*)\n\ntext \u2039 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. \u203a\n\ntext \u2039 La conjunci\u00f3n de dos f\u00f3rmulas verdaderas es verdadera. \u203a\nvalue \"True \u2227 True\"  \n(* \u219d \"True\" :: \"bool\" *)\n\ntext \u2039 La conjunci\u00f3n de un f\u00f3rmula verdadera y una falsa es falsa. \u203a \nvalue \"True \u2227 False\"  \n(* \u219d \"False\" :: \"bool\" *)\n\ntext \u2039 La disyunci\u00f3n de una f\u00f3rmula verdadera y una falsa es\n  verdadera. \u203a \nvalue \"True \u2228 False\" \n(* \u219d \"True\" :: \"bool\" *)\n\ntext \u2039 La disyunci\u00f3n de dos f\u00f3rmulas falsas es falsa. \u203a\nvalue \"False \u2228 False\" \n(* \u219d \"False\" :: \"bool\"*)\n\ntext \u2039 La negaci\u00f3n de una f\u00f3rmula verdadera es falsa. \u203a\nvalue \"\u00acTrue\" \n(* \u219d \"False\" :: \"bool\"*)\n\ntext \u2039 Una f\u00f3rmula falsa implica una f\u00f3rmula verdadera. \u203a\nvalue \"False \u27f6 True\" \n(* \u219d \"True\" :: \"bool\"*)\n\ntext \u2039 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. \u203a\n\ntext \u2039 Ej. de simp: Todo elemento es igual a s\u00ed mismo. \u203a\nlemma \"\u2200x. x = x\" \nby simp\n\ntext \u2039 Ej. de simp: Existe un elemento igual a 1. \u203a\nlemma \"\u2203x. x = 1\" \nby simp\n\nsection \u2039 Definiciones no recursivas \u203a\n\ntext \u2039 La disyunci\u00f3n exclusiva de A y B se verifica si una es verdadera\n  y la otra no lo es. \u203a\n\ndefinition xor :: \"bool \u21d2 bool \u21d2 bool\" where\n  \"xor A B \u2261 (A \u2227 \u00acB) \u2228 (\u00acA \u2227 B)\"\n  \ntext \u2039 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\u203a\n\nlemma \"xor True True = False\"\nby (simp add: xor_def)\n\ntext \u2039 Se a\u00f1ade la definici\u00f3n de la disyunci\u00f3n exclusiva al conjunto de\n  reglas de simplificaci\u00f3n autom\u00e1ticas. \u203a\n\ndeclare xor_def [simp]\n\nlemma \"xor True False = True\"\nby simp\n\nsection \u2039 Definiciones locales \u203a\n\ntext \u2039 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\". \u203a\n\nvalue \"let x = 3::nat in x * x\" \n(* \u219d \"9\" :: \"nat\" *)\n\nsection \u2039 Pares \u203a\n\ntext \u2039 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. \u203a \n\nvalue \"let p = (2,3)::nat \u00d7 nat in fst p + 1 = snd p\" \n(* \u219d \"True\" :: \"bool\" *)\n\nsection \u2039 Listas \u203a\n\ntext \u2039 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]. \u203a\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 \u2039 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]. \u203a \n\nvalue \"let xs = [a,b,c] in hd xs = a \u2227 tl xs = [b,c]\" \n(* \u219d \"True\" :: \"bool\" *)\n\ntext \u2039 (length xs) es la longitud de la lista xs. Por ejemplo, la\n  longitud de la lista [1,2,5] es 3. \u203a\n\nvalue \"length [1::nat,2,5]\" \n(* \u219d \"3\" :: \"nat\" *)\n\ntext \u2039 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. \u203a\n\nsection \u2039 Funciones an\u00f3nimas \u203a\n\ntext \u2039 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. \u203a\n\nvalue \"(\u03bbx. x + x) 1::nat\" \n(* \u219d \"2\" :: \"nat\" *)\n\nsection \u2039 Condicionales \u203a\n\ntext \u2039 El valor absoluto del entero x es x, si \"x \u2265 0\" y es -x en caso \n  contrario. \u203a\n\ndefinition absoluto :: \"int \u21d2 int\" where\n  \"absoluto x \u2261 (if x \u2265 0 then x else -x)\"\n\ntext \u2039 Ejemplo, el valor absoluto de -3 es 3. \u203a\n\nvalue \"absoluto(-3)\" \n(* \u219d \"3\" :: \"int\" *)\n\ntext \u2039 Def.: Un n\u00famero natural n es un sucesor si es de la forma \n  (Suc m). \u203a\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 \u2039 Ejemplo, el n\u00famero 3 es sucesor. \u203a\n\nvalue \"es_sucesor 3\" \n(* \u219d \"True\" :: \"bool\" *)\n\nsection \u2039 Tipos de datos y definiciones recursivas \u203a\n\ntext \u2039 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. \u203a \n\ndatatype 'a Lista = Vacia | Cons 'a \"'a Lista\"\n\ntext \u2039 (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\u203a\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 \u2039 Se puede declarar que acorte los nombres. \u203a\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 \u2039 (suma n) es la suma de los primeros n n\u00fameros naturales. Por\n  ejemplo,\n     suma 3 = 6\n\u203a\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 \u2039 (sumaImpares n) es la suma de los n primeros n\u00fameros impares. \n  Por ejemplo, \n     sumaImpares 3 = 9\n\u203a\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\/RA2019\/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. chapter \u2039 Tema 1: Programaci\u00f3n funcional en Isabelle \u203a theory T1_Programacion_funcional_en_Isabelle imports Main begin section \u2039 Introducci\u00f3n \u203a text \u2039 En este tema se presenta el&#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":[144],"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\/6812"}],"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=6812"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6812\/revisions"}],"predecessor-version":[{"id":6813,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6812\/revisions\/6813"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6812"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6812"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6812"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}