{"id":1853,"date":"2012-01-19T08:05:13","date_gmt":"2012-01-19T08:05:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1853"},"modified":"2013-03-08T05:48:56","modified_gmt":"2013-03-08T05:48:56","slug":"ra2011-isabelle-como-un-lenguaje-funcional","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2011-isabelle-como-un-lenguaje-funcional\/","title":{"rendered":"RA2011: Isabelle como un lenguaje funcional"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-11\">Razonamiento autom\u00e1tico<\/a> se ha presentado <http=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\/\">Isabelle<\/a> como un lenguaje funcional.<\/p>\n<p>La clase se ha basado en la siguiente teor\u00eda Isabelle<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 6: Isabelle como un lenguaje funcional *}\r\n\r\ntheory Tema_6\r\nimports Main\r\nbegin\r\n\r\nsection {* Introducci\u00f3n *}\r\n\r\ntext {*\r\n  Esta notas son una introducci\u00f3n a la demostraci\u00f3n asistida utilizando\r\n  el sistema Isabelle\/HOL\/Isar. \r\n\r\n  La versi\u00f3n de Isabelle utilizada es la 2011.\r\n\r\n  Un lema introduce una proposici\u00f3n seguida de una demostraci\u00f3n.\r\n\r\n  Isabelle dispone de varios procedimientos autom\u00e1ticos para generar\r\n  demostraciones, uno de los cuales es el de simplificaci\u00f3n (llamado simp).\r\n\r\n  El procedimiento simp aplica un conjunto de reglas de reescritura que\r\n  inicialmente contiene un gran n\u00famero de reglas relativas a los objetos\r\n  definidos. \r\n\r\n  El ejemplo del lema m\u00e1s trivial es el siguiente\r\n*}\r\n\r\nlemma elMasTrivial: \"True\" \r\nby simp\r\n\r\ntext {* \r\n  En este cap\u00edtulos se presenta el lenguaje funcional que est\u00e1 incluido en\r\n  Isabelle. \r\n\r\n  El lenguaje funcional es muy parecido al ML est\u00e1ndard.\r\n*}\r\n\r\nsection {* N\u00fameros naturales, enteros y booleanos *}\r\n\r\ntext {*\r\n  En Isabelle est\u00e1n definidos los n\u00famero naturales con la sintaxis de\r\n  Peano usando dos constructores: \r\n  \u00b7 0 (cero) y \r\n  \u00b7 \"Suc n\" (el sucesor de n). \r\n  \r\n  Los n\u00fameros como el 1  son abreviaturas de los correspondientes en la\r\n  notaci\u00f3n de Peano, en este caso \"Suc 0\". \r\n  \r\n  El tipo de los n\u00fameros naturales es nat. \r\n\r\n  Lema [Ejemplo de simplificaci\u00f3n de n\u00fameros naturales]\r\n  El siguiente del 0 es el 1.\r\n*}\r\n\r\nlemma \"Suc 0 = 1\" \r\nby simp\r\n\r\ntext {* \r\n  En Isabelle est\u00e1n definida la suma y el producto de n\u00fameros naturales:\r\n  \u00b7 \"x+y\" es la suma de x e y \r\n  \u00b7 \"x*y\" es el producto de x e y \r\n\r\n  Lema [Ejemplo de suma]\r\n  La suma de los n\u00fameros naturales 1 y 2 es el n\u00famero natural 3.\r\n*}\r\n\r\nlemma \"1 + 2 = (3::nat)\" \r\nby simp\r\n\r\ntext {* \r\n  La notaci\u00f3n del par de dos puntos se usa para asignar un tipo a un t\u00e9rmino\r\n  (por ejemplo, 3::nat significa que se considera que 3 es un n\u00famero natural).\r\n\r\n  Lema [Ejemplo de producto]\r\n  El producto de los n\u00fameros naturales 2 y 3 es el n\u00famero natural 6.\r\n*}\r\n\r\nlemma \"2 * 3 = (6::nat)\" \r\nby simp\r\n\r\ntext {* \r\n  En Isabelle est\u00e1 definida la divisi\u00f3n de n\u00fameros naturales: \r\n  \u00b7 \"n div m\" es el cociente entero de n entre \"m\"\r\n  \u00b7 \"n mod m\" es el resto de dividir \"n\" entre \"m\".\r\n\r\n  Lema [Ejemplo de divisi\u00f3n]\r\n  La divisi\u00f3n natural de 7 entre 3 es 2.\r\n*}\r\n\r\nlemma \"7 div 3 = (2::nat)\" \r\nby simp\r\n\r\ntext {* \r\n  Lema [Ejemplo de resto]\r\n  El resto de dividir 7 entre 3 es 1.\r\n*}\r\n\r\nlemma \"7 mod 3 = (1::nat)\" \r\nby simp\r\n\r\ntext {* \r\n  En Isabelle tambi\u00e9n est\u00e1n definidos los n\u00fameros enteros. \r\n\r\n  El tipo de los enteros se representa por int.\r\n\r\n  Lema [Ejemplo de operaci\u00f3n con enteros]\r\n  La suma de 1 y -2 es el n\u00famero entero -1.\r\n*}\r\n\r\nlemma \"1 + -2 = (-1::int)\" \r\nby simp\r\n\r\ntext {* \r\n  Los numerales est\u00e1n sobrecargados. \r\n\r\n  Por ejemplo, el '1' puede ser un natural o un entero, dependiendo del\r\n  contexto. \r\n\r\n  Isabelle resuelve ambig\u00fcedades mediante inferencia de tipos.\r\n\r\n  A veces, es necesario usar declaraciones de tipo para resolver la ambig\u00fcedad.\r\n\r\n  En Isabelle est\u00e1n definidos \r\n  \u00b7 los valores booleanos  \"True, False\", \r\n  \u00b7 las conectivas \"\u00ac, \u2227, \u2228, \u27f6, \u2194\" y \r\n  \u00b7 los cuantificadores \"\u2200, \u2203\". \r\n\r\n  El tipo de los booleanos es bool. \r\n\r\n  Lema [Ejemplos de evaluaciones booleanas]\r\n    \u00b7 La conjunci\u00f3n de dos f\u00f3rmulas verdaderas es verdadera.\r\n    \u00b7 La conjunci\u00f3n de un f\u00f3rmula verdadera y una falsa es falsa.\r\n    \u00b7 La disyunci\u00f3n de una f\u00f3rmula verdadera y una falsa es verdadera.\r\n    \u00b7 La disyunci\u00f3n de dos f\u00f3rmulas falsas es falsa.\r\n    \u00b7 La negaci\u00f3n de una f\u00f3rmula verdadera es falsa.\r\n    \u00b7 Una f\u00f3rmula falsa implica una f\u00f3rmula verdadera.\r\n    \u00b7 Todo elemento es igual a s\u00ed mismo.\r\n    \u00b7 Existe un elemento igual a 1.\r\n*}\r\n\r\nlemma \"True \u2227 True = True\" \r\nby simp\r\n\r\nlemma \"True \u2227 False = False\" \r\nby simp\r\n \r\nlemma \"True \u2228 False = True\" \r\nby simp\r\n\r\nlemma \"False \u2228 False = False\" \r\nby simp\r\n\r\nlemma \"\u00ac True = (False::bool)\" \r\nby simp\r\n\r\nlemma \"False \u27f6 True\" \r\nby simp\r\n\r\nlemma \"\u2200 x. x = x\" \r\nby simp\r\n\r\nlemma \"\u2203 x. x = 1\" \r\nby simp\r\n\r\nsection {* Definiciones no recursivas *}\r\n\r\ntext {*\r\n  Definici\u00f3n [Ejemplo de definici\u00f3n no recursiva]\r\n  La disyunci\u00f3n exclusiva de A y B se verifica si una es verdadera y la\r\n  otra no lo es.\r\n*}\r\n\r\ndefinition xor :: \"bool \u21d2 bool \u21d2 bool\" where\r\n  \"xor A B \u2261 (A \u2227 \u00ac B) \u2228 (\u00ac A \u2227 B)\"\r\n\r\ntext {* \r\n  Lema [Ejemplo de demostraci\u00f3n con definiciones no recursivas]\r\n  La disyunci\u00f3n exclusiva de dos f\u00f3rmulas verdaderas es falsa.\r\n\r\n  Demostraci\u00f3n. Por simplificaci\u00f3n, usando la definici\u00f3n de la disyunci\u00f3n\r\n  exclusiva. \r\n*}\r\n\r\nlemma \"xor True True = False\"\r\nby (simp  add: xor_def)\r\n\r\ntext {* \r\n  Se a\u00f1ade la definici\u00f3n de la disyunci\u00f3n exlusiva al conjunto de reglas de\r\n  simplificaci\u00f3n autom\u00e1ticas.\r\n*}\r\n\r\ndeclare xor_def[simp]\r\n\r\nsection {* Definiciones locales *}\r\n\r\ntext {*\r\n  Se puede asignar valores a variables locales mediante 'let' y usarlo en las \r\n  expresiones dentro de 'in'. \r\n\r\n  Lema [Ejemplo de entorno local]\r\n  Sea x el n\u00famero natural 3. Entonces \"x \u00d7 x = 9\".\r\n*}\r\n\r\nlemma \"(let x = 3::nat in x * x = 9)\" \r\nby simp\r\n\r\nsection {* Pares *}\r\n\r\ntext {* \r\n  Un par se representa escribiendo los elementos entre par\u00e9ntesis y separados\r\n  por coma.\r\n  \r\n  El tipo de los pares es el producto de los tipos.\r\n  \r\n  La funci\u00f3n fst devuelve el primer elemento de un par y la snd el segundo.\r\n\r\n  Lema [Ejemplo de uso de pares]\r\n  Sea p el par de n\u00fameros naturales (2,3). La suma del primer elemento de\r\n  p y 1 es igual al segundo elemento de p.\r\n*}\r\n\r\nlemma \"let p = (2,3)::nat \u00d7 nat in fst p + 1 = snd p\" \r\nby simp\r\n\r\nsection {* Listas *}\r\n\r\ntext {*\r\n  Una lista se representa escribiendo los elementos entre corchetes y separados\r\n  por coma.\r\n  \r\n  La lista vac\u00eda se representa por [].\r\n\r\n  Todos los elementos de una lista tienen que ser del mismo tipo.\r\n  \r\n  El tipo de las listas de elementos del tipo a es \"a list\".\r\n\r\n  El t\u00e9rmino a#l representa la lista obtenida a\u00f1adiendo el elemento a al\r\n  principio de la lista l.\r\n\r\n  Lema [Ejemplo de construcci\u00f3n de listas]\r\n  La lista obtenida a\u00f1adiendo sucesivamente a la lista vac\u00eda los elementos 3,\r\n  2 y 1 es [1,2,3]. \r\n*}\r\n\r\nlemma \"1#(2#(3#[])) = [1,2,3]\" \r\nby simp\r\n\r\ntext {* \r\n  (hd l) es el primer elemento de la lista l.\r\n\r\n  (tl l) es el resto de la lista l.\r\n\r\n  Lema [Ejemplo de c\u00e1lculo con listas]\r\n  Sea l la lista de n\u00fameros naturales [1,2,3]. Entonces, el primero de l es 1 y\r\n  el resto de l es [2,3].  \r\n*}\r\n\r\nlemma \"let l = [1,2,3]::(nat list) in hd l = 1 \u2227 tl l = [2,3]\" \r\nby simp\r\n\r\ntext {* \r\n  (length l)es la longitud de la lista l.\r\n\r\n  Lema [Ejemplo de c\u00e1lculo de longitud]\r\n  La longitud de la lista [1,2,3] es 3.\r\n*}\r\n\r\nlemma \"length [1,2,3] = 3\" \r\nby simp\r\n\r\ntext {* \r\n  En la sesi\u00f3n 38 de \"HOL: The basis of Higher-Order Logic\"\r\n  (en http:\/\/isabelle.informatik.tu-muenchen.de\/library\/HOL\/outline.pdf)\r\n  se encuentran  m\u00e1s definiciones y propiedades de las listas.\r\n*}\r\n\r\nsection {* Registros *}\r\n\r\ntext {*\r\n  Un registro es una colecci\u00f3n de campos y valores. \r\n\r\n  Definici\u00f3n [Ejemplo de definici\u00f3n de registro]\r\n  Los puntos del plano pueden representarse mediante registros con dos campos,\r\n  las coordenadas, con valores enteros.  \r\n*}\r\n\r\nrecord punto = \r\n  coordenada_x :: int\r\n  coordenada_y :: int\r\n\r\ntext {* \r\n  Definici\u00f3n [Ejemplo de definici\u00f3n de un registro]\r\n  El punto pt tiene de coordenadas 3 y 7.  \r\n*}\r\n\r\ndefinition pt :: punto where\r\n  \"pt \u2261 (|coordenada_x = 3, coordenada_y = 7|)\"\r\n\r\ntext {* \r\n  Lema [Ejemplo de propiedad de registro]\r\n  La coordenada x del punto pt es 3.  \r\n*}\r\n\r\nlemma \"coordenada_x pt = 3\" \r\nby (simp add: pt_def)\r\n\r\ntext {* \r\n  Lema [Ejemplo de actualizaci\u00f3n de un registro]\r\n  Sea pt2 el punto obtenido a partir del punto pt cambiando el\r\n  valor de su coordenada x por 4. Entonces la coordenada x del punto pt2\r\n  es 4. \r\n*}\r\n\r\nlemma \"let pt2=pt(|coordenada_x:=4|) in coordenada_x (pt2) = 4\" \r\nby (simp add: pt_def)\r\n\r\nsection {* Funciones an\u00f3nimas *}\r\n\r\ntext {*\r\n  En Isabelle pueden definirse funciones an\u00f3nimas.  \r\n\r\n  Lema [Ejemplo de uso de funciones an\u00f3nimas]\r\n  El valor de la funci\u00f3n que a un n\u00famero le asigna su doble aplicada a 1 es 2.  \r\n*}\r\n\r\nlemma \"(\u03bb x. x + x) 1 = (2::nat)\" \r\nby simp\r\n\r\nsection {* Condicionales *}\r\n\r\ntext {*\r\n  Definici\u00f3n [Ejemplo con el condicional if]\r\n  El valor absoluto del entero x es x, si \"x \u2265 0\" y es -x en caso\r\n  contrario.    \r\n*}\r\n\r\ndefinition absoluto :: \"int \u21d2 int\" where\r\n  \"absoluto x \u2261 (if x \u2265 0 then x else -x)\"\r\n\r\ntext {* \r\n  Lema [Ejemplo de simplificaci\u00f3n con el condicional if]\r\n  El valor absoluto de -3 es 3.  \r\n*}\r\n\r\nlemma \"absoluto(-3) = 3\"\r\nby (simp add:absoluto_def) \r\n\r\ntext {* \r\n  Definici\u00f3n [Ejemplo con el condicional case]\r\n  Un n\u00famero natural n es un sucesor si es de la forma \"Suc m\".\r\n*}\r\n\r\ndefinition es_sucesor :: \"nat \u21d2 bool\" where\r\n  \"es_sucesor n \u2261\r\n  (case n of \r\n    0     \u21d2 False \r\n  | Suc m \u21d2 True)\"\r\n\r\ntext {* \r\n  Lema [Ejemplo de simplificaci\u00f3n con el condicional case]\r\n  El n\u00famero 3 es sucesor.  \r\n*}\r\n\r\nlemma \"es_sucesor 3\"\r\nby (simp add: es_sucesor_def)\r\n\r\nsection {* Tipos de datos y recursi\u00f3n primitiva *}\r\n\r\ntext {*\r\n  Definici\u00f3n [Ejemplo de definici\u00f3n de tipo de dato recursivo]\r\n  Una lista de elementos de tipo a es la lista Vacia o se obtiene a\u00f1adiendo,\r\n  con ConsLista, un elemento de tipo a a una lista de elementos de tipo a.\r\n*}\r\n\r\ndatatype 'a Lista = Vacia | ConsLista 'a \"'a Lista\"\r\n\r\ntext {* \r\n  Definici\u00f3n [Ejemplo de definici\u00f3n primitiva recursiva]\r\n  (conc xs ys) es la concatenaci\u00f3n de las lista xs e ys.  \r\n*}\r\n\r\nprimrec conc :: \"'a Lista \u21d2 'a Lista \u21d2 'a Lista\" where\r\n  \"conc Vacia ys = ys\"\r\n| \"conc (ConsLista x xs) ys = ConsLista x (conc xs ys)\"\r\n\r\ntext {* \r\n  Lema [Ejemplo de simplificaci\u00f3n con tipo de dato recursivo]\r\n  La concatenaci\u00f3n de la lista formada por 1 y 2 con la lista formada por el 3\r\n  es la lista cuyos elementos son 1,2 y 3.\r\n*}\r\n\r\nlemma \"conc (ConsLista 1 (ConsLista 2 Vacia)) (ConsLista 3 Vacia) =\r\n       (ConsLista 1 (ConsLista 2 (ConsLista 3 Vacia)))\"\r\nby simp\r\n\r\ntext {* \r\n  Ejercicio [Ejemplo de definici\u00f3n primitiva recursiva sobre los naturales] \r\n  Definir una funci\u00f3n que sume los primeros n n\u00fameros naturales y usarla para\r\n  comprobar que la suma de los 3 primeros n\u00fameros naturales es 6.\r\n*}\r\n\r\nprimrec suma :: \"nat \u21d2 nat\" where\r\n  \"suma 0 = 0\"\r\n| \"suma (Suc m) = (Suc m) + suma m\"\r\n\r\nlemma \"suma 3 = 6\"\r\nby (simp add: suma_def) \r\n\r\nvalue \"suma 3\"\r\nvalue \"2+(3::int)\"\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha presentado Isabelle como un lenguaje funcional. La clase se ha basado en la siguiente teor\u00eda Isabelle<\/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":[187],"tags":[296],"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\/1853"}],"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=1853"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1853\/revisions"}],"predecessor-version":[{"id":2866,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1853\/revisions\/2866"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1853"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1853"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1853"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}