{"id":6678,"date":"2019-05-16T12:32:17","date_gmt":"2019-05-16T10:32:17","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6678"},"modified":"2019-05-25T17:45:39","modified_gmt":"2019-05-25T15:45:39","slug":"lmf2018-definiciones-inductivas-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2018-definiciones-inductivas-en-isabelle-hol\/","title":{"rendered":"LMF2018: 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-18\">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 basado en la siguiente teor\u00eda Isabelle<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* Tema 9: Definiciones inductivas *}\n\ntheory T9_Definiciones_inductivas\nimports Main\nbegin\n\nsection {* El conjunto de los n\u00fameros pares *}\n\ntext {* \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.\n*}\n\nsubsection {* Definici\u00f3n inductiva del conjunto de los pares *}\n\ninductive_set par :: \"nat set\" where\n  cero [intro!]: \"0 \u2208 par\" \n| paso [intro!]: \"n \u2208 par \u27f9 (Suc (Suc n)) \u2208 par\"\n\ntext {*\n  \u00b7 Una definici\u00f3n inductiva est\u00e1 formada con reglas de introducci\u00f3n.\n\n  \u00b7 La 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*}\n\nsubsection {* Uso de las reglas de introducci\u00f3n *}\n\ntext {*\n  Lema: Los n\u00fameros de la forma 2*k son pares.\n*}\n\n\u2015 \u2039La demostraci\u00f3n aplicativa es\u203a\nlemma dobles_son_pares [intro!]: \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 auto\n     (* *)\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) auto\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\" by auto\nnext\n  show \"\u22c0k. 2 * k \u2208 par \u27f9 2 * Suc k \u2208 par\" by auto\nqed\n\ntext {*\n  \u00b7 Nota: Nuestro objetivo es demostrar la equivalencia de la definici\u00f3n\n    anterior y la definici\u00f3n mediante divisibilidad (even).\n  \n  \u00b7 Lema: Si n es divisible por 2, entonces es par.\n*}\n\nlemma even_imp_par: \"even n \u27f9 n \u2208 par\"\n  by auto\n\nsubsection {* Regla de inducci\u00f3n *} \n\ntext {*\n  Entre 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*}\n\ntext {*\n  Lema: Los n\u00fameros pares son divisibles por 2.\n*} \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 \u2039Demostraci\u00f3n declarativa\u203a\nlemma par_imp_even_4: \n  \"n \u2208 par \u27f9 even n\"\nproof (induction rule: par.induct)\n  show \"even 0\" by simp\nnext\n  fix n::nat\n  assume H1: \"n \u2208 par\" and\n         H2: \"even n\"\n  have \"\u2203k. n = 2*k\" using H2 by (simp add: dvd_def)\n  then obtain k where \"n = 2*k\" ..\n  then have \"Suc (Suc n) = 2*(k+1)\" by simp\n  then have \"\u2203k. Suc (Suc n) = 2*k\" ..\n  then show \"even (Suc (Suc n))\" by (simp add: dvd_def)\nqed\n\n\u2015 \u20392\u00aa demostraci\u00f3n declarativa\u203a\nlemma par_imp_even_5: \n  \"n \u2208 par \u27f9 even n\"\nproof (induction rule: par.induct)\n  show \"even 0\" 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))\" by simp\nqed\n\ntext {*\n  Lema: Un n\u00famero n es par syss es divisible por 2. \n*}\n\ntheorem par_iff_even: \"(n \u2208 par) = (even n)\"\n  by (blast intro: even_imp_par par_imp_even)\n\nsubsection{* Generalizaci\u00f3n y regla de inducci\u00f3n *}\n\ntext {*\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:\n*}\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 {*\n  En 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).\n*}\n\ntext {*\n  Reformulaci\u00f3n del lema: Si n es par, entonces n-2 tambi\u00e9n lo es.\n*}\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 auto\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\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\" by auto\nnext\n  show \"\u22c0n. \u27e6n \u2208 par; n - 2 \u2208 par\u27e7 \u27f9 Suc (Suc n) - 2 \u2208 par\" by auto\nqed\n\ntext {* \n  Con el lema anterior se puede demostrar el original.\n*}\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\" by simp \nqed\n\ntext {*\n  Lemma. Un n\u00famero natural n es par syss n+2 es par.\n*}\n\nlemma [iff]: \"((Suc (Suc n)) \u2208 par) = (n \u2208 par)\"\n  by (blast dest: Suc_Suc_par_imp_par)\n\ntext {*\n  Se usa el atributo \"iff\" porque sirve como regla de simplificaci\u00f3n.\n*}\n\nsubsection {* Definiciones mutuamente inductivas *}\n\ntext {*\n  Definici\u00f3n cruzada de los conjuntos inductivos de los pares y de los \n  impares:\n*}\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 {*\n  El 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*}\n\ntext {*\n  Ejemplo de demostraci\u00f3n usando el esquema anterior.\n*}\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 auto\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) auto\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::nat)\" by simp\nnext\n  fix n :: \"nat\"\n  assume H1: \"n \u2208 Impares\" and\n         H2: \"even (Suc n)\"\n  show \"even (Suc 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\" using H2 by (simp add: dvd_def)\n  then obtain k where \"n = 2*k\" ..\n  then have \"Suc (Suc n) = 2*(k+1)\" by auto\n  then have \"\u2203k. Suc (Suc n) = 2*k\" ..\n  then show \"even (Suc (Suc n))\" by (simp add: dvd_def)\nqed\n\nsubsection {* Definici\u00f3n inductiva de predicados *}\n\ntext {*\n  Definici\u00f3n inductiva del predicado es_par tal que (es_par n) se\n  verifica si n es par.\n*}\n\ninductive es_par :: \"nat \u21d2 bool\" where\n  \"es_par 0\" \n| \"es_par n \u27f9 es_par (Suc(Suc n))\"\n\ntext {*\n  Heur\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.\n*}\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 basado en la siguiente teor\u00eda Isabelle<\/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\/6678"}],"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=6678"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6678\/revisions"}],"predecessor-version":[{"id":6683,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6678\/revisions\/6683"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6678"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6678"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6678"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}