{"id":203,"date":"2020-02-24T15:38:53","date_gmt":"2020-02-24T13:38:53","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=203"},"modified":"2021-08-21T13:21:00","modified_gmt":"2021-08-21T11:21:00","slug":"praeclarum-theorema","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/praeclarum-theorema\/","title":{"rendered":"Praeclarum theorema"},"content":{"rendered":"<p>Demostrar el <a href=\"http:\/\/bit.ly\/2S9IYBX\">Praeclarum theorema<\/a> de Leibniz:<\/p>\n<pre lang=\"isar\">\ntheory Praeclarum_theorema\nimports Main\nbegin\n\nlemma \"(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\"\n  oops\n\nend\n<\/pre>\n<h4>Soluciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Praeclarum_theorema\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n: autom\u00e1tica *)\nlemma \"(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\"\n  by simp\n\n(* 2\u00aa demostraci\u00f3n: aplicativa *)\nlemma \"(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\"\n  apply (rule impI)\n  apply (rule impI)\n  apply (erule conjE)+\n  apply (rule conjI)\n   apply (erule mp)\n   apply assumption\n  apply (erule mp)\n  apply assumption\n  done\n\n(* 3\u00aa demostraci\u00f3n: estructurada *)\nlemma \"(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\"\nproof\n  assume \"(p \u27f6 q) \u2227 (r \u27f6 s)\"\n  show \"(p \u2227 r) \u27f6 (q \u2227 s)\"\n  proof\n    assume \"p \u2227 r\"\n    show \"q \u2227 s\"\n    proof\n      have \"p \u27f6 q\" using \u2039(p \u27f6 q) \u2227 (r \u27f6 s)\u203a ..\n      moreover have \"p\" using \u2039p \u2227 r\u203a ..\n      ultimately show \"q\" ..\n    next\n      have \"r \u27f6 s\" using \u2039(p \u27f6 q) \u2227 (r \u27f6 s)\u203a ..\n      moreover have \"r\" using \u2039p \u2227 r\u203a ..\n      ultimately show \"s\" ..\n    qed\n  qed\nqed\n\n(* 4\u00aa demostraci\u00f3n: detallada *)\nlemma \"(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\"\nproof (rule impI)\n  assume \"(p \u27f6 q) \u2227 (r \u27f6 s)\"\n  show \"(p \u2227 r) \u27f6 (q \u2227 s)\"\n  proof (rule impI)\n    assume \"p \u2227 r\"\n    show \"q \u2227 s\"\n    proof (rule conjI)\n      have \"p \u27f6 q\" using \u2039(p \u27f6 q) \u2227 (r \u27f6 s)\u203a by (rule conjunct1)\n      moreover have \"p\" using \u2039p \u2227 r\u203a by (rule conjunct1)\n      ultimately show \"q\" by (rule mp)\n    next\n      have \"r \u27f6 s\" using \u2039(p \u27f6 q) \u2227 (r \u27f6 s)\u203a by (rule conjunct2)\n      moreover have \"r\" using \u2039p \u2227 r\u203a by (rule conjunct2)\n      ultimately show \"s\" by (rule mp)\n    qed\n  qed\nqed\n\nend\n<\/pre>\n<h4>Otras soluciones<\/h4>\n<ul>\n<li>Se pueden escribir otras soluciones en los comentarios.\n<li>El c\u00f3digo se debe escribir entre una l\u00ednea con &#60;pre lang=&quot;isar&quot;&#62; y otra con &#60;\/pre&#62;\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Demostrar el Praeclarum theorema de Leibniz: theory Praeclarum_theorema imports Main begin lemma \u00ab(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\u00bb oops end Soluciones con Isabelle\/HOL theory Praeclarum_theorema imports Main begin (* 1\u00aa demostraci\u00f3n: autom\u00e1tica *) lemma \u00ab(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\u00bb by simp (* 2\u00aa demostraci\u00f3n: aplicativa *) lemma \u00ab(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\u00bb apply (rule impI) apply (rule impI) apply (erule conjE)+ apply (rule conjI) apply (erule mp) apply assumption apply (erule mp) apply assumption done (* 3\u00aa demostraci\u00f3n: estructurada *) lemma \u00ab(p \u27f6 q) \u2227 (r \u27f6 s) \u27f6 ((p \u2227 r) \u27f6 (q \u2227 s))\u00bb&#8230;<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[104],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/203"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=203"}],"version-history":[{"count":6,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/203\/revisions"}],"predecessor-version":[{"id":271,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/203\/revisions\/271"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=203"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=203"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=203"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}