{"id":7199,"date":"2020-05-28T13:05:07","date_gmt":"2020-05-28T11:05:07","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7199"},"modified":"2020-05-28T13:05:07","modified_gmt":"2020-05-28T11:05:07","slug":"lmf2019-definiciones-inductivas-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2019-definiciones-inductivas-en-isabelle-hol\/","title":{"rendered":"LMF2019: Definiciones inductivas en Isabelle\/HOL"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado c\u00f3mo definir en Isabelle\/HOL conjuntos y relaciones inductivas y c\u00f3mo demostrar sus propiedades.<\/p>\n<p>La clase se ha dado mediante videoconferencia y el v\u00eddeo correspondiente es<\/p>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/IWAuIlQDebk\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/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 9: Definiciones inductivas\u203a\n\ntheory T9_Definiciones_inductivas\nimports Main\nbegin\n\nsection \u2039Definici\u00f3n inductiva del conjunto de los n\u00fameros pares\u203a\n\ntext \u2039\n  \u00b7 El conjunto de los n\u00fameros pares se define inductivamente como el\n    menor conjunto que contiene al 0 y es cerrado por la operaci\u00f3n (+2).\n\n  \u00b7 El conjunto de los n\u00fameros pares tambi\u00e9n puede definirse como los \n    naturales divisible por 2.\n\n  \u00b7 Veremos c\u00f3mo se escriben las dos definiciones en Isabelle\/HOL y c\u00f3mo\n    se demuestra su equivalencia.\u203a\n\ninductive_set par :: \"nat set\" where\n  cero: \"0 \u2208 par\" \n| paso: \"n \u2208 par \u27f9 (Suc (Suc n)) \u2208 par\"\n\ntext \u2039La definici\u00f3n inductiva genera varios teoremas:\n   \u00b7 par.cero:   0 \u2208 par\n   \u00b7 par.paso:   n \u2208 par \u27f9 Suc (Suc n) \u2208 par\n   \u00b7 par.simps:  (a \u2208 par) = (a = 0 \u2228 (\u2203n. a = Suc (Suc n) \u2227 n \u2208 par))\n\u203a\n\nthm par.cero\nthm par.paso\nthm par.simps\n\nsubsection \u2039Uso de las reglas de introducci\u00f3n\u203a\n\ntext \u2039Lema: Los n\u00fameros de la forma 2*k son pares.\u203a\n\n\u2015 \u2039La demostraci\u00f3n aplicativa es\u203a\nlemma dobles_son_pares: \n  \"2*k \u2208 par\"\n  apply (induct k) \n     (* 1. 2 * 0 \u2208 par\n        2. \u22c0k. 2 * k \u2208 par \u27f9 2 * Suc k \u2208 par *)\n   apply (simp add: par.cero)\n     (* \u22c0k. 2 * k \u2208 par \u27f9 2 * Suc k \u2208 par *)\n  apply (simp add: par.paso)\n  done\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma dobles_son_pares_2: \n  \"2*k \u2208 par\"\n  by (induct k) (simp_all add: par.cero par.paso)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma dobles_son_pares_3:\n  \"2*k \u2208 par\"\nproof (induct k)\n  show \"2 * 0 \u2208 par\" \n    by (simp add: par.cero)\nnext\n  show \"\u22c0k. 2 * k \u2208 par \u27f9 2 * Suc k \u2208 par\" \n    by (simp add: par.paso)\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma dobles_son_pares_4:\n  \"2*k \u2208 par\"\nproof (induct k) \n  have \"2 * 0 = (0::nat)\"\n    by (simp only: mult_0_right)\n  then show \"2 * 0 \u2208 par\"\n    by (simp only: par.cero)\nnext\n  fix k :: \"nat\" \n  assume \"2 * k \u2208 par\" \n  have \"2 * Suc k = Suc (Suc (2 * k))\" \n  proof -\n    have \"2 * Suc k = 2 + 2 * k\"\n      by (simp only: mult_Suc_right)\n    also have \"\u2026 = Suc (Suc (2 * k))\"\n      by (simp only: add_2_eq_Suc)\n    finally show \"2 * Suc k = Suc (Suc (2 * k))\"\n      by this\n  qed\n  then show \"2 * Suc k \u2208 par\"\n    using \u20392 * k \u2208 par\u203a\n    by (simp only: par.paso)\nqed\n\ntext \u2039Nota: Nuestro objetivo es demostrar la equivalencia de la \n  definici\u00f3n anterior y la definici\u00f3n mediante divisibilidad (even).\n  \n  Lema: Si n es divisible por 2, entonces es par.\u203a\n\n\u2015 \u2039La demostraci\u00f3n declarativa detallada es\u203a\nlemma \"even n \u27f9 n \u2208 par\" \nproof -\n  assume \"even n\"\n  then have \"\u2203k. n = 2*k\"\n    by (simp only: dvd_def)\n  then obtain k where \"n = 2*k\"\n    by (rule exE)\n  then show \"n \u2208 par\"\n    by (simp only: dobles_son_pares)\nqed\n\n\u2015 \u2039La demostaci\u00f3n autom\u00e1tica es\u203a\nlemma even_imp_par: \"even n \u27f9 n \u2208 par\"\n  by (auto simp only: dobles_son_pares)\n\nsubsection \u2039Regla de inducci\u00f3n\u203a \n\ntext \u2039Entre las reglas generadas por la defini\u00f3n de par est\u00e1 la de\n  inducci\u00f3n:\n  \u00b7 par.induct: \u27e6 x \u2208 par; \n                 P 0; \n                 \u22c0n. \u27e6n \u2208 par; P n\u27e7 \u27f9 P (Suc (Suc n))\u27e7 \n                \u27f9 P x\n\u203a\n\nthm par.induct\n\ntext \u2039Lema: Los n\u00fameros pares son divisibles por 2.\u203a \n\n\u2015 \u2039Demostraci\u00f3n aplicativa\u203a\nlemma par_imp_even: \n  \"n \u2208 par \u27f9 even n\"\n  apply (induction rule: par.induct)\n     (* 1. even 0\n        2. \u22c0n. \u27e6n \u2208 par; even n\u27e7 \u27f9 even (Suc (Suc n)) *)\n   apply (simp only: dvd_def)\n     (* 1. \u2203k. 0 = 2 * k\n        2. \u22c0n. \u27e6n \u2208 par; even n\u27e7 \u27f9 even (Suc (Suc n)) *)\n   apply (rule_tac x=0 in exI)\n     (* 1. 0 = 2 * 0\n        2. \u22c0n. \u27e6n \u2208 par; even n\u27e7 \u27f9 even (Suc (Suc n)) *)\n   apply simp\n     (* \u22c0n. \u27e6n \u2208 par; even n\u27e7 \u27f9 even (Suc (Suc n)) *)\n  apply (simp only: dvd_def)\n     (* \u22c0n. \u27e6n \u2208 par; \u2203k. n = 2 * k\u27e7 \u27f9 \u2203k. Suc (Suc n) = 2 * k *)\n  apply (erule exE)\n     (* \u22c0n k. \u27e6n \u2208 par; n = 2 * k\u27e7 \u27f9 \u2203k. Suc (Suc n) = 2 * k*)\n  apply (rule_tac x=\"k+1\" in exI)\n     (* \u22c0n k. \u27e6n \u2208 par; n = 2 * k\u27e7 \u27f9 Suc (Suc n) = 2 * (k + 1) *)\n  apply simp\n     (* *)\n  done\n\n\u2015 \u20392\u00aa demostraci\u00f3n aplicativa\u203a\nlemma par_imp_even_2: \n  \"n \u2208 par \u27f9 even n\"\n  apply (induction rule: par.induct)\n     (* 1. even 0\n        2. \u22c0n. \u27e6n \u2208 par; even n\u27e7 \u27f9 even (Suc (Suc n)) *)\n   apply simp_all\n     (* *)\n  done\n\n\u2015 \u2039Demostraci\u00f3n autom\u00e1tica\u203a\nlemma par_imp_even_3: \n  \"n \u2208 par \u27f9 even n\"\n  by (induction rule: par.induct) simp_all\n\n\u2015 \u20392\u00aa demostraci\u00f3n declarativa\u203a\nlemma par_imp_even_4: \n  \"n \u2208 par \u27f9 even n\"\nproof (induction rule: par.induct)\n  show \"even 0\" \n    by simp\nnext\n  fix n :: nat\n  assume H1: \"n \u2208 par\" and\n         H2: \"even n\"\n  then show \"even (Suc (Suc n))\" \n    by simp\nqed\n\n\u2015 \u2039Demostraci\u00f3n declarativa detallada\u203a\nlemma par_imp_even_5: \n  \"n \u2208 par \u27f9 even n\"\nproof (induction rule: par.induct)\n  show \"even 0\" \n    by (simp only: even_zero)\nnext\n  fix n :: nat\n  assume H1: \"n \u2208 par\" and\n         H2: \"even n\"\n  have \"\u2203k. n = 2*k\" \n    using H2 by (simp only: dvd_def)\n  then obtain k where \"n = 2*k\" \n    by (rule exE)\n  then have \"Suc (Suc n) = 2*(k+1)\" \n  proof -\n    have \"Suc (Suc n) = 2 + n\"\n      by (simp only: add_2_eq_Suc)\n    also have \"\u2026 = 2 + 2 * k\"\n      by (simp only: \u2039n = 2 * k\u203a)\n    also have \"\u2026 = 2 * Suc k\"\n      by (simp only: mult_Suc_right)\n    also have \"\u2026 = 2 * (k + 1)\"\n      by (simp only: Suc_eq_plus1)\n    finally show \"Suc (Suc n) = 2*(k+1)\"\n      by this\n  qed\n  then have \"\u2203k. Suc (Suc n) = 2*k\" \n    by (rule exI)\n  then show \"even (Suc (Suc n))\" \n    by (simp only: dvd_def)\nqed\n\ntext \u2039Lema: Un n\u00famero n es par syss es divisible por 2.\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\ntheorem par_iff_even: \"(n \u2208 par) = (even n)\" \nproof (rule iffI)\n  show \"n \u2208 par \u27f9 even n\"\n    by (rule par_imp_even)\nnext\n  show \"even n \u27f9 n \u2208 par\"\n    by (rule even_imp_par)\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\ntheorem par_iff_even_2: \"(n \u2208 par) = (even n)\"\n  by (auto simp only: par_imp_even even_imp_par)\n\nsubsection \u2039Generalizaci\u00f3n y regla de inducci\u00f3n\u203a\n\ntext \u2039\n  \u00b7 Antes de aplicar inducci\u00f3n se debe de generalizar la f\u00f3rmula a\n    probar.\n \n  \u00b7 Vamos a ilustrar el principio anterior en el caso de los conjuntos\n    inductivamente definidos, con el siguiente ejemplo: si n+2 es par,\n    entonces n tambi\u00e9n lo es.\n\n  \u00b7 El siguiente intento falla:\u203a\n\nlemma \"Suc (Suc n) \u2208 par \u27f9 n \u2208 par\"\n  apply (erule par.induct) \n    (* 1. n \u2208 par\n       2. \u22c0na. \u27e6na \u2208 par; n \u2208 par\u27e7 \u27f9 n \u2208 par *)\noops\n\ntext \u2039En el intento anterior, los subobjetivos generados son\n     1. n \u2208 par\n     2. \u22c0na. \u27e6na \u2208 par; n \u2208 par\u27e7 \u27f9 n \u2208 par\n  que no se pueden demostrar.\n\n  Se ha perdido la informaci\u00f3n sobre Suc (Suc n).\u203a\n\ntext \u2039Reformulaci\u00f3n del lema: Si n es par, entonces n-2 tambi\u00e9n lo es.\u203a\n\n\u2015 \u2039La demostraci\u00f3n aplicativa es\u203a\nlemma par_imp_par_menos: \n  \"n \u2208 par \u27f9 n - 2 \u2208 par\"\n  apply (induction rule: par.induct) \n     (* 1. 0 - 2 \u2208 par\n        2. \u22c0n. \u27e6n \u2208 par; n - 2 \u2208 par\u27e7 \u27f9 Suc (Suc n) - 2 \u2208 par *)\n   apply (simp add: par.cero)\n  apply (simp add: par.paso)\n     (* *)\n  done\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma par_imp_par_menos_2: \n  \"n \u2208 par \u27f9 n - 2 \u2208 par\"\n  by (induction rule: par.induct) (auto simp add: par.cero par.paso)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma \"n \u2208  par \u27f9 n - 2 \u2208 par\"\nproof (induction rule: par.induct)\n  show \"0 - 2 \u2208 par\" \n    by (auto simp add: par.cero)\nnext\n  show \"\u22c0n. \u27e6n \u2208 par; n - 2 \u2208 par\u27e7 \u27f9 Suc (Suc n) - 2 \u2208 par\" \n    by (auto simp add: par.paso)\nqed\n\ntext \u2039Con el lema anterior se puede demostrar el original.\u203a\n\n\u2015 \u2039La demostraci\u00f3n aplicativa es\u203a\nlemma \n  \"Suc (Suc n) \u2208 par \u27f9 n \u2208 par\"\n  apply (drule par_imp_par_menos_2)\n    (* Suc (Suc n) - 2 \u2208 par \u27f9 n \u2208 par *)\n  apply simp\n    (* *)\n  done\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma Suc_Suc_par_imp_par: \n  \"Suc (Suc n) \u2208 par \u27f9 n \u2208 par\" \n  by (drule par_imp_par_menos_2, simp)\n\n\u2015 \u2039La demostraci\u00f3n declarativa es\u203a\nlemma\n  assumes \"Suc (Suc n) \u2208 par\" \n  shows   \"n \u2208 par\"\nproof -\n  have \"Suc (Suc n) - 2 \u2208 par\" \n    using assms by (rule par_imp_par_menos_2)\n  then show \"n \u2208 par\" \n    by simp \nqed\n\ntext \u2039Lemma. Un n\u00famero natural n es par syss n+2 es par.\u203a\n\nlemma \"((Suc (Suc n)) \u2208 par) = (n \u2208 par)\"\n  using Suc_Suc_par_imp_par par.paso by blast\n\nsection \u2039Definiciones mutuamente inductivas\u203a\n\ntext \u2039Definici\u00f3n cruzada de los conjuntos inductivos de los pares y de los \n  impares:\u203a\n\ninductive_set\n  Pares    :: \"nat set\" and\n  Impares  :: \"nat set\"\nwhere\n  ceroP:    \"0 \u2208 Pares\"\n| ParesI:   \"n \u2208 Impares \u27f9 Suc n \u2208 Pares\"\n| ImparesI: \"n \u2208 Pares   \u27f9 Suc n \u2208 Impares\"\n\ntext \u2039El esquema de inducci\u00f3n generado por la definici\u00f3n anterior es\n  \u00b7 Pares_Impares.induct:\n    \u27e6P1 0; \n     \u22c0n. \u27e6n \u2208 Impares; P2 n\u27e7 \u27f9 P1 (Suc n);\n     \u22c0n. \u27e6n \u2208 Pares;   P1 n\u27e7 \u27f9 P2 (Suc n)\u27e7\n    \u27f9 (x1 \u2208 Pares \u27f6 P1 x1) \u2227 (x2 \u2208 Impares \u27f6 P2 x2)\n\u203a\n\nthm Pares_Impares.induct\n\ntext \u2039Ejemplo de demostraci\u00f3n usando el esquema anterior.\u203a\n\n\u2015 \u2039Demostraci\u00f3n aplicativa\u203a\nlemma \"(m \u2208 Pares \u27f6 even m) \u2227 (n \u2208 Impares \u27f6 even (Suc n))\"\n  apply (induction rule: Pares_Impares.induct)\n      (* 1. even 0\n         2. \u22c0n. \u27e6n \u2208 Impares; even (Suc n)\u27e7 \u27f9 even (Suc n)\n         3. \u22c0n. \u27e6n \u2208 Pares; even n\u27e7 \u27f9 even (Suc (Suc n))*)\n    apply simp_all\n      (* *)\n  done\n\n\u2015 \u2039Demostraci\u00f3n autom\u00e1tica\u203a\nlemma \"(m \u2208 Pares \u27f6 even m) \u2227 (n \u2208 Impares \u27f6 even (Suc n))\"\n  by (induction rule: Pares_Impares.induct) simp_all\n\n\u2015 \u2039La demostraci\u00f3n declarativa es\u203a\nlemma \"(m \u2208 Pares \u27f6 even m) \u2227 (n \u2208 Impares \u27f6 even (Suc n))\"\nproof (induction rule: Pares_Impares.induct)\n  show \"even 0\" \n    by simp\nnext\n  fix n :: \"nat\"\n  assume H1: \"n \u2208 Impares\" and\n         H2: \"even (Suc n)\"\n  show \"even (Suc n)\" \n    using H2 by simp\nnext\n  fix n :: \"nat\"\n  assume H1: \"n \u2208 Pares\" and\n         H2: \"even n\"\n  have \"\u2203k. n = 2*k\" \n    using H2 by (simp add: dvd_def)\n  then obtain k where \"n = 2*k\" \n    by (rule exE)\n  then have \"Suc (Suc n) = 2*(k+1)\" \n    by simp\n  then have \"\u2203k. Suc (Suc n) = 2*k\" \n    by (rule exI)\n  then show \"even (Suc (Suc n))\" \n    by (simp add: dvd_def)\nqed\n\nsection \u2039Definici\u00f3n inductiva de predicados\u203a\n\ntext \u2039Definici\u00f3n inductiva del predicado es_par tal que (es_par n) se\n  verifica si n es par.\u203a\n\ninductive es_par :: \"nat \u21d2 bool\" where\n  \"es_par 0\" \n| \"es_par n \u27f9 es_par (Suc (Suc n))\"\n\ntext \u2039Heur\u00edstica para elegir entre definir conjuntos o predicados:\n  \u00b7 si se va a combinar con operaciones conjuntistas, definir conjunto;\n  \u00b7 en caso contrario, definir predicado.\u203a\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado c\u00f3mo definir en Isabelle\/HOL conjuntos y relaciones inductivas y c\u00f3mo demostrar sus propiedades. La clase se ha dado mediante videoconferencia y el v\u00eddeo correspondiente es La teor\u00eda con los ejemplos presentados en la clase es 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":[334],"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\/7199"}],"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=7199"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7199\/revisions"}],"predecessor-version":[{"id":7200,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7199\/revisions\/7200"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7199"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7199"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7199"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}