{"id":6940,"date":"2020-01-16T09:22:50","date_gmt":"2020-01-16T08:22:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6940"},"modified":"2020-01-18T09:29:08","modified_gmt":"2020-01-18T08:29:08","slug":"ra2019-deduccion-natural-de-primer-orden-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-deduccion-natural-de-primer-orden-con-isabelle-hol\/","title":{"rendered":"RA2019: Deducci\u00f3n natural de primer orden 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 deducci\u00f3n natural de primer orden Isabelle\/HOL. La presentaci\u00f3n se basa en los ejemplos del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-14\/temas\/tema-8.pdf\">tema 8<\/a> del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-14\">L\u00f3gica inform\u00e1tica<\/a> que, a su vez, se basa en el cap\u00edtulo 2 del libro de Huth y Ryan <a href=\"http:\/\/goo.gl\/fGsqf\">Logic in Computer Science (Modelling and reasoning about systems)<\/a>.<\/p>\n<p>La p\u00e1gina al lado de cada ejemplo indica la p\u00e1gina de las transparencias donde se encuentra la demostraci\u00f3n.<\/p>\n<p>Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostraci\u00f3n de las transparencias, las siguientes van eliminando detalles de la prueba hasta la \u00faltima que es autom\u00e1tica.<\/p>\n<p>A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039Tema 7: Deducci\u00f3n natural en l\u00f3gica de primer orden\u203a\n\ntheory T7_Deduccion_natural_en_logica_de_primer_orden\nimports Main \nbegin\n\ntext \u2039El objetivo de este tema es presentar la deducci\u00f3n natural en \n  l\u00f3gica de primer orden con Isabelle\/HOL. La presentaci\u00f3n se \n  basa en los ejemplos de tema 4 del curso LMF que se encuentra \n  en http:\/\/goo.gl\/uJj8d (que a su vez se basa en el libro de \n  Huth y Ryan \"Logic in Computer Science\" http:\/\/goo.gl\/qsVpY ). \n\n  La p\u00e1gina al lado de cada ejemplo indica la p\u00e1gina de las \n  transparencias de LMF donde se encuentra la demostraci\u00f3n.\u203a\n\nsection \u2039Reglas del cuantificador universal\u203a\n\ntext \u2039Las reglas del cuantificador universal son\n  \u00b7 allE:    \u27e6\u2200x. P x; P a \u27f9 R\u27e7 \u27f9 R\n  \u00b7 allI:    (\u22c0x. P x) \u27f9 \u2200x. P x \u203a\n\nsubsection \u2039Ejemplo 1\u203a\n\ntext \u2039Ejemplo 1 (p. 10). Demostrar que\n     P(c), \u2200x. (P(x) \u27f6 \u00acQ(x)) \u22a2 \u00acQ(c) \u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_1a: \n  assumes 1: \"P(c)\" and\n          2: \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\n  shows \"\u00acQ(c)\"\nproof -\n  have 3: \"P(c) \u27f6 \u00acQ(c)\" using 2 by (rule allE)\n  show 4: \"\u00acQ(c)\" using 3 1 by (rule mp)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_1b: \n  assumes \"P(c)\"\n          \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\n  shows \"\u00acQ(c)\"\nproof -\n  have \"P(c) \u27f6 \u00acQ(c)\" using assms(2) ..\n  then show \"\u00acQ(c)\" using assms(1) ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_1c: \n  assumes \"P(c)\"\n          \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\n  shows \"\u00acQ(c)\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_1d: \n  \"\u27e6 P(c)\n   ; \u2200x. (P(x) \u27f6 \u00acQ(x))\u27e7 \n  \u27f9 \u00acQ(c)\"\n  apply (erule allE) (* da \u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c *)\n  apply (erule mp)   (* da P c \u27f9 P c *)\n  apply assumption   (* da No subgoals! *)\n  done\n\ntext \u2039Referencia sobre los tipos de reglas: \"A Proof Assistant for\nHigher-Order Logic\" http:\/\/bit.ly\/2TqYBWF \u203a\n\ntext \u2039Explicaciones\n  apply (erule allE) \n  + Objetivo:       \"\u27e6P(c); \u2200x. (P(x) \u27f6 \u00acQ(x))\u27e7 \u27f9 \u00acQ(c)\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"\u00acQ(c)\", \"\u2200x. (P(x) \u27f6 \u00acQ(x))\") y\n                    (\"?R\",    \"\u2200x. ?P x\")\n    es              ?R \/ \u00acQ(c)\n                    ?P x \/ P(x) \u27f6 \u00acQ(x) \n  + Nuevo objetivo: \"\u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c\"\n\n  apply (erule mp)   \n  + Objetivo:       \"\u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c\"\n  + mp:             \"\u27e6?P \u27f6 ?Q; ?P\u27e7 \u27f9 ?Q\"\n  + Unificador de   (\"\u00ac Q c\", \"P ?x \u27f6 \u00ac Q ?x\") y\n                    (\"?Q\",    \"?P \u27f6 ?Q\")\n    es              ?Q \/ \u00ac Q c\n                    ?P \/ P c\n  + Nuevo objetivo: \"P c \u27f9 P c\"  \u203a\n\nsubsection \u2039Ejemplo 2\u203a\n\ntext \u2039Ejemplo 2 (p. 11). Demostrar que\n     \u2200x. (P x \u27f6 \u00ac(Q x)), \u2200x. P x \u22a2 \u2200x. \u00ac(Q x) \u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_2a: \n  assumes 1: \"\u2200x. (P x \u27f6 \u00ac(Q x))\" and\n          2: \"\u2200x. P x\"\n  shows \"\u2200x. \u00ac(Q x)\"\nproof -\n  { fix a\n    have 3: \"P a \u27f6 \u00ac(Q a)\" using 1 by (rule allE)\n    have 4: \"P a\" using 2 by (rule allE)\n    have 5: \"\u00ac(Q a)\" using 3 4 by (rule mp) }\n  then show \"\u2200x. \u00ac(Q x)\" by (rule allI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada hacia atr\u00e1s es\u203a\nlemma ejemplo_2b: \n  assumes 1: \"\u2200x. (P x \u27f6 \u00ac(Q x))\" and\n          2: \"\u2200x. P x\"\n  shows \"\u2200x. \u00ac(Q x)\"\nproof (rule allI)\n  fix a\n  have 3: \"P a \u27f6 \u00ac(Q a)\" using 1 by (rule allE)\n  have 4: \"P a\" using 2 by (rule allE)\n  show 5: \"\u00ac(Q a)\" using 3 4 by (rule mp) \nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_2c: \n  assumes \"\u2200x. (P x \u27f6 \u00ac(Q x))\"\n          \"\u2200x. P x\"\n  shows \"\u2200x. \u00ac(Q x)\"\nproof \n  fix a\n  have \"P a\" using assms(2) ..\n  have \"P a \u27f6 \u00ac(Q a)\" using assms(1) ..\n  then show \"\u00ac(Q a)\" using \u2039P a\u203a ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_2d: \n  assumes \"\u2200x. (P x \u27f6 \u00ac(Q x))\"\n          \"\u2200x. P x\"\n  shows   \"\u2200x. \u00ac(Q x)\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_2e: \n  \"\u27e6\u2200x. (P x \u27f6 \u00ac(Q x)); \u2200y. P y\u27e7 \u27f9 \u2200z. \u00ac(Q z)\"\n  apply (rule allI)   (* da \u22c0z. \u27e6P (?x2 z) \u27f6 \u00ac Q (?x2 z);\n                                 P (?y4 z)\u27e7\n                                \u27f9 \u00ac Q z*)\n  apply (erule allE)+ (* da \u22c0z. \u27e6P (?x2 z) \u27f6 \u00ac Q (?x2 z);\n                                 P (?y4 z)\u27e7\n                                \u27f9 \u00ac Q z *)\n  apply (erule mp)    (* da \u22c0z. P (?y4 z) \u27f9 P z *)\n  apply assumption    (* da No subgoals! *) \n  done\n\nsection \u2039Reglas del cuantificador existencial\u203a\n\ntext \u2039Las reglas del cuantificador existencial son\n  \u00b7 exI:     P a \u27f9 \u2203x. P x\n  \u00b7 exE:     \u27e6\u2203x. P x; \u22c0x. P x \u27f9 Q\u27e7 \u27f9 Q\n\n  En la regla exE la nueva variable se introduce mediante la declaraci\u00f3n \n  \"obtain ... where ... by (rule exE)\" \n\u203a\n\nsubsection \u2039Ejemplo 3\u203a\n\ntext \u2039Ejemplo 3 (p. 12). Demostrar que\n     \u2200x. P x \u22a2 \u2203x. P x\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_3a:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\nproof -\n  fix a\n  have \"P a\" using assms by (rule allE)\n  then show \"\u2203x. P x\" by (rule exI)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_3b:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\nproof -\n  fix a\n  have \"P a\" using assms ..\n  then show \"\u2203x. P x\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada se puede simplificar\u203a\nlemma ejemplo_3c:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\nproof (rule exI)\n  fix a\n  show \"P a\" using assms ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada se puede simplificar a\u00fan m\u00e1s\u203a\nlemma ejemplo_3d:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\nproof \n  fix a\n  show \"P a\" using assms ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_3e:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_3f: \n  \"\u2200x. P x \u27f9 \u2203y. P y\"\n  apply (erule allE) (* da P ?x \u27f9 \u2203y. P y *)\n  apply (erule exI)  (* da No subgoals! *)\n  done\n\nsubsection \u2039Ejemplo 4\u203a\n\ntext \u2039Ejemplo 4 (p. 13). Demostrar\n     \u2200x. (P x \u27f6 Q x), \u2203x. P x \u22a2 \u2203x. Q x\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_4a:\n  assumes 1: \"\u2200x. (P x \u27f6 Q x)\" and\n          2: \"\u2203x. P x\"\n  shows \"\u2203x. Q x\"\nproof -\n  obtain a where 3: \"P a\" using 2 by (rule exE)\n  have 4: \"P a \u27f6 Q a\" using 1 by (rule allE)\n  have 5: \"Q a\" using 4 3 by (rule mp)\n  then show 6: \"\u2203x. Q x\" by (rule exI)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_4b:\n  assumes \"\u2200x. (P x \u27f6 Q x)\"\n          \"\u2203x. P x\"\n  shows \"\u2203x. Q x\"\nproof -\n  obtain a where \"P a\" using assms(2) ..\n  have \"P a \u27f6 Q a\" using assms(1) ..\n  then have \"Q a\" using \u2039P a\u203a ..\n  then show \"\u2203x. Q x\" ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_4c:\n  assumes \"\u2200x. (P x \u27f6 Q x)\"\n          \"\u2203x. P x\"\n  shows \"\u2203x. Q x\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_4f: \n  \"\u27e6\u2200x. P x \u27f6 Q x; \u2203y. P y\u27e7 \u27f9 \u2203z. Q z\"\n  apply (erule exE)  (* da \u22c0y. \u27e6\u2200x. P x \u27f6 Q x; P y\u27e7 \u27f9 \u2203z. Q z *)\n  apply (erule allE) (* da \u22c0y. \u27e6P y; P (?x2 y) \u27f6 Q (?x2 y)\u27e7 \u27f9 \u2203z. Q z *)\n  apply (rule exI)   (* da \u22c0y. \u27e6P y; P (?x2 y) \u27f6 Q (?x2 y)\u27e7 \u27f9 Q (?z4 y) *)\n  apply (erule mp)   (* da \u22c0y. P y \u27f9 P (?x2 y) *)\n  apply assumption   (* da No subgoals! *)\n  done\n\nsection \u2039Demostraci\u00f3n de equivalencias\u203a\n\nsubsection \u2039Ejemplo 5.1\u203a\n\ntext \u2039Ejemplo 5.1 (p. 15). Demostrar\n     \u00ac\u2200x. P x  \u22a2 \u2203x. \u00ac(P x)\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_5_1a:\n  assumes \"\u00ac(\u2200x. P(x))\"\n  shows   \"\u2203x. \u00acP(x)\"\nproof (rule ccontr)\n  assume \"\u00ac(\u2203x. \u00acP(x))\"\n  have \"\u2200x. P(x)\"\n  proof (rule allI)\n    fix a\n    show \"P(a)\"\n    proof (rule ccontr)\n      assume \"\u00acP(a)\"\n      then have \"\u2203x. \u00acP(x)\" by (rule exI)\n      with \u2039\u00ac(\u2203x. \u00acP(x))\u203a show False by (rule notE)\n    qed\n  qed\n  with assms show False by (rule notE)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_5_1b:\n  assumes \"\u00ac(\u2200x. P(x))\"\n  shows   \"\u2203x. \u00acP(x)\"\nproof (rule ccontr)\n  assume \"\u00ac(\u2203x. \u00acP(x))\"\n  have \"\u2200x. P(x)\"\n  proof \n    fix a\n    show \"P(a)\"\n    proof (rule ccontr)\n      assume \"\u00acP(a)\"\n      then have \"\u2203x. \u00acP(x)\" ..\n      with \u2039\u00ac(\u2203x. \u00acP(x))\u203a show False ..\n    qed\n  qed\n  with assms show False ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_5_1c:\n  assumes \"\u00ac(\u2200x. P(x))\"\n  shows   \"\u2203x. \u00acP(x)\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_5_1d: \"\u00ac(\u2200x. P x) \u27f9 \u2203y. \u00acP y\"\n  apply (rule ccontr) (* da \u27e6\u00ac (\u2200x. P x); \u2204y. \u00ac P y\u27e7 \u27f9 False *)\n  apply (erule notE)  (* da \u2204y. \u00ac P y \u27f9 \u2200x. P x *)\n  apply (rule allI)   (* da \u22c0x. \u2204y. \u00ac P y \u27f9 P x *)\n  apply (rule ccontr) (* da \u22c0x. \u27e6\u2204y. \u00ac P y; \u00ac P x\u27e7 \u27f9 False *)\n  apply (erule notE)  (* da \u22c0x. \u00ac P x \u27f9 \u2203y. \u00ac P y *)\n   apply (erule exI)  (* da No subgoals! *)\n  done\n\n\ntext \u2039\n  Ejemplo 5.2 (p. 16). Demostrar\n     \u2203x. \u00ac(P x)  \u22a2 \u00ac\u2200x. P x\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_5_2a:\n  assumes \"\u2203x. \u00acP(x)\"\n  shows   \"\u00ac(\u2200x. P(x))\"\nproof (rule notI)\n  assume \"\u2200x. P(x)\"\n  obtain a where \"\u00acP(a)\" using assms by (rule exE)\n  have \"P(a)\" using \u2039\u2200x. P(x)\u203a by (rule allE)\n  with \u2039\u00acP(a)\u203a show False by (rule notE)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_5_2b:\n  assumes \"\u2203x. \u00acP(x)\"\n  shows   \"\u00ac(\u2200x. P(x))\"\nproof \n  assume \"\u2200x. P(x)\"\n  obtain a where \"\u00acP(a)\" using assms ..\n  have \"P(a)\" using \u2039\u2200x. P(x)\u203a ..\n  with \u2039\u00acP(a)\u203a show False ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_5_2c:\n  assumes \"\u2203x. \u00acP(x)\"\n  shows   \"\u00ac(\u2200x. P(x))\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 5.3 (p. 17). Demostrar\n     \u22a2 \u00ac\u2200x. P x  \u27f7 \u2203x. \u00ac(P x)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_5_3a:\n  \"(\u00ac(\u2200x. P(x))) \u27f7 (\u2203x. \u00acP(x))\"\nproof (rule iffI)\n  assume \"\u00ac(\u2200x. P(x))\"\n  then show \"\u2203x. \u00acP(x)\" by (rule ejemplo_5_1a)\nnext\n  assume \"\u2203x. \u00acP(x)\"\n  then show \"\u00ac(\u2200x. P(x))\" by (rule ejemplo_5_2a)\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_5_3b:\n  \"(\u00ac(\u2200x. P(x))) \u27f7 (\u2203x. \u00acP(x))\"\nby auto\n\ntext \u2039\n  Ejemplo 6.1 (p. 18). Demostrar\n     \u2200x. P(x) \u2227 Q(x) \u22a2  (\u2200x. P(x)) \u2227 (\u2200x. Q(x))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_6_1a:\n  assumes \"\u2200x. P(x) \u2227 Q(x)\"\n  shows   \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\nproof (rule conjI)\n  show \"\u2200x. P(x)\"\n  proof (rule allI)\n    fix a\n    have \"P(a) \u2227 Q(a)\" using assms by (rule allE)\n    then show \"P(a)\" by (rule conjunct1)\n  qed\nnext\n  show \"\u2200x. Q(x)\"\n  proof (rule allI)\n    fix a\n    have \"P(a) \u2227 Q(a)\" using assms by (rule allE)\n    then show \"Q(a)\" by (rule conjunct2)\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_6_1b:\n  assumes \"\u2200x. P(x) \u2227 Q(x)\"\n  shows   \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\nproof \n  show \"\u2200x. P(x)\"\n  proof \n    fix a\n    have \"P(a) \u2227 Q(a)\" using assms ..\n    then show \"P(a)\" ..\n  qed\nnext\n  show \"\u2200x. Q(x)\"\n  proof \n    fix a\n    have \"P(a) \u2227 Q(a)\" using assms ..\n    then show \"Q(a)\" ..\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_6_1c:\n  assumes \"\u2200x. P(x) \u2227 Q(x)\"\n  shows   \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 6.2 (p. 19). Demostrar\n     (\u2200x. P(x)) \u2227 (\u2200x. Q(x)) \u22a2 \u2200x. P(x) \u2227 Q(x)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_6_2a:\n  assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n  shows   \"\u2200x. P(x) \u2227 Q(x)\"\nproof (rule allI)\n  fix a\n  have \"\u2200x. P(x)\" using assms by (rule conjunct1)\n  then have \"P(a)\" by (rule allE)\n  have \"\u2200x. Q(x)\" using assms by (rule conjunct2)\n  then have \"Q(a)\" by (rule allE)\n  with \u2039P(a)\u203a show \"P(a) \u2227 Q(a)\" by (rule conjI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_6_2b:\n  assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n  shows   \"\u2200x. P(x) \u2227 Q(x)\"\nproof\n  fix a\n  have \"\u2200x. P(x)\" using assms ..\n  then have \"P(a)\" by (rule allE)\n  have \"\u2200x. Q(x)\" using assms ..\n  then have \"Q(a)\" ..\n  with \u2039P(a)\u203a show \"P(a) \u2227 Q(a)\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_6_2c:\n  assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n  shows   \"\u2200x. P(x) \u2227 Q(x)\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 6.3 (p. 20). Demostrar\n     \u22a2 \u2200x. P(x) \u2227 Q(x) \u27f7 (\u2200x. P(x)) \u2227 (\u2200x. Q(x))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_6_3a:\n  \"(\u2200x. P(x) \u2227 Q(x)) \u27f7 ((\u2200x. P(x)) \u2227 (\u2200x. Q(x)))\"\nproof (rule iffI)\n  assume \"\u2200x. P(x) \u2227 Q(x)\"\n  then show \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\" by (rule ejemplo_6_1a)\nnext\n  assume \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n  then show \"\u2200x. P(x) \u2227 Q(x)\" by (rule ejemplo_6_2a)\nqed\n\ntext \u2039\n  Ejemplo 7.1 (p. 21). Demostrar\n     (\u2203x. P(x)) \u2228 (\u2203x. Q(x)) \u22a2 \u2203x. P(x) \u2228 Q(x)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_7_1a:\n  assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  shows   \"\u2203x. P(x) \u2228 Q(x)\"\nusing assms\nproof (rule disjE)\n  assume \"\u2203x. P(x)\"\n  then obtain a where \"P(a)\" by (rule exE)\n  then have \"P(a) \u2228 Q(a)\" by (rule disjI1)\n  then show \"\u2203x. P(x) \u2228 Q(x)\" by (rule exI)\nnext\n  assume \"\u2203x. Q(x)\"\n  then obtain a where \"Q(a)\" by (rule exE)\n  then have \"P(a) \u2228 Q(a)\" by (rule disjI2)\n  then show \"\u2203x. P(x) \u2228 Q(x)\" by (rule exI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_7_1b:\n  assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  shows   \"\u2203x. P(x) \u2228 Q(x)\"\nusing assms\nproof\n  assume \"\u2203x. P(x)\"\n  then obtain a where \"P(a)\" ..\n  then have \"P(a) \u2228 Q(a)\" ..\n  then show \"\u2203x. P(x) \u2228 Q(x)\" ..\nnext\n  assume \"\u2203x. Q(x)\"\n  then obtain a where \"Q(a)\" ..\n  then have \"P(a) \u2228 Q(a)\" ..\n  then show \"\u2203x. P(x) \u2228 Q(x)\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_7_1c:\n  assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  shows   \"\u2203x. P(x) \u2228 Q(x)\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 7.2 (p. 22). Demostrar\n     \u2203x. P(x) \u2228 Q(x) \u22a2 (\u2203x. P(x)) \u2228 (\u2203x. Q(x))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_7_2a:\n  assumes \"\u2203x. P(x) \u2228 Q(x)\"\n  shows   \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\nproof -\n  obtain a where \"P(a) \u2228 Q(a)\" using assms by (rule exE)\n  then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  proof (rule disjE)\n    assume \"P(a)\"\n    then have \"\u2203x. P(x)\" by (rule exI)\n    then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule disjI1)\n  next\n    assume \"Q(a)\"\n    then have \"\u2203x. Q(x)\" by (rule exI)\n    then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule disjI2)\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejercicio_7_2b:\n  assumes \"\u2203x. P(x) \u2228 Q(x)\"\n  shows   \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\nproof -\n  obtain a where \"P(a) \u2228 Q(a)\" using assms ..\n  then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  proof \n    assume \"P(a)\"\n    then have \"\u2203x. P(x)\" ..\n    then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" ..\n  next\n    assume \"Q(a)\"\n    then have \"\u2203x. Q(x)\" ..\n    then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" ..\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejercicio_7_2c:\n  assumes \"\u2203x. P(x) \u2228 Q(x)\"\n  shows   \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 7.3 (p. 23). Demostrar\n     \u22a2 ((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_7_3a:\n  \"((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))\"\nproof (rule iffI)\n  assume \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  then show \"\u2203x. P(x) \u2228 Q(x)\" by (rule ejemplo_7_1a)\nnext\n  assume \"\u2203x. P(x) \u2228 Q(x)\"\n  then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule ejemplo_7_2a)\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_7_3b:\n  \"((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 8.1 (p. 24). Demostrar\n     \u2203x y. P(x,y) \u22a2 \u2203y x. P(x,y)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_8_1a:\n  assumes \"\u2203x y. P(x,y)\"\n  shows   \"\u2203y x. P(x,y)\"\nproof -\n  obtain a where \"\u2203y. P(a,y)\" using assms by (rule exE)\n  then obtain b where \"P(a,b)\" by (rule exE)\n  then have \"\u2203x. P(x,b)\" by (rule exI)\n  then show \"\u2203y x. P(x,y)\" by (rule exI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_8_1b:\n  assumes \"\u2203x y. P(x,y)\"\n  shows   \"\u2203y x. P(x,y)\"\nproof -\n  obtain a where \"\u2203y. P(a,y)\" using assms ..\n  then obtain b where \"P(a,b)\" ..\n  then have \"\u2203x. P(x,b)\" ..\n  then show \"\u2203y x. P(x,y)\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_8_1c:\n  assumes \"\u2203x y. P(x,y)\"\n  shows   \"\u2203y x. P(x,y)\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 8.2. Demostrar\n     \u2203y x. P(x,y) \u22a2 \u2203x y. P(x,y)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_8_2a:\n  assumes \"\u2203y x. P(x,y)\"\n  shows   \"\u2203x y. P(x,y)\"\nproof -\n  obtain b where \"\u2203x. P(x,b)\" using assms by (rule exE)\n  then obtain a where \"P(a,b)\" by (rule exE)\n  then have \"\u2203y. P(a,y)\" by (rule exI)\n  then show \"\u2203x y. P(x,y)\" by (rule exI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_8_2b:\n  assumes \"\u2203y x. P(x,y)\"\n  shows   \"\u2203x y. P(x,y)\"\nproof -\n  obtain b where \"\u2203x. P(x,b)\" using assms ..\n  then obtain a where \"P(a,b)\" ..\n  then have \"\u2203y. P(a,y)\" ..\n  then show \"\u2203x y. P(x,y)\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_8_2c:\n  assumes \"\u2203y x. P(x,y)\"\n  shows   \"\u2203x y. P(x,y)\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 8.3 (p. 25). Demostrar\n     \u22a2 (\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_8_3a:\n  \"(\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\"\nproof (rule iffI)\n  assume \"\u2203x y. P(x,y)\"\n  then show \"\u2203y x. P(x,y)\" by (rule ejemplo_8_1a)\nnext\n  assume \"\u2203y x. P(x,y)\"\n  then show \"\u2203x y. P(x,y)\" by (rule ejemplo_8_2a)\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_8_3b:\n  \"(\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\"\nby auto\n\nsection \u2039Reglas de la igualdad\u203a\n\ntext \u2039\n  Las reglas b\u00e1sicas de la igualdad son:\n  \u00b7 refl:  t = t\n  \u00b7 subst: \u27e6s = t; P s\u27e7 \u27f9 P t\n\u203a\n\ntext \u2039\n  Ejemplo 9 (p. 27). Demostrar\n     x + 1 = 1 + x, x + 1 > 1 \u27f6 x + 1 > 0 \u22a2 1 + x > 1 \u27f6 1 + x > 0\n\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_9a: \n  assumes \"x + 1 = 1 + x\" \n          \"x + 1 > 1 \u27f6 x + 1 > 0\"\n  shows   \"1 + x > 1 \u27f6 1 + x > 0\"\nproof -\n  show \"1 + x > 1 \u27f6 1 + x > 0\" using assms by (rule subst)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_9b: \n  assumes \"x + 1 = 1 + x\" \n          \"x + 1 > 1 \u27f6 x + 1 > 0\"\n  shows   \"1 + x > 1 \u27f6 1 + x > 0\"\nusing assms \nby (rule subst)\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_9c: \n  assumes \"x + 1 = 1 + x\" \n          \"x + 1 > 1 \u27f6 x + 1 > 0\"\n  shows   \"1 + x > 1 \u27f6 1 + x > 0\"\nusing assms \nby auto\n\ntext \u2039\n  Ejemplo 10 (p. 27). Demostrar\n     x = y, y = z \u22a2 x = z\n\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_10a:\n  assumes \"x = y\" \n          \"y = z\"\n  shows   \"x = z\"\nproof -\n  show \"x = z\" using assms(2,1) by (rule subst)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_10b: \n  assumes \"x = y\" \n          \"y = z\"\n  shows   \"x = z\"\nusing assms(2,1)\nby (rule subst)\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_10c: \n  assumes \"x = y\" \n          \"y = z\"\n  shows   \"x = z\"\nusing assms\nby auto\n\ntext \u2039\n  Ejemplo 11 (p. 28). Demostrar\n     s = t \u22a2 t = s\n\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_11a:\n  assumes \"s = t\"\n  shows   \"t = s\"\nproof -\n  have \"s = s\" by (rule refl)\n  with assms show \"t = s\" by (rule subst)\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_11b:\n  assumes \"s = t\"\n  shows   \"t = s\"\nusing assms\nby auto\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha presentado la deducci\u00f3n natural de primer orden Isabelle\/HOL. La presentaci\u00f3n se basa en los ejemplos del tema 8 del curso de L\u00f3gica inform\u00e1tica que, a su vez, se basa en el cap\u00edtulo 2 del libro de Huth y Ryan Logic in Computer Science&#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":[],"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\/6940"}],"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=6940"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6940\/revisions"}],"predecessor-version":[{"id":6945,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6940\/revisions\/6945"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6940"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6940"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6940"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}