{"id":1865,"date":"2012-02-02T19:11:20","date_gmt":"2012-02-02T19:11:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1865"},"modified":"2013-03-08T05:48:55","modified_gmt":"2013-03-08T05:48:55","slug":"ra2011-el-lenguaje-de-demostracion-isar","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2011-el-lenguaje-de-demostracion-isar\/","title":{"rendered":"RA2011: El lenguaje de demostraci\u00f3n Isar"},"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 el lenguaje de demostraci\u00f3n de  <http=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\/\">Isabelle<\/a>: Isar.<\/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 7: El lenguaje de demostraci\u00f3n Isar *}\r\n\r\ntheory Tema_7\r\nimports Main\r\nbegin\r\n\r\ntext {*\r\n  Este tema describe los elementos b\u00e1sicos del lenguaje de demostraci\u00f3n\r\n  Isar (Intelligible semi-automated reasoning).\r\n*}\r\n\r\nsection {* Panorama de la sintaxis (simplificada) de Isar *}\r\n\r\ntext {* \r\n  Representaci\u00f3n de lemas (y teoremas)\r\n  \u00b7 Un lema (o teorema) comienza con una etiqueta seguida por algunas\r\n    premisas y una conclusi\u00f3n.\r\n  \u00b7 Las premisas se introducen con la palabra \"assumes\" y se separan\r\n    con \"and\".\r\n  \u00b7 Cada premisa puede etiquetarse para referenciarse en la demostraci\u00f3n.\r\n  \u00b7 La conclusi\u00f3n se introduce con la palabra \"shows\".\r\n\r\n  Gram\u00e1tica (simplificada) de las demostraciones en Isar\r\n  <demostraci\u00f3n> ::= proof <m\u00e9todo> <declaraci\u00f3n>* qed\r\n                   | by <m\u00e9todo>\r\n  <declaraci\u00f3n>  ::= fix <variable>+ \r\n                   | assume <proposici\u00f3n>+\r\n                   | (from <hecho>+)? have <proposici\u00f3n>+ <demostraci\u00f3n>\r\n                   | (from <hecho>+)? show <proposici\u00f3n>+ <demostraci\u00f3n>\r\n  <proposici\u00f3n>  ::= (<etiqueta>:)? <cadena>\r\n  hecho          ::= <etiqueta>\r\n  m\u00e9todo         ::= -\r\n                   | this\r\n                   | rule <hecho>\r\n                   | simp \r\n                   | blast\r\n                   | auto\r\n                   | induct <variable>\r\n\r\n  La declaraci\u00f3n \"show\" demuestra la conclusi\u00f3n de la demostraci\u00f3n\r\n  mientras que la declaraci\u00f3n \"have\" demuestra un resultado intermedio.\r\n*}\r\n\r\nsection {* Razonamiento proposicional *}\r\n\r\ntext {* \r\n  Regla de introducci\u00f3n de la conjunci\u00f3n:\r\n  \u00b7 conjI: \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\r\n\r\n  Nota: Se puede consultar mediante\r\n     thm conjI     \r\n\r\n  Lema. [Ejemplo de introducci\u00f3n de conjunci\u00f3n con razonamiento progresivo] \r\n    P, Q \u22a2 P \u2227 (Q \u2227 P)  \r\n\r\n  Demostraci\u00f3n. Estamos suponiendo\r\n     P                                     (1)\r\n  y\r\n     Q                                     (2)\r\n  De (2) y (1), por introducci\u00f3n de la conjunci\u00f3n, se tiene\r\n     Q \u2227 P                                 (3)\r\n  De (1) y (3), por introducci\u00f3n de la conjunci\u00f3n, se tiene\r\n     P \u2227 (Q \u2227 P)\r\n*}\r\n\r\nlemma conj2: \r\n  assumes 1: P and 2: \"Q\" \r\n  shows \"P \u2227 (Q \u2227 P)\"\r\nproof -\r\n  from 2 1 have 3: \"Q \u2227 P\" by (rule conjI)\r\n  from 1 3 show \"P \u2227 (Q \u2227 P)\" by (rule conjI)\r\nqed\r\n\r\ntext {* \r\n  Razonamiento progresivo y regresivo en Isabelle:\r\n  \u00b7 Isabelle soporta razonamiento progresivo. La anterior demostraci\u00f3n\r\n    es una muestra. \r\n  \u00b7 Isabelle soporta razonamiento regresivo. La siguiente demostraci\u00f3n\r\n    es una muestra. \r\n\r\n  Lema. [Ejemplo de introducci\u00f3n de la conjunci\u00f3n con razonamiento regresivo] \r\n     P, Q \u22a2 P \u2227 (Q \u2227 P)\r\n\r\n  Demostraci\u00f3n. Estamos suponiendo\r\n     P                                    (1)\r\n  y\r\n     Q                                    (2)\r\n\r\n  Para demostrar el lema, por introducci\u00f3n de la conjunci\u00f3n, basta probar\r\n     P\r\n  y\r\n     Q \u2227 P                                (3)\r\n\r\n  La condici\u00f3n 'P' se tiene por la hip\u00f3tesis (1). Para demostrar\r\n  la condici\u00f3n (3), por introducci\u00f3n de la conjunci\u00f3n, basta probar\r\n     Q                                     \r\n  y\r\n     P\r\n  La condici\u00f3n 'Q' se tiene por la hip\u00f3tesis (2) y la condici\u00f3n 'P' se\r\n  tiene por la hip\u00f3tesis (1).\r\n*}\r\n\r\nlemma \r\n  assumes 1: \"P\" and 2: \"Q\" \r\n  shows \"P \u2227 (Q \u2227 P)\"\r\nproof (rule conjI)\r\n  from 1 show \"P\" by this\r\nnext\r\n  show \"Q \u2227 P\"\r\n  proof (rule conjI)\r\n    from 2 show \"Q\" by this\r\n  next\r\n    from 1 show \"P\" by this\r\n  qed\r\nqed\r\n\r\ntext {* \r\n  El m\u00e9todo \"this\" demuestra el objetivo usando el hecho actual; es\r\n  decir, el de la cl\u00e1usula \"from\".  \r\n\r\n  Reglas de eliminaci\u00f3n de la conjunci\u00f3n:\r\n  \u00b7 conjunct1: P \u2227 Q \u27f9 P\r\n  \u00b7 conjunct2: P \u2227 Q \u27f9 Q\r\n\r\n  Regla de introducci\u00f3n de la implicaci\u00f3n:\r\n  \u00b7 impI: (P \u27f9 Q) \u27f9 P \u27f6 Q\r\n\r\n  Lema. [Ejemplo de razonamiento h\u00edbrido]\r\n  Sean a y b dos n\u00fameros naturales. Si 0 < a y a < b, entonces a*a < b*b.    \r\n*}\r\n\r\nlemma\r\n  fixes a b :: \"nat\"\r\n  shows \"0 < a \u2227 a < b \u27f6 a * a < b * b\"\r\nproof (rule impI)\r\n  assume x: \"0 < a \u2227 a < b\"\r\n  from x have za: \"0 < a\" by (rule conjunct1)\r\n  from x have ab: \"a < b\" by (rule conjunct2)\r\n  from za ab have aa: \"a*a < a*b\" by simp\r\n  from ab have bb: \"a*b < b*b\" by simp\r\n  from aa bb show \"a*a < b*b\" by arith\r\nqed\r\n\r\ntext {* \r\n  Modus ponens:\r\n  \u00b7 mp: \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q\r\n\r\n  Reglas de introducci\u00f3n de la disyunci\u00f3n:\r\n  \u00b7 disjI1: P \u27f9 P \u2228 Q\r\n  \u00b7 disjI2: Q \u27f9 P \u2228 Q\r\n\r\n  Regla de eliminaci\u00f3n de la disyunci\u00f3n:\r\n  . disjE: \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R\r\n\r\n  Lema. [Razonamiento por casos] \r\n     A \u2228 B, A \u27f6 C, B \u27f6 C \u22a2 C\r\n*}\r\n\r\nlemma \r\n  assumes ab: \"A \u2228 B\" and ac: \"A \u27f6 C\" and bc: \"B \u27f6 C\"\r\n  shows \"C\"\r\nproof -\r\n  note ab\r\n  moreover { \r\n    assume a: \"A\" \r\n    from ac a have \"C\" by (rule mp) } \r\n  moreover { \r\n    assume b: \"B\" \r\n    from bc b have \"C\" by (rule mp) }\r\n  ultimately show \"C\" by (rule disjE)\r\nqed\r\n\r\ntext {* \r\n  Resumen de reglas proposicionales:\r\n  \u00b7 TrueI:         True\r\n  \u00b7 FalseE:        False \u27f9 P\r\n  \u00b7 conjI:         \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\r\n  \u00b7 conjunct1:     P \u2227 Q \u27f9 P\r\n  \u00b7 conjunct2:     P \u2227 Q \u27f9 Q\r\n  \u00b7 conjE:         \u27e6P \u2227 Q; \u27e6P; Q\u27e7 \u27f9 R\u27e7 \u27f9 R\r\n  \u00b7 disjI1:        P \u27f9 P \u2228 Q\r\n  \u00b7 disjI2:        Q \u27f9 P \u2228 Q\r\n  \u00b7 disjE:         \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R\r\n  \u00b7 notI:          (P \u27f9 False) \u27f9 \u00acP\r\n  \u00b7 notE:          \u27e6\u00acP; P\u27e7 \u27f9 R\r\n  \u00b7 impI:          (P \u27f9 Q) \u27f9 P \u27f6 Q\r\n  \u00b7 impE:          \u27e6P \u27f6 Q; P; Q \u27f9 R\u27e7 \u27f9 R\r\n  \u00b7 mp:            \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q\r\n  \u00b7 iff:           (P \u27f6 Q) \u27f6 (Q \u27f6 P) \u27f6 P = Q\r\n  \u00b7 iffI:          \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P = Q\r\n  \u00b7 iffD1:         \u27e6Q = P; Q\u27e7 \u27f9 P\r\n  \u00b7 iffD2:         \u27e6P = Q; Q\u27e7 \u27f9 P\r\n  \u00b7 iffE:          \u27e6P = Q; \u27e6P \u27f6 Q; Q \u27f6 P\u27e7 \u27f9 R\u27e7 \u27f9 R\r\n  \u00b7 ccontr:        (\u00acP \u27f9 False) \u27f9 P\r\n  \u00b7 classical:     (\u00acP \u27f9 P) \u27f9 P      \r\n  \u00b7 exlude_middle: \u00acP \u2228 P\r\n  \u00b7 disjCI:        (\u00acQ \u27f9 P) \u27f9 P \u2228 Q\r\n  \u00b7 impCE:         \u27e6P \u27f6 Q; \u00acP \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R\r\n  \u00b7 iffCE:         \u27e6P = Q; \u27e6P; Q\u27e7 \u27f9 R; \u27e6\u00acP; \u00acQ\u27e7 \u27f9 R\u27e7 \u27f9 R\r\n  \u00b7 notnotD:       \u00ac\u00acP \u27f9 P\r\n  \u00b7 swap:          \u27e6\u00acP; \u00acR \u27f9 P\u27e7 \u27f9 R\r\n\r\n  Referencia de reglas de inferencia: M\u00e1s informaci\u00f3n sobre las reglas\r\n  de inferencia se encuentra en la secci\u00f3n  2.2 de \"Isabelle's Logics:\r\n  HOL\".\r\n*}\r\n\r\nsection {* Atajos de Isar *}\r\n\r\ntext {*\r\n  Isar tiene muchos atajos, como los siguientes:\r\n  this        | \u00e9ste           | el hecho probado en la declaraci\u00f3n anterior\r\n  then        | entonces       | from this\r\n  hence       | por lo tanto   | then have\r\n  thus        | de esta manera | then show\r\n  with hecho+ | con            | from hecho+ and this\r\n  .           | por \u00e9sto       | by this\r\n  ..          | trivialmente   | by regla (Isabelle adivina la regla)\r\n\r\n  Razonamiento acumulativo:\r\n  Una sucesi\u00f3n de hechos que se van a usar como premisa en una declaraci\u00f3n\r\n  puede agruparse usando \"moreover\" (adem\u00e1s) y usarse en la declaraci\u00f3n\r\n  usando \"ultimately\" (finalmente). \r\n\r\n  Lema. [Ejemplo de uso de atajos y razonamiento acumulativo]\r\n     A \u2227 B \u22a2 B \u2227 A.\r\n*}\r\n\r\nlemma \"A \u2227 B \u27f6 B \u2227 A\"\r\nproof (rule impI)\r\n  assume ab: \"A \u2227 B\"\r\n  hence \"B\" by (rule conjunct2)\r\n  moreover from ab have \"A\" ..\r\n  ultimately show \"B \u2227 A\" by (rule conjI)\r\nqed\r\n\r\nsection {* Cuantificadores universal y existencial *}\r\n\r\nthm allE\r\ntext {* \r\n  Reglas del cuantificador universal:\r\n  \u00b7 allI: (\u22c0x. P x) \u27f9 \u2200x. P x\r\n  \u00b7 allE: \u27e6\u2200x. P x; P x \u27f9 R\u27e7 \u27f9 R\r\n  En la regla allI la nueva variable se introduce mediante la palabra \"fix\".\r\n\r\n  Lema. [Ejemplo con  cuantificadores universales]\r\n     \u2200x. P \u27f6 Q x \u22a2 P \u27f6 (\u2200x. Q x)\r\n*}\r\n\r\nlemma\r\n  assumes a: \"\u2200 x. P \u27f6 Q x\"\r\n  shows \"P \u27f6 (\u2200 x. Q x)\"\r\nproof (rule impI)\r\n  assume p: \"P\"\r\n  show \"\u2200 x. Q x\"\r\n  proof (rule allI)\r\n    fix y\r\n    from a have pq: \"P \u27f6 Q y\" by (rule allE)\r\n    from pq p show \"Q y\" by (rule mp)\r\n  qed\r\nqed\r\n\r\ntext {* \r\n  Reglas del cuantificador existencial:\r\n  \u00b7 exI: P x \u27f9 \u2203x. P x\r\n  \u00b7 exE: \u27e6\u2203x. P x; \u22c0x. P x \u27f9 Q\u27e7 \u27f9 Q\r\n  En la regla exE la nueva variable se introduce mediante la declaraci\u00f3n \r\n  \"obtain ... where ... by (rule exE)\" \r\n\r\n  Lema. [Ejemplo con cuantificador existencial y demostraci\u00f3n progresiva]\r\n     \u2203x. P \u2227 Q(x) \u22a2 P \u2227 (\u2203x. Q(x))\r\n*}\r\n\r\nlemma\r\n  assumes e: \"\u2203 x. P \u2227 Q(x)\"\r\n  shows \"P \u2227 (\u2203 x. Q(x))\"\r\nproof -\r\n  from e obtain y where f: \"P \u2227 Q(y)\" by (rule exE) \r\n  from f have p: \"P\" by (rule conjunct1)\r\n  from f have q: \"Q(y)\" by (rule conjunct2)\r\n  from q have eq: \"\u2203 x. Q(x)\" by (rule exI)\r\n  from p eq show \"P \u2227 (\u2203 x. Q(x))\" by (rule conjI)\r\nqed\r\n\r\ntext {* \r\n  Lema. [Ejemplo con cuantificador existencial y demostraci\u00f3n autom\u00e1tica] \r\n     \u2203x. P \u2227 Q(x) \u22a2 P \u2227 (\u2203x. Q(x))\r\n*}\r\n\r\nlemma\r\n  assumes e: \"\u2203 x. P \u2227 Q(x)\"\r\n  shows \"P \u2227 (\u2203 x. Q(x))\"\r\nproof -\r\n  from e obtain y where f: \"P \u2227 Q(y)\" ..\r\n  from f have p: \"P\" ..\r\n  from f have q: \"Q(y)\" ..\r\n  from q have eq: \"\u2203x. Q(x)\" ..\r\n  from p eq show \"P \u2227 (\u2203x. Q(x))\" ..\r\nqed\r\n\r\ntext {* \r\n  Lema. [Ejemplo con cuantificador existencial y demostraci\u00f3n regresiva]\r\n     \u2203x. P \u2227 Q(x) \u22a2 P \u2227 (\u2203x. Q(x))\"\r\n*}\r\n\r\nlemma\r\n  assumes e: \"\u2203x. P \u2227 Q(x)\"\r\n  shows \"P \u2227 (\u2203x. Q(x))\"\r\nproof (rule conjI)\r\n  show \"P\"\r\n    proof -\r\n    from e obtain y where p: \"P \u2227 Q(y)\" by (rule exE)\r\n    from p show \"P\" by (rule conjunct1)\r\n    qed\r\n  show \"\u2203x. Q(x)\"\r\n    proof -\r\n    from e obtain y where p: \"P \u2227 Q(y)\" by (rule exE)\r\n    from p have q: \"Q(y)\" by (rule conjunct2)\r\n    from q show \"\u2203x. Q(x)\" by (rule exI)\r\n    qed\r\nqed\r\n\r\ntext {* \r\n  Definici\u00f3n. [Ejemplo de definici\u00f3n existencial]\r\n  El n\u00famero natural x divide al n\u00famero natural y si existe un natural k\r\n  tal que k\u00d7x = y. Se representa por x | y. \r\n*}\r\n\r\ndefinition divide :: \"nat \u21d2 nat \u21d2 bool\" (\"_ | _\" [80,80] 80) where\r\n  \"x | y \u2261 \u2203k. k*x = y\"\r\n\r\ntext {* \r\n  Ejemplo de activaci\u00f3n autom\u00e1tica de regla de simplificaci\u00f3n:\r\n  La definici\u00f3n de divide se a\u00f1ade a las reglas de simplificaci\u00f3n. \r\n*}\r\n\r\ndeclare divide_def[simp]\r\n\r\ntext {* \r\n  Lema. [Transitividad de la divisibilidad]\r\n  Sean a, b y c n\u00fameros naturales. Si b es divisible por a y c es\r\n  divisible por b, entonces c es divisible por a. \r\n*}\r\n\r\nlemma divide_trans: \r\n  fixes a b c :: \"nat\"\r\n  assumes ab: \"a | b\" and bc: \"b | c\"\r\n  shows \"a | c\"\r\nproof simp\r\n  from ab obtain m where m: \"m*a = b\" by auto\r\n  from bc obtain n where n: \"n*b = c\" by auto\r\n  from m n have \"m*n*a = c\" by auto\r\n  thus \"\u2203k. k*a = c\" by (rule exI)\r\nqed\r\n\r\ntext {* \r\n  M\u00e9todo auto: En el lema anterior es la primera vez que se usa el\r\n  m\u00e9todo autom\u00e1tico \"auto\".\r\n\r\n  Lema. [CNS de divisibilidad]\r\n  Sean a y b dos n\u00fameros naturales. Entonces a es divisible por b syss\r\n  el resto de dividir a entre b es cero.  \r\n*}\r\n\r\nlemma CNS_divisibilidad: \r\n  \"(a | b) = (b mod a = 0)\" \r\nby auto\r\n\r\nsection {* Razonamiento ecuacional *}\r\n\r\ntext {* \r\n  Elementos para el razonamiento ecuacional:\r\n  El razonamiento ecuacional se realiza de manera m\u00e1s concisa usando la\r\n  combinaci\u00f3n de \"also\" (adem\u00e1s) y \"finally\" (finalmente).\r\n  \r\n  Lema. [Ejemplo de razonamiento ecuacional]\r\n  Si a=b, b=c y c=d, entonces a=d.  \r\n*}\r\n\r\nlemma \r\n  assumes 1: \"a = b\" and 2: \"b = c\" and 3: \"c = d\"\r\n  shows \"a = d\"\r\nproof -\r\n  have \"a = b\" by (rule 1)\r\n  also have \"\u2026 = c\" by (rule 2)\r\n  also have \"\u2026 = d\" by (rule 3)\r\n  finally show \"a = d\" .\r\nqed\r\n\r\ntext {* \r\n  El lema anterior puede demostrarse autom\u00e1ticamente con la maza\r\n  (\"sledgehammer\"). \r\n*}\r\n\r\nlemma \r\n  assumes 1: \"a = b\" and 2: \"b = c\" and 3: \"c = d\"\r\n  shows \"a = d\"\r\nproof -\r\n  show \"a=d\" by (metis 1 2 3)\r\nqed\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 el lenguaje de demostraci\u00f3n de Isabelle: Isar. 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\/1865"}],"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=1865"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1865\/revisions"}],"predecessor-version":[{"id":2861,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1865\/revisions\/2861"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1865"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1865"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1865"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}