{"id":4239,"date":"2014-04-04T18:52:21","date_gmt":"2014-04-04T16:52:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4239"},"modified":"2014-04-05T08:53:34","modified_gmt":"2014-04-05T06:53:34","slug":"lmf2014-ejercicios-de-deduccion-en-logica-de-primer-orden-con-isabellehol-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2014-ejercicios-de-deduccion-en-logica-de-primer-orden-con-isabellehol-2\/","title":{"rendered":"LMF2014: Ejercicios de deducci\u00f3n en l\u00f3gica de primer orden con Isabelle\/HOL (2)"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-13\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha explicado c\u00f3mo demostrar mediante deducci\u00f3n natural teoremas de primer orden con Isabelle\/HOL. En concreto, se han visto los ejercicios 13, 15, 16, 19, 21, 32 y 35 de la <a href=\"http:\/\/bit.ly\/OjBcRp\">relaci\u00f3n 6<\/a>.<\/p>\n<p>Los ejercicios y sus soluciones se muestran a continuaci\u00f3n:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\ntheory R6\r\nimports Main \r\nbegin\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 13. Demostrar\r\n       (\u2200x. P x) \u2228 (\u2200x. Q x) \u22a2 \u2200x. P x \u2228 Q x\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_13a: \r\n  \"(\u2200x. P x) \u2228 (\u2200x. Q x) \u27f9 \u2200x. P x \u2228 Q x\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_13b: \r\n  assumes \"(\u2200x. P x) \u2228 (\u2200x. Q x)\"\r\n  shows   \"\u2200x. P x \u2228 Q x\"\r\nproof\r\n  fix a\r\n  note assms\r\n  thus \"P a \u2228 Q a\"\r\n  proof\r\n    assume \"\u2200x. P x\"\r\n    hence \"P a\" ..\r\n    thus \"P a \u2228 Q a\" ..\r\n  next\r\n    assume \"\u2200x. Q x\"\r\n    hence \"Q a\" ..\r\n    thus \"P a \u2228 Q a\" ..\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_13c: \r\n  assumes \"(\u2200x. P x) \u2228 (\u2200x. Q x)\"\r\n  shows   \"\u2200x. P x \u2228 Q x\"\r\nproof (rule  allI)\r\n  fix a\r\n  note assms\r\n  thus \"P a \u2228 Q a\"\r\n  proof (rule disjE)\r\n    assume \"\u2200x. P x\"\r\n    hence \"P a\" by (rule allE)\r\n    thus \"P a \u2228 Q a\" by (rule disjI1)\r\n  next\r\n    assume \"\u2200x. Q x\"\r\n    hence \"Q a\" by (rule allE)\r\n    thus \"P a \u2228 Q a\" by (rule disjI2)\r\n  qed\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 15. Demostrar\r\n       \u2200x y. P y \u27f6 Q x \u22a2 (\u2203y. P y) \u27f6 (\u2200x. Q x)\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_15a: \r\n  \"\u2200x y. P y \u27f6 Q x \u27f9 (\u2203y. P y) \u27f6 (\u2200x. Q x)\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_15b: \r\n  assumes \"\u2200x y. P y \u27f6 Q x\"\r\n  shows   \"(\u2203y. P y) \u27f6 (\u2200x. Q x)\"\r\nproof\r\n  assume \"\u2203y. P y\"\r\n  then obtain b where \"P b\" ..\r\n  show \"\u2200x. Q x\"\r\n  proof\r\n    fix a\r\n    have \"\u2200y. P y \u27f6 Q a\" using assms ..\r\n    hence \"P b \u27f6 Q a\" ..\r\n    thus \"Q a\" using `P b` ..\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_15c: \r\n  assumes \"\u2200x y. P y \u27f6 Q x\"\r\n  shows   \"(\u2203y. P y) \u27f6 (\u2200x. Q x)\"\r\nproof (rule impI)\r\n  assume \"\u2203y. P y\"\r\n  then obtain b where \"P b\" by (rule exE)\r\n  show \"\u2200x. Q x\"\r\n  proof (rule allI)\r\n    fix a\r\n    have \"\u2200y. P y \u27f6 Q a\" using assms by (rule allE)\r\n    hence \"P b \u27f6 Q a\" by (rule allE)\r\n    thus \"Q a\" using `P b` by (rule mp)\r\n  qed\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 16. Demostrar\r\n       \u00ac(\u2200x. \u00ac(P x)) \u22a2 \u2203x. P x\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_16a: \r\n  \"\u00ac(\u2200x. \u00ac(P x)) \u27f9 \u2203x. P x\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_16b: \r\n  assumes \"\u00ac(\u2200x. \u00ac(P x))\"\r\n  shows   \"\u2203x. P x\"\r\nproof (rule ccontr)\r\n  assume \"\u00ac(\u2203x. P x)\"\r\n  have \"\u2200x. \u00ac(P x)\"\r\n  proof\r\n    fix a\r\n    show \"\u00ac(P a)\"\r\n    proof\r\n      assume \"P a\"\r\n      hence \"\u2203x. P x\" ..\r\n      with `\u00ac(\u2203x. P x)` show False ..\r\n    qed\r\n  qed\r\n  with assms show False ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_16c: \r\n  assumes \"\u00ac(\u2200x. \u00ac(P x))\"\r\n  shows   \"\u2203x. P x\"\r\nproof (rule ccontr)\r\n  assume \"\u00ac(\u2203x. P x)\"\r\n  have \"\u2200x. \u00ac(P x)\"\r\n  proof (rule allI)\r\n    fix a\r\n    show \"\u00ac(P a)\"\r\n    proof\r\n      assume \"P a\"\r\n      hence \"\u2203x. P x\" by (rule exI)\r\n      with `\u00ac(\u2203x. P x)` show False by (rule notE)\r\n    qed\r\n  qed\r\n  with assms show False by (rule notE)\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 19. Demostrar\r\n       P a \u27f6 (\u2200x. Q x) \u22a2 \u2200x. P a \u27f6 Q x\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_19a:\r\n  \"P a \u27f6 (\u2200x. Q x) \u27f9 \u2200x. P a \u27f6 Q x\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_19b: \r\n  assumes \"P a \u27f6 (\u2200x. Q x)\"\r\n  shows   \"\u2200x. P a \u27f6 Q x\"\r\nproof\r\n  fix b\r\n  show \"P a \u27f6 Q b\"\r\n  proof\r\n    assume \"P a\"\r\n    with assms have \"\u2200x. Q x\" ..\r\n    thus \"Q b\" ..\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_19c: \r\n  assumes \"P a \u27f6 (\u2200x. Q x)\"\r\n  shows   \"\u2200x. P a \u27f6 Q x\"\r\nproof (rule allI)\r\n  fix b\r\n  show \"P a \u27f6 Q b\"\r\n  proof (rule impI)\r\n    assume \"P a\"\r\n    with assms have \"\u2200x. Q x\" by (rule mp)\r\n    thus \"Q b\" by (rule allE)\r\n  qed\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 21. Demostrar\r\n     {\u2200x. P x \u2228 Q x, \u2203x. \u00ac(Q x), \u2200x. R x \u27f6 \u00ac(P x)} \u22a2 \u2203x. \u00ac(R x)\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_21a:\r\n  \"\u27e6\u2200x. P x \u2228 Q x; \u2203x. \u00ac(Q x); \u2200x. R x \u27f6 \u00ac(P x)\u27e7 \u27f9 \u2203x. \u00ac(R x)\" \r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_21b:\r\n  assumes \"\u2200x. P x \u2228 Q x\" \r\n          \"\u2203x. \u00ac(Q x)\" \r\n          \"\u2200x. R x \u27f6 \u00ac(P x)\"\r\n  shows   \"\u2203x. \u00ac(R x)\" \r\nproof -\r\n  obtain a where \"\u00ac(Q a)\" using assms(2) ..\r\n  have \"P a \u2228 Q a\" using assms(1) ..\r\n  hence \"P a\"\r\n  proof\r\n    assume \"P a\"\r\n    thus \"P a\" .\r\n  next\r\n    assume \"Q a\"\r\n    with `\u00ac(Q a)` show \"P a\" ..\r\n  qed\r\n  hence \"\u00ac\u00ac(P a)\" by (rule notnotI)\r\n  have \"R a \u27f6 \u00ac(P a)\" using assms(3) ..\r\n  hence \"\u00ac(R a)\" using `\u00ac\u00ac(P a)` by (rule mt)\r\n  thus \"\u2203x. \u00ac(R x)\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_21c:\r\n  assumes \"\u2200x. P x \u2228 Q x\" \r\n          \"\u2203x. \u00ac(Q x)\" \r\n          \"\u2200x. R x \u27f6 \u00ac(P x)\"\r\n  shows   \"\u2203x. \u00ac(R x)\" \r\nproof -\r\n  obtain a where \"\u00ac(Q a)\" using assms(2) by (rule exE)\r\n  have \"P a \u2228 Q a\" using assms(1) by (rule allE)\r\n  hence \"P a\"\r\n  proof (rule disjE)\r\n    assume \"P a\"\r\n    thus \"P a\" by this\r\n  next\r\n    assume \"Q a\"\r\n    with `\u00ac(Q a)` show \"P a\" by (rule notE)\r\n  qed\r\n  hence \"\u00ac\u00ac(P a)\" by (rule notnotI)\r\n  have \"R a \u27f6 \u00ac(P a)\" using assms(3) by (rule allE)\r\n  hence \"\u00ac(R a)\" using `\u00ac\u00ac(P a)` by (rule mt)\r\n  thus \"\u2203x. \u00ac(R x)\" by (rule exI)\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 32. Demostrar o refutar\r\n       \u2203x y. R x y \u2228 R y x; \u00ac(\u2203x. R x x)\u27e7 \u27f9 \u2203x y. x \u2260 y\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_32a:\r\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\r\n  assumes \"\u2203x y. R x y \u2228 R y x\"\r\n          \"\u00ac(\u2203x. R x x)\"\r\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\r\nusing assms\r\nby metis\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_32b:\r\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\r\n  assumes \"\u2203x y. R x y \u2228 R y x\"\r\n          \"\u00ac(\u2203x. R x x)\"\r\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\r\nproof -\r\n  obtain a where \"\u2203y. R a y \u2228 R y a\" using assms(1) ..\r\n  then obtain b where \"R a b \u2228 R b a\" ..\r\n  hence \"a \u2260 b\"\r\n  proof\r\n    assume \"R a b\"\r\n    show \"a \u2260 b\"\r\n    proof\r\n      assume \"a = b\"\r\n      hence \"R b b\" using `R a b` by (rule subst)\r\n      hence \"\u2203x. R x x\" ..\r\n      with assms(2) show False ..\r\n    qed\r\n  next\r\n    assume \"R b a\"\r\n    show \"a \u2260 b\"\r\n    proof\r\n      assume \"a = b\"\r\n      hence \"R a a\" using `R b a` by (rule ssubst)\r\n      hence \"\u2203x. R x x\" ..\r\n      with assms(2) show False ..\r\n    qed\r\n  qed\r\n  hence \"\u2203y. a \u2260 y\" ..\r\n  thus \"\u2203(x::'c) y. x \u2260 y\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_32c:\r\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\r\n  assumes \"\u2203x y. R x y \u2228 R y x\"\r\n          \"\u00ac(\u2203x. R x x)\"\r\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\r\nproof -\r\n  obtain a where \"\u2203y. R a y \u2228 R y a\" using assms(1) by (rule exE)\r\n  then obtain b where \"R a b \u2228 R b a\" by (rule exE)\r\n  hence \"a \u2260 b\"\r\n  proof (rule disjE)\r\n    assume \"R a b\"\r\n    show \"a \u2260 b\"\r\n    proof (rule notI)\r\n      assume \"a = b\"\r\n      hence \"R b b\" using `R a b` by (rule subst)\r\n      hence \"\u2203x. R x x\" by (rule exI)\r\n      with assms(2) show False by (rule notE)\r\n    qed\r\n  next\r\n    assume \"R b a\"\r\n    show \"a \u2260 b\"\r\n    proof (rule notI)\r\n      assume \"a = b\"\r\n      hence \"R a a\" using `R b a` by (rule ssubst)\r\n      hence \"\u2203x. R x x\" by (rule exI)\r\n      with assms(2) show False by (rule notE)\r\n    qed\r\n  qed\r\n  hence \"\u2203y. a \u2260 y\" by (rule exI)\r\n  thus \"\u2203(x::'c) y. x \u2260 y\" by (rule exI)\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 35. Demostrar o refutar\r\n     {\u2200y. Q a y, \r\n      \u2200x y. Q x y \u27f6 Q (s x) (s y)} \r\n     \u22a2 \u2203z. Qa z \u2227 Q z (s (s a))\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_35a:\r\n  \"\u27e6\u2200y. Q a y; \u2200x y. Q x y \u27f6 Q (s x) (s y)\u27e7 \u27f9 \u2203z. Q a z \u2227 Q z (s (s a))\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructura es\"\r\nlemma ejercicio_35b:\r\n  assumes \"\u2200y. Q a y\" \r\n          \"\u2200x y. Q x y \u27f6 Q (s x) (s y)\" \r\n  shows   \"\u2203z. Q a z \u2227 Q z (s (s a))\"\r\nproof - \r\n  have \"Q a (s a)\" using assms(1) ..\r\n  have \"\u2200y. Q a y \u27f6 Q (s a) (s y)\" using assms(2) ..\r\n  hence \"Q a (s a) \u27f6 Q (s a) (s (s a))\" ..\r\n  hence \"Q (s a) (s (s a))\" using `Q a (s a)` ..\r\n  with `Q a (s a)` have \"Q a (s a) \u2227 Q (s a) (s (s a))\" ..\r\n  thus \"\u2203z. Q a z \u2227 Q z (s (s a))\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_35c:\r\n  assumes \"\u2200y. Q a y\" \r\n          \"\u2200x y. Q x y \u27f6 Q (s x) (s y)\" \r\n  shows   \"\u2203z. Q a z \u2227 Q z (s (s a))\"\r\nproof - \r\n  have \"Q a (s a)\" using assms(1) by (rule allE)\r\n  have \"\u2200y. Q a y \u27f6 Q (s a) (s y)\" using assms(2) by (rule allE)\r\n  hence \"Q a (s a) \u27f6 Q (s a) (s (s a))\" by (rule allE)\r\n  hence \"Q (s a) (s (s a))\" using `Q a (s a)` by (rule mp)\r\n  with `Q a (s a)` have \"Q a (s a) \u2227 Q (s a) (s (s a))\" by (rule conjI)\r\n  thus \"\u2203z. Q a z \u2227 Q z (s (s a))\" by (rule exI)\r\nqed\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha explicado c\u00f3mo demostrar mediante deducci\u00f3n natural teoremas de primer orden con Isabelle\/HOL. En concreto, se han visto los ejercicios 13, 15, 16, 19, 21, 32 y 35 de la relaci\u00f3n 6. Los ejercicios y sus soluciones se muestran a continuaci\u00f3n:<\/p>\n","protected":false},"author":2,"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,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[234],"tags":[144,303,189],"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\/4239"}],"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=4239"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4239\/revisions"}],"predecessor-version":[{"id":4240,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4239\/revisions\/4240"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4239"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4239"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4239"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}