{"id":1868,"date":"2012-02-08T20:56:31","date_gmt":"2012-02-08T20:56:31","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1868"},"modified":"2013-03-08T05:48:55","modified_gmt":"2013-03-08T05:48:55","slug":"ra2011-patrones-de-induccion-en-isabelle-casos-induccion-y-otros","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2011-patrones-de-induccion-en-isabelle-casos-induccion-y-otros\/","title":{"rendered":"RA2011: Patrones de inducci\u00f3n en Isabelle: casos, inducci\u00f3n y otros"},"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 han presentado los principales patrones de inducci\u00f3n en <http=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\/\">Isabelle<\/a>: en la primera parte se ha presentado los patrones de de mostraci\u00f3n por casos y por inducci\u00f3n y en la segunda parte se han presentado otros patrones (eliminaci\u00f3n de disyunci\u00f3n, negaci\u00f3n, contradicci\u00f3n y equivalencias).<\/p>\n<p>La primera parte de la clase se ha basado en la siguiente teor\u00eda Isabelle<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 8: Distinci\u00f3n de casos e inducci\u00f3n *}\r\n\r\ntheory Tema_8\r\nimports Main Parity\r\nbegin\r\n\r\nsection {* Razonamiento por distinci\u00f3n de casos *}\r\n\r\nsubsection {* Distinci\u00f3n de casos booleanos *}\r\n\r\ntext {*\r\n  Lema. [Demostraci\u00f3n por distinci\u00f3n de casos booleanos]\r\n     \u00acA \u2228 A\r\n*}\r\n\r\nlemma \"\u00acA \u2228 A\" \r\nproof cases\r\n  assume \"A\" thus ?thesis ..\r\nnext\r\n  assume \"\u00acA\" thus ?thesis ..\r\nqed\r\n\r\ntext {*\r\n  Lema. [Demostraci\u00f3n por distinci\u00f3n de casos booleanos nominados]\r\n     \u00acA \u2228 A\r\n*}\r\n\r\nlemma \"\u00acA \u2228 A\" \r\nproof (cases \"A\")\r\n  case True thus ?thesis ..\r\nnext\r\n  case False thus ?thesis .. \r\nqed\r\n\r\ntext {*\r\n  El m\u00e9todo \"cases\" sobre una f\u00f3rmula:\r\n  \u00b7 El m\u00e9todo (cases F) es una abreviatura de la aplicaci\u00f3n de la regla\r\n       \u27e6F \u27f9 Q; \u00acF \u27f9 Q\u27e7 \u27f9 Q  \r\n  \u00b7 La expresi\u00f3n \"case True\" es una abreviatura de F.\r\n  \u00b7 La expresi\u00f3n \"case False\" es una abreviatura de \u00acF.\r\n  \u00b7 Ventajas de \"cases\" con nombre: \r\n    \u00b7 reduce la escritura de la f\u00f3rmula y\r\n    \u00b7 es independiente del orden de los casos.\r\n*}\r\n\r\nsubsection {* Distinci\u00f3n de casos sobre otros tipos de datos *}\r\n\r\ntext {*\r\n  Lema. [Distinci\u00f3n de casos sobre listas]\r\n  La longitud del resto de una lista es la longitud de la lista menos 1.\r\n*}\r\n\r\nlemma \"length(tl xs) = length xs - 1\" \r\nproof (cases xs)\r\n  case Nil thus ?thesis by simp\r\nnext\r\n  case Cons thus ?thesis by simp \r\nqed\r\n\r\ntext {*\r\n  Distinci\u00f3n de casos sobre listas:\r\n  \u00b7 El m\u00e9todo de distinci\u00f3n de casos se activa con (cases xs) donde xs\r\n    es del tipo lista. \r\n  \u00b7 \"case Nil\" es una abreviatura de \r\n       \"assume Nil: xs =[]\".\r\n  \u00b7 \"case Cons\" es una abreviatura de \r\n       \"fix ? ?? assume Cons: xs = ? # ??\"\r\n    donde ? y ?? son variables an\u00f3nimas. \r\n\r\n  Lema. [Ejemplo de an\u00e1lisis de casos]\r\n  El resultado de eliminar los n+1 primeros elementos de xs es el mismo\r\n  que eliminar los n primeros elementos del resto de xs.  \r\n*}\r\n\r\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\r\nproof (cases xs)\r\n  case Nil thus \"drop (n + 1) xs = drop n (tl xs)\" by simp\r\nnext\r\n  case Cons thus \"drop (n + 1) xs = drop n (tl xs)\" by simp\r\nqed\r\n\r\ntext {*\r\n  La funci\u00f3n drop est\u00e1 definida en la teor\u00eda List de forma que\r\n  (drop n xs) la lista obtenida eliminando en xs} los n primeros\r\n  elementos. Su definici\u00f3n es la siguiente  \r\n     primrec drop:: \"nat => 'a list => 'a list\" where\r\n     drop_Nil:  \"drop n [] = []\" |\r\n     drop_Cons: \"drop n (x#xs) = (case n of \r\n                                    0 => x#xs | \r\n                                    Suc(m) => drop m xs)\"\r\n*}\r\n\r\nsection {* Inducci\u00f3n matem\u00e1tica *}\r\nthm nat.induct\r\ntext {*\r\n  [Principio de inducci\u00f3n matem\u00e1tica]\r\n  Para demostrar una propiedad P para todos los n\u00fameros naturales basta\r\n  probar que el 0 tiene la propiedad P y que si n tiene la propiedad P,\r\n  entonces n+1 tambi\u00e9n la tiene. \r\n     \u27e6P 0; \u22c0n. P n \u27f9 P (Suc n)\u27e7 \u27f9 P m\r\n  \r\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n: Usaremos el principio de\r\n  inducci\u00f3n matem\u00e1tica para demostrar que \r\n     1 + 3 + ... + (2n-1) = n^2\r\n\r\n  Definici\u00f3n. [Suma de los primeros impares] \r\n  (suma_impares n) la suma de los n n\u00fameros impares.    \r\n*}\r\n\r\nprimrec suma_impares :: \"nat \u21d2 nat\" where\r\n\"suma_impares 0 = 0\" |\r\n\"suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n\"\r\n\r\ntext {* \r\n  Lema. [Ejemplo de suma de impares]\r\n  La suma de los 3 primeros n\u00fameros impares es 9.\r\n*}\r\n\r\nlemma \"suma_impares 2 = 4\"\r\nby (simp add: suma_impares_def)\r\n\r\ntext {*\r\n  La suma de los 3 primero n\u00famero impares se puede calcular mediante \"value\". \r\n*}\r\n\r\nvalue \"suma_impares 3\"\r\n\r\ntext {*\r\n  Lema. [Ejemplo de demostraci\u00f3n por inducci\u00f3n matem\u00e1tica]\r\n  La suma de los n primeros n\u00fameros impares es n^2.\r\n  \r\n  Demostraci\u00f3n autom\u00e1tica: Por inducci\u00f3n en n.\r\n*}\r\n\r\nlemma \"suma_impares n = n * n\"\r\nby (induct n) simp_all\r\n\r\ntext {*\r\n  En la demostraci\u00f3n \"by (induct n) simp_all\" se aplica inducci\u00f3n en n y\r\n  los dos casos se prueban por simplificaci\u00f3n.  \r\n  \r\n  Demostraci\u00f3n del lema anterior usando patrones.\r\n*}\r\n\r\nlemma \"suma_impares n = n * n\" (is \"?P n\")\r\nproof (induct n)\r\n  show \"?P 0\" by simp\r\nnext\r\n  fix n assume \"?P n\"\r\n  thus \"?P (Suc n)\" by simp\r\nqed\r\n\r\ntext {*\r\n  Patrones: Cualquier f\u00f3rmula seguida de (is patr\u00f3n) equipara el patr\u00f3n\r\n  con la f\u00f3rmula.\r\n\r\n  Demostraci\u00f3n del lema anterior con patrones y razonamiento ecuacional.\r\n*}\r\n\r\nlemma \"suma_impares n = n * n\" (is \"?P n\")\r\nproof (induct n)\r\n  show \"?P 0\" by simp\r\nnext\r\n  fix n assume HI: \"?P n\"\r\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" by simp\r\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\r\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\r\n  finally show \"?P (Suc n)\" by simp\r\nqed\r\n\r\ntext {*\r\n  Demostraci\u00f3n del lema anterior por inducci\u00f3n y razonamiento ecuacional.\r\n*}\r\n\r\nlemma \"suma_impares n = n * n\"\r\nproof (induct n)\r\n  show \"suma_impares 0 = 0 * 0\" by simp\r\nnext\r\n  fix n assume HI: \"suma_impares n = n * n\"\r\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" by simp\r\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\r\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\r\n  finally show \"suma_impares (Suc n) = (Suc n) * (Suc n)\" by simp\r\nqed\r\n\r\ntext {* \r\n  Definici\u00f3n. [N\u00fameros pares]\r\n  Un n\u00famero natural n es par si existe un natural m tal que n=m+m. \r\n*}\r\n\r\ndefinition par ::  \"nat \u21d2 bool\" where\r\n  \"par n \u2261 \u2203m. n=m+m\"\r\n\r\ntext {* \r\n  Lema. [Ejemplo de inducci\u00f3n y existenciales]\r\n  Para todo n\u00famero natural n, se verifica que n*(n+1) par.\r\n*}\r\n\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"par (n*(n+1))\"\r\nproof (induct n)\r\n  show \"par (0*(0+1))\" by (simp add:par_def)\r\nnext\r\n  fix n assume \"par (n*(n+1))\"\r\n  hence \"\u2203m. n*(n+1) = m+m\" by (simp add:par_def)\r\n  then obtain m where m: \"n*(n+1) = m+m\" by (rule exE)\r\n  hence \"(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)\" by auto\r\n  hence \"\u2203m. (Suc n)*((Suc n)+1) = m+m\" by (rule exI)\r\n  thus \"par ((Suc n)*((Suc n)+1))\" by (simp add:par_def)\r\nqed\r\n\r\ntext {*\r\n  En Isabelle puede demostrarse de manera m\u00e1s simple un lema equivalente usando\r\n  en lugar de la funci\u00f3n \"par\" la funci\u00f3n \"even\" definida en la teor\u00eda Parity.\r\n*}\r\n\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"even (n*(n+1))\"\r\nby auto\r\n\r\ntext {*\r\n  Para completar la demostraci\u00f3n basta demostrar la equivalencia de las\r\n  funciones \"par\" y \"even\". \r\n*}\r\n\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"par n = even n\"\r\nproof - \r\n  have \"par n = (\u2203m. n = m+m)\" by (simp add:par_def)\r\n  thus \"par n = even n\" by presburger\r\nqed\r\n\r\ntext {*\r\n  En la demostraci\u00f3n anterior hemos usado la t\u00e1ctica \"presburger\" que\r\n  corresponde a la aritm\u00e9tica de Presburger.\r\n*}\r\n\r\nsection {* Inducci\u00f3n estructural *}\r\n\r\nthm list.induct\r\n\r\ntext {*\r\n  Inducci\u00f3n estructural]\r\n  \u00b7 En Isabelle puede hacerse inducci\u00f3n estructural sobre cualquier tipo\r\n    recursivo.\r\n  \u00b7 La inducci\u00f3n matem\u00e1tica es la inducci\u00f3n estructural sobre el tipo de\r\n    los naturales.\r\n  \u00b7 El esquema de inducci\u00f3n estructural sobre listas es\r\n    \u00b7 list.induct: \u27e6P []; \u22c0x ys. P ys \u27f9 P (x # ys)\u27e7 \u27f9 P zs\r\n  \u00b7 Para demostrar una propiedad para todas las listas basta demostrar\r\n    que la lista vac\u00eda tiene la propiedad y que al a\u00f1adir un elemento a una\r\n    lista que tiene la propiedad se obtiene una lista que tambi\u00e9n tiene la\r\n    propiedad. \r\n\r\n  Concatenaci\u00f3n de listas:\r\n  En la teor\u00eda List.thy est\u00e1 definida la concatenaci\u00f3n de listas (que\r\n  se representa por @) como sigue\r\n    primrec\r\n      append_Nil:  \"[]@ys = ys\"\r\n      append_Cons: \"(x#xs)@ys = x#(xs@ys)\"\r\n\r\n  Lema. [Ejemplo de inducci\u00f3n sobre listas]\r\n  La concatenaci\u00f3n de listas es asociativa.\r\n  \r\n  Demostraci\u00f3n autom\u00e1tica del lema.\r\n*}\r\n\r\nlemma conc_asociativa_1: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\nby (induct xs) simp_all\r\n\r\ntext {*\r\n  Demostraci\u00f3n estructurada del lema anterior.\r\n*}\r\n\r\nlemma conc_asociativa: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\nproof (induct xs)\r\n  show \"[] @ (ys @ zs) = ([] @ ys) @ zs\"\r\n  proof -\r\n    have \"[] @ (ys @ zs) = ys @ zs\" by simp\r\n    also have \"\u2026 = ([] @ ys) @ zs\" by simp\r\n    finally show ?thesis .\r\n  qed\r\nnext\r\n  fix x xs\r\n  assume HI: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\n  show \"(x#xs) @ (ys @ zs) = ((x#xs) @ ys) @ zs\"\r\n  proof -\r\n    have \"(x#xs) @ (ys @ zs) = x#(xs @ (ys @ zs))\" by simp\r\n    also have \"\u2026 = x#((xs @ ys) @ zs)\" using HI by simp\r\n    also have \"\u2026 = (x#(xs @ ys)) @ zs\" by simp\r\n    also have \"\u2026 = ((x#xs) @ ys) @ zs\" by simp\r\n    finally show ?thesis .\r\n  qed\r\nqed\r\n\r\ntext {* \r\n  Ejercicio. [\u00c1rboles binarios]\r\n  Definir un tipo de dato para los \u00e1rboles binarios.\r\n*}\r\n\r\ndatatype 'a arbol = Hoja \"'a\" \r\n                  | Nodo \"'a\" \"'a arbol\" \"'a arbol\"\r\n\r\ntext {* \r\n  Ejercicio. [Imagen especular]\r\n  Definir la funci\u00f3n \"espejo\" que aplicada a un \u00e1rbol devuelve su imagen\r\n  especular.  \r\n*}\r\n\r\nprimrec espejo :: \"'a arbol \u21d2 'a arbol\" where\r\n  \"espejo (Hoja a) = (Hoja a)\"\r\n| \"espejo (Nodo f x y) = (Nodo f (espejo y) (espejo x))\"\r\n\r\ntext {* \r\n  Ejercicio. [La imagen especular es involutiva]\r\n  Demostrar que la funci\u00f3n \"espejo\" involutiva; es decir, para cualquier\r\n  \u00e1rbol t, se tiene que \r\n     espejo (espejo(t)) = t.\r\n  \r\n  Demostraci\u00f3n autom\u00e1tica del lema.\r\n*}\r\n\r\nlemma espejo_involutiva_1: \"espejo(espejo(t)) = t\"\r\nby (induct t) auto\r\n\r\ntext {*\r\n  Demostraci\u00f3n estructurada del lema.\r\n*}\r\n\r\nlemma espejo_involutiva: \"espejo(espejo(t)) = t\" (is \"?P t\")\r\nproof (induct t)\r\n  fix x :: 'a show \"?P (Hoja x)\" by simp \r\nnext\r\n  fix t1 :: \"'a arbol\" assume h1: \"?P t1\"\r\n  fix t2 :: \"'a arbol\" assume h2: \"?P t2\"\r\n  fix x :: 'a\r\n  show \"?P (Nodo x t1 t2)\" \r\n  proof -\r\n    have \"espejo(espejo(Nodo x t1 t2)) = espejo(Nodo x (espejo t2) (espejo t1))\"\r\n      by simp\r\n    also have \"\u2026 = Nodo x (espejo (espejo t1)) (espejo (espejo t2))\" by simp\r\n    also have \"\u2026 = Nodo x t1 t2\" using h1 h2 by simp \r\n    finally show ?thesis .\r\n qed\r\nqed\r\n\r\ntext {* \r\n  Ejercicio. [Aplanamiento de \u00e1rboles]\r\n  Definir la funci\u00f3n \"aplana\" que aplane los \u00e1rboles recorri\u00e9ndolos en\r\n  orden infijo.  \r\n*}\r\n\r\nprimrec aplana :: \"'a arbol \u21d2 'a list\" where\r\n  \"aplana (Hoja a) = [a]\"\r\n| \"aplana (Nodo x t1 t2) = (aplana t1)@[x]@(aplana t2)\"\r\n\r\ntext {* \r\n  Ejercicio. [Aplanamiento de la imagen especular] Demostrar que\r\n     aplana (espejo t) = rev (aplana t)\r\n  \r\n  Demostraci\u00f3n autom\u00e1tica del lema.\r\n*}\r\n\r\nlemma \"aplana (espejo t) = rev (aplana t)\"\r\nby (induct t) auto\r\n\r\ntext {* \r\n  Demostraci\u00f3n estructurada del lema anterior.\r\n*}\r\n\r\nlemma \"aplana (espejo t) = rev (aplana t)\" (is \"?P t\")\r\nproof (induct t)\r\n  fix x :: 'a \r\n  show \"?P (Hoja x)\" by simp \r\nnext\r\n  fix t1 :: \"'a arbol\" assume h1: \"?P t1\"\r\n  fix t2 :: \"'a arbol\" assume h2: \"?P t2\"\r\n  fix x :: 'a\r\n  show \"?P (Nodo x t1 t2)\" \r\n  proof -\r\n    have \"aplana (espejo (Nodo x t1 t2)) = \r\n          aplana (Nodo x (espejo t2) (espejo t1))\" by simp\r\n    also have \"\u2026 = (aplana(espejo t2))@[x]@(aplana(espejo t1))\" by simp\r\n    also have \"\u2026 = (rev(aplana t2))@[x]@(rev(aplana t1))\" using h1 h2 by simp\r\n    also have \"\u2026 = rev((aplana t1)@[x]@(aplana t2))\" by simp\r\n    also have \"\u2026 = rev(aplana (Nodo x t1 t2))\" by simp\r\n    finally show ?thesis .\r\n qed\r\nqed\r\n\r\nend\r\n<\/pre>\n<p>La segunda parte de la clase se ha basado en la siguiente teor\u00eda Isabelle<\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 9: Patrones de demostraci\u00f3n *}\r\n\r\ntheory Tema_9\r\nimports Main\r\nbegin\r\n\r\nsection {* Demostraciones por casos *} \r\n\r\ntext {*\r\n  Nota. [Regla de eliminaci\u00f3n de la disyunci\u00f3n]\r\n  \u00b7 disjE: \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R\r\n\r\n  Lema. [Ejemplo de demostraci\u00f3n por casos]\r\n     P \u2228 Q \u27f9 Q \u2228 P\r\n*}\r\n\r\nlemma disj_conmutativa: \"P \u2228 Q \u27f9 Q \u2228 P\"\r\nproof -\r\n  assume \"P \u2228 Q\" \r\n  thus \"Q \u2228 P\" \r\n  proof (rule disjE) \r\n    assume P \r\n    thus ?thesis  by (rule disjI2)\r\n  next\r\n    assume Q \r\n    thus ?thesis by (rule disjI1) \r\n  qed \r\nqed \r\n\r\ntext {*\r\n  Nota. El lema anterior puede demostrarse autom\u00e1ticamente como se\r\n  muestra a continuaci\u00f3n. \r\n*}\r\n\r\nlemma disj_conmutativa_auto: \"P \u2228 Q \u27f9 Q \u2228 P\"\r\nby auto\r\n\r\nsection {* Negaci\u00f3n *}\r\n\r\ntext {*\r\n  Reglas de la negaci\u00f3n:\r\n  \u00b7 notI: (P \u27f9 False) \u27f9 \u00acP\r\n  \u00b7 notE: \u27e6\u00acP; P\u27e7 \u27f9 R\r\n\r\n  Lema. [Ejemplo de demostraci\u00f3n con negaciones]\r\n  Si x\\<^bsup>2\\<^esup>+y=13 e y \u2260 4, entonces x \u2260 3.\r\n*}\r\n\r\nlemma \r\n  fixes x :: \"nat\"\r\n  assumes 1: \"x * x + y = 13\" \r\n      and 2: \"y \u2260 4\"\r\n  shows \"x \u2260 3\"\r\nproof (rule notI)\r\n  assume \"x = 3\"\r\n  with 1 have \"y = 4\" by simp\r\n  with 2 show \"False\" by (rule notE)\r\nqed\r\n\r\ntext {*\r\n  La demostraci\u00f3n puede hacerse autom\u00e1ticamente como se muestra a\r\n  continuaci\u00f3n. \r\n*}\r\n\r\nlemma \r\n  fixes x :: \"nat\"\r\n  assumes 1: \"x * x + y = 13\" \r\n      and 2: \"y \u2260 4\"\r\n  shows \"x \u2260 3\"\r\nproof (rule notI)\r\n  assume \"x = 3\"\r\n  with 1 2 show \"False\" by auto\r\nqed\r\n\r\ntext {*\r\n  El lema anterior puede demostrarse m\u00e1s autom\u00e1ticamente como se muestra a\r\n  continuaci\u00f3n. \r\n*}\r\n\r\nlemma \r\n  fixes x :: \"nat\"\r\n  assumes 1: \"x * x + y = 13\" \r\n      and 2: \"y \u2260 4\"\r\n  shows \"x \u2260 3\"\r\nusing assms\r\nby auto\r\n\r\nsection {* Contradicciones *}\r\n\r\ntext {*\r\n  Regla de contradicci\u00f3n:\r\n  \u00b7 FalseE: False \u27f9 P\r\n\r\n  Lema. [Ejemplo de uso de la regla de contradicci\u00f3n]\r\n  Si 1=2, entonces 3=7.\r\n*}\r\n\r\nlemma \r\n  assumes \"1 = (2::nat)\"\r\n  shows \"3 = (7::nat)\"\r\nproof - \r\n  have \"False\" using assms by simp\r\n  thus \"3 = (7::nat)\" by (rule FalseE)\r\nqed\r\n\r\ntext {*\r\n  El lema puede demostrarse autom\u00e1ticamente, como sigue.\r\n*}\r\n\r\nlemma \r\n  assumes \"1 = (2::nat)\"\r\n  shows \"3 = (7::nat)\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Lema. [Ejemplo de demostraci\u00f3n por casos y contradicci\u00f3n]\r\n     \u00acP, P \u2228 Q \u22a2 Q\r\n*}\r\n\r\nlemma disjCE:\r\n  assumes \"\u00acP\" and \"P \u2228 Q\"\r\n  shows \"Q\"\r\nusing `P \u2228 Q`\r\nproof (rule disjE)\r\n  assume \"P\"\r\n  thus \"Q\" using `\u00acP` by contradiction\r\nnext\r\n  assume \"Q\"\r\n  thus \"Q\" by assumption\r\nqed\r\n\r\nsection {* Equivalencias *}\r\n\r\ntext {*\r\n  Reglas de equivalencia:\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\r\n  Lema. [Ejemplo de introducci\u00f3n de equivalencia]\r\n  La f\u00f3rmula \r\n     (R \u27f6 C) \u2227 (S \u27f6 C))\r\n  es equivalente a \r\n     R \u2228 S \u27f6 C\r\n*}\r\n\r\nlemma \"((R \u27f6 C) \u2227 (S \u27f6 C)) = (R \u2228 S \u27f6 C)\"\r\nproof (rule iffI)\r\n  assume \"(R \u27f6 C) \u2227 (S \u27f6 C)\"\r\n  thus \"R \u2228 S \u27f6 C\" by blast\r\nnext\r\n  assume \"R \u2228 S \u27f6 C\"\r\n  thus \"(R \u27f6 C) \u2227 (S \u27f6 C)\" by blast\r\nqed\r\n\r\ntext {* \r\n  El m\u00e9todo \"blast\":\r\n  En la demostraci\u00f3n anterior es la primera vez que se usa el m\u00e9todo de\r\n  razonamiento autom\u00e1tico \"blast\".\r\n\r\n  Nota. El lema anterior puede demostrarse autom\u00e1ticamente como se\r\n  muestra a continuaci\u00f3n.  \r\n*}\r\n\r\nlemma \"((R \u27f6 C) \u2227 (S \u27f6 C)) = (R \u2228 S \u27f6 C)\"\r\nby auto\r\n\r\ntext {*\r\n  Lema. [Ejemplo de eliminaci\u00f3n de equivalencia]\r\n  \u00b7 A \u27f7 B, A \u22a2 B\r\n  \u00b7 A \u27f7 B, B \u22a2 A\r\n*}\r\n\r\nlemma assumes \"A = B\" and \"A\" shows \"B\"\r\nusing assms \r\nby (rule iffD1)\r\n\r\nlemma assumes \"A = B\" and \"B\" shows \"A\"\r\nusing assms\r\nby (rule iffD2)\r\n\r\nend\r\n<\/pre>\n<p>Como trabajo se ha propuesto la realizaci\u00f3n de los ejercicios de las <a href=\"https:\/\/www.glc.us.es\/~jalonso\/WikiRA2010\/index.php5\/Razonamiento_autom%C3%A1tico\">relaciones de razonamiento sobre listas<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se han presentado los principales patrones de inducci\u00f3n en Isabelle: en la primera parte se ha presentado los patrones de de mostraci\u00f3n por casos y por inducci\u00f3n y en la segunda parte se han presentado otros patrones (eliminaci\u00f3n de disyunci\u00f3n, negaci\u00f3n, contradicci\u00f3n y equivalencias). La&#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":[170,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\/1868"}],"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=1868"}],"version-history":[{"count":6,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1868\/revisions"}],"predecessor-version":[{"id":2860,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1868\/revisions\/2860"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1868"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1868"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1868"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}