{"id":6580,"date":"2019-03-26T18:39:09","date_gmt":"2019-03-26T17:39:09","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6580"},"modified":"2019-03-26T18:39:09","modified_gmt":"2019-03-26T17:39:09","slug":"lmf2018-deduccion-natural-proposicional-con-las-tacticas-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2018-deduccion-natural-proposicional-con-las-tacticas-isabelle-hol\/","title":{"rendered":"LMF2018: Deducci\u00f3n natural proposicional con las t\u00e1cticas Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-18\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado c\u00f3mo construir las pruebas por deducci\u00f3n natural usando las t\u00e1cticas de Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\ntheory T2b\nimports Main\nbegin\n\nsection \"Introducci\u00f3n\"\n\nsubsection \"Enunciado de teoremas\"  \n  \ntheorem primerEjemplo: \"(A \u27f6 B) \u2228 (B \u27f6 A)\"\noops  \n\nsubsection \"Demostraci\u00f3n por asunci\u00f3n\"\n\nlemma \"\u27e6A; B; C\u27e7 \u27f9 B\"\n  apply assumption\n  done\n\nsubsection \"Ejemplo de aplicaci\u00f3n de rule\"\n\ntext {* 1\u00ba ejemplo de aplicaci\u00f3n de rule *}\nlemma \"A \u2227 B \u27f9 B \u2227 A\"\n  apply (rule conjI)\n  oops\n\ntext {* 2\u00ba ejemplo de aplicaci\u00f3n de rule *}\nlemma \"A \u2227 B \u27f9 B \u2228 A\"\n  apply (rule disjI1)\n  oops\n\nlemma \"\u27e6(A \u2227 B) \u2228 C; D\u27e7 \u27f9 B \u2228 C\"    \n  apply (rule disjE)\n    apply assumption\n  oops   \n    \nsubsection \"Ejemplo de demostraci\u00f3n con rule y assumption\"\n\ntheorem K: \"A \u27f6 (B \u27f6 A)\"\n  apply (rule impI)  (* da  A \u27f9 B \u27f6 A *)\n  apply (rule impI)  (* da \u27e6A; B\u27e7 \u27f9 A *)\n  apply assumption   (* da No subgoals! *)\n  done\n\nsubsection \"Ejemplo de derivaci\u00f3n con hip\u00f3tesis\"    \n        \ntext {* Derivaci\u00f3n de A, B \u22a2 A \u2227 (B \u2227 A) *}\ntheorem \"\u27e6A; B\u27e7 \u27f9 A \u2227 (B \u2227 A)\"\n  apply (rule conjI)  (* da \u27e6A; B\u27e7 \u27f9 A\n                            \u27e6A; B\u27e7 \u27f9 B \u2227 A *)\n   apply assumption   (* da \u27e6A; B\u27e7 \u27f9 B \u2227 A *)\n  apply (rule conjI)  (* da \u27e6A; B\u27e7 \u27f9 B\n                            \u27e6A; B\u27e7 \u27f9 A *)\n   apply assumption   (* da \u27e6A; B\u27e7 \u27f9 A *)\n  apply assumption    (* da No subgoals *)\n  done \n\ntext {* La prueba anterior se puede simplificar usando assumption+ *}\ntheorem \"\u27e6A; B\u27e7 \u27f9 A \u2227 (B \u2227 A)\"\n  apply (rule conjI)  (* da \u27e6A; B\u27e7 \u27f9 A\n                            \u27e6A; B\u27e7 \u27f9 B \u2227 A *)\n   apply assumption   (* da \u27e6A; B\u27e7 \u27f9 B \u2227 A *)\n  apply (rule conjI)  (* da \u27e6A; B\u27e7 \u27f9 B\n                            \u27e6A; B\u27e7 \u27f9 A *)\n   apply assumption+  (* da No subgoals *)\n  done \n    \nsubsection \"Ejemplo de aplicaci\u00f3n de erule\"\n    \nlemma \"\u27e6(A \u2227 B) \u2228 C; D\u27e7 \u27f9 B \u2228 C\"    \n  apply (erule disjE)\n  oops\n\ntext {* Demostraci\u00f3n con erule *}    \nlemma \"A \u2228 B \u27f9 B \u2228 A\"\n  apply (erule disjE)   (* da A \u27f9 B \u2228 A\n                              B \u27f9 B \u2228 A*)\n   apply (rule disjI2)  (* da A \u27f9 A\n                              B \u27f9 B \u2228 A *)\n   apply assumption     (* da B \u27f9 B \u2228 A *)\n  apply (rule disjI1)   (* da B \u27f9 B *)\n  apply assumption      (* da No subgoals *)\n  done\n\ntext {* Variaci\u00f3n de la demostraci\u00f3n anterior cambiando erule por rule *}\nlemma \"A \u2228 B \u27f9 B \u2228 A\"\n  apply (rule disjE)    (* da A \u2228 B \u27f9 ?P \u2228 ?Q\n                              \u27e6A \u2228 B; ?P\u27e7 \u27f9 B \u2228 A\n                              \u27e6A \u2228 B; ?Q\u27e7 \u27f9 B \u2228 A *)\n    apply assumption    (* da \u27e6A \u2228 B; A\u27e7 \u27f9 B \u2228 A\n                              \u27e6A \u2228 B; B\u27e7 \u27f9 B \u2228 A *) \n   apply (rule disjI2)  (* da \u27e6A \u2228 B; A\u27e7 \u27f9 A\n                              \u27e6A \u2228 B; B\u27e7 \u27f9 B \u2228 A*)\n   apply assumption     (* da \u27e6A \u2228 B; B\u27e7 \u27f9 B \u2228 A *)\n  apply (rule disjI1)   (* da \u27e6A \u2228 B; B\u27e7 \u27f9 B *)\n  apply assumption      (* da No subgoals! *)\n  done\n    \nsubsection \"Ejemplo de aplicaci\u00f3n de drule\"\n    \nlemma \"\u27e6A \u27f6 B; A \u2227 C\u27e7 \u27f9 B \u2227 C\"    \n  apply (drule mp)\n  oops\n\ntext {* Demostraci\u00f3n con drule *}    \nlemma \"A \u2227 B \u27f9 A\"\n  apply (drule conjunct1) (* da A \u27f9 A *)\n  apply assumption        (* da No subgoals! *)\n  done   \n\nsubsection \"Ejemplo de aplicaci\u00f3n de frule\"\n    \nlemma \"\u27e6A \u27f6 B; A \u2227 C\u27e7 \u27f9 B \u2227 C\"    \n  apply (frule mp)\n  oops\n\ntext {* Demostraci\u00f3n con frule *}    \nlemma \"A \u2227 B \u27f9 A\"\n  apply (frule conjunct1)  (* da \u27e6A \u2227 B; A\u27e7 \u27f9 A *)\n  apply assumption         (* da No subgoals! *)\n  done  \n  \nsubsection \"Ejemplo de aplicaci\u00f3n de erule_tac\"\n    \nlemma \"\u27e6A \u2227 B; C \u2227 (B \u2227 D)\u27e7 \u27f9 B \u2227 D\"\n  apply (erule_tac Q=\"B \u2227 D\" in conjE)\n  apply assumption\n  done\n\nlemma \"\u27e6A \u2227 B; C \u2227 (B \u2227 D)\u27e7 \u27f9 B \u2227 D\"\n  apply (erule conjE)\n  oops\n\ntext {* Demostraci\u00f3n con erule_tac *}    \nlemma \"\u27e6A \u2227 B; C \u2227 D\u27e7 \u27f9 D\"\n  apply (erule_tac P=C in conjE)  (* da \u27e6A \u2227 B; C; D\u27e7 \u27f9 D *)\n  apply assumption                (* da No subgoals! *)\n  done  \n    \ntext {* Demostraci\u00f3n sin erule_tac *}    \nlemma \"\u27e6A \u2227 B; C \u2227 D\u27e7 \u27f9 D\"\n  apply (erule conjE)  (* da \u27e6C \u2227 D; A; B\u27e7 \u27f9 D *)\n  apply (erule conjE)  (* da \u27e6A; B; C; D\u27e7 \u27f9 D *)\n  apply assumption     (* da No subgoals! *)\n  done  \nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado c\u00f3mo construir las pruebas por deducci\u00f3n natural usando las t\u00e1cticas de Isabelle\/HOL. La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<\/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":[268],"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\/6580"}],"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=6580"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6580\/revisions"}],"predecessor-version":[{"id":6581,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6580\/revisions\/6581"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6580"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6580"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6580"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}