{"id":6475,"date":"2019-02-07T18:42:51","date_gmt":"2019-02-07T17:42:51","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6475"},"modified":"2019-02-09T09:05:33","modified_gmt":"2019-02-09T08:05:33","slug":"ra2018-definiciones-inductivas-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2018-definiciones-inductivas-en-isabellehol\/","title":{"rendered":"RA2018: Definiciones inductivas en IsabelleHOL"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-18\">Razonamiento autom\u00e1tico<\/a> se ha estudiado c\u00f3mo demostrar en Isabelle la correcci\u00f3n de un compilador de expresiones aritm\u00e9ticas.<\/p>\n<p>La clase se ha basado en la siguiente teor\u00eda Isabelle<\/p>\n<pre lang=\"isar\">\nchapter {* Tema 11: Definiciones inductivas *}\n\ntheory T11_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 autom\u00e1tica es\u203a\nlemma dobles_son_pares [intro!]: \n  \"2*k \u2208 par\"\nby (induct k) auto\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma dobles_son_pares_2:\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\"\nby 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 \u20391\u00aa demostraci\u00f3n (detallada)\u203a\nlemma par_imp_even: \n  \"n \u2208 par \u27f9 even n\"\nproof (induction rule: par.induct)\n  show \"2 dvd (0::nat)\" by (simp_all add: dvd_def)\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 auto\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 (con arith)\u203a\nlemma par_imp_even_2: \n  \"n \u2208 par \u27f9 even n\"\nproof (induction rule: par.induct)\n  show \"even (0::nat)\" by (simp_all add: dvd_def)\nnext\n  fix n::nat\n  assume H1: \"n \u2208 par\" and\n         H2: \"even n\"\n  then show \"even (Suc (Suc n))\" by (auto simp add: dvd_def, arith)\nqed\n\n\u2015 \u20393\u00aa demostraci\u00f3n (autom\u00e1tica)\u203a\nlemma par_imp_even_3: \n  \"n \u2208 par \u27f9 even n\"\nby (induction rule:par.induct) (auto simp add: dvd_def, arith)\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)\"\nby (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) \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 autom\u00e1tica es\u203a\nlemma par_imp_par_menos_2: \n  \"n \u2208 par \u27f9 n - 2 \u2208 par\"\nby (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 estructurada es\u203a\nlemma\n  assumes \"Suc (Suc n) \u2208 par\" \n  shows   \"n \u2208 par\"\nproof -\n  have \"Suc (Suc n) - 2 \u2208 par\" using assms by (rule par_imp_par_menos_2)\n  then show \"n \u2208 par\" by simp \nqed\n\n\u2015 \u2039La demostraci\u00f3n aplicativa es\u203a\nlemma \n  \"Suc (Suc n) \u2208 par \u27f9 n \u2208 par\"\napply (drule par_imp_par_menos_2) \napply simp\ndone\n\n(* Comentar el uso de drule *)\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\"\nby (drule par_imp_par_menos_2, simp)\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)\"\nby (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\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<p>Como ejercicio se propuso la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/RA2018\/index.php\/R8\">relaci\u00f3n 8<\/a> sobre gram\u00e1ticas libres de contexto.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo demostrar en Isabelle la correcci\u00f3n de un compilador de expresiones aritm\u00e9ticas. La clase se ha basado en la siguiente teor\u00eda Isabelle chapter {* Tema 11: Definiciones inductivas *} theory T11_Definiciones_inductivas imports Main begin section {* El conjunto&#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":[322],"tags":[144,323],"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\/6475"}],"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=6475"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6475\/revisions"}],"predecessor-version":[{"id":6481,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6475\/revisions\/6481"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6475"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6475"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6475"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}