{"id":4624,"date":"2014-11-27T20:51:40","date_gmt":"2014-11-27T19:51:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4624"},"modified":"2014-11-28T13:56:05","modified_gmt":"2014-11-28T12:56:05","slug":"ra2014-verificacion-de-la-ordenacion-por-insercion-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2014-verificacion-de-la-ordenacion-por-insercion-con-isabellehol\/","title":{"rendered":"RA2014: Verificaci\u00f3n de la ordenaci\u00f3n por inserci\u00f3n con Isabelle\/HOL"},"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-14\">Razonamiento autom\u00e1tico<\/a> se ha estudiado c\u00f3mo demostrar la correcci\u00f3n del algoritmo de ordenaci\u00f3n por inserci\u00f3n.<\/p>\n<p>La correspondiente teor\u00eda Isabelle\/HOL se muestra a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* T5a: Verificaci\u00f3n de la ordenaci\u00f3n por inserci\u00f3n *}\n\ntheory T5a\nimports Main\nbegin\n\ntext {*\n  En este de tema se define el algoritmo de ordenaci\u00f3n de listas \n  por inserci\u00f3n y se demuestra que es correcto. Se plantea como una \n  \u2759sucesi\u00f3n de ejercicios.\n*}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 1. Definir la funci\u00f3n\n     inserta :: int \u21d2 int list \u21d2 int list\n  tal que (inserta a xs) es la lista obtenida insertando a delante del\n  primer elemento de xs que es mayor o igual que a. Por ejemplo,\n     inserta 3 [2,5,1,7] = [2,3,5,1,7]\n  ------------------------------------------------------------------ *}\n\nfun inserta :: \"int \u21d2 int list \u21d2 int list\" where\n  \"inserta a []     = [a]\"\n| \"inserta a (x#xs) = (if a \u2264 x then a#x#xs \n                                else x # inserta a xs)\"\n\nvalue \"inserta 3 [2,5,1,7]\" -- \"= [2,3,5,1,7]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n\n     ordena :: int list \u21d2 int list\n  tal que (ordena xs) es la lista obtenida ordenando xs por inserci\u00f3n. \n  Por ejemplo, \n     ordena [3,2,5,3] = [2,3,3,5]\n  ------------------------------------------------------------------ *}\n\nfun ordena :: \"int list \u21d2 int list\" where\n  \"ordena []     = []\"\n| \"ordena (x#xs) = inserta x (ordena xs)\"\n\nvalue \"ordena [3,2,5,3]\" -- \"[2,3,3,5]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 3. Definir la funci\u00f3n\n     menor :: int \u21d2 int list \u21d2 bool\n  tal que (menor a xs) se verifica si a es menor o igual que todos los\n  elementos de xs.Por ejemplo,  \n     menor 2 [3,2,5] = True\n     menor 2 [3,0,5] = False\n  ------------------------------------------------------------------ *}\n\nfun menor :: \"int \u21d2 int list \u21d2 bool\" where\n  \"menor a []     = True\"\n| \"menor a (x#xs) = (a \u2264 x \u2227 menor a xs)\"\n\nvalue \"menor 2 [3,2,5]\" -- \"= True\"\nvalue \"menor 2 [3,0,5]\" -- \"= False\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 4. Definir la funci\u00f3n\n     ordenada :: int list \u21d2 bool\n  tal que (ordenada xs) se verifica si xs es una lista ordenada de\n  manera creciente. Por ejemplo,  \n     ordenada [2,3,3,5] = True \n     ordenada [2,4,3,5] = False \n  ------------------------------------------------------------------ *}\n\nfun ordenada :: \"int list \u21d2 bool\" where\n  \"ordenada []     = True\"\n| \"ordenada (x#xs) = (menor x xs & ordenada xs)\"\n\nvalue \"ordenada [2,3,3,5]\" -- \"= True\" \nvalue \"ordenada [2,4,3,5]\" -- \"= False\" \n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 5. Demostrar que si y es una cota inferior de zs y x \u2264 y,\n  entonces x es una cota inferior de zs.\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma menor_menor: \n  assumes \"x \u2264 y\"  \n  shows   \"menor y zs \u27f6 menor x zs\"\nusing assms\nby (induct zs) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma menor_menor_2: \n  assumes \"x \u2264 y\"  \n  shows   \"menor y zs \u27f6 menor x zs\"\nproof (induct zs)\n  show \"menor y [] \u27f6 menor x []\" by simp\nnext\n  fix z zs\n  assume HI: \"menor y zs \u27f6 menor x zs\"  \n  show \"menor y (z # zs) \u27f6 menor x (z # zs)\"\n  proof\n    assume sup: \"menor y (z # zs)\"\n    show \"menor x (z # zs)\"\n    proof (simp only: menor.simps(2))\n      show \"x \u2264 z \u2227 menor x zs\"\n      proof\n          have \"x \u2264 y\" using assms .\n          also have \"y \u2264 z\" using sup by simp\n          finally show \"x \u2264 z\" .\n      next\n        have \"menor y zs\" using sup by simp\n        with HI show \"menor x zs\" by simp\n      qed\n    qed\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 6. Demostrar el siguiente teorema de correcci\u00f3n: x es una\n  cota inferior de la lista obtenida insertando y en zs syss x \u2264 y y x\n  es una cota inferior de zs.\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma menor_inserta:\n  \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\nby (induct zs) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma menor_inserta_2: \n  \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\nproof (induct zs)\n  show \"menor x (inserta y []) = (x \u2264 y \u2227 menor x [])\" by simp\nnext \n  fix z zs\n  assume HI: \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\n  show \"menor x (inserta y (z#zs)) = (x \u2264 y \u2227 menor x (z#zs))\" \n  proof (cases \"y \u2264 z\")\n    assume \"y \u2264 z\"\n    hence \"menor x (inserta y (z#zs)) = menor x (y#z#zs)\" by simp\n    also have \"\u2026 = (x \u2264 y \u2227 menor x (z#zs))\" by simp\n    finally show ?thesis by simp\n  next\n    assume \"\u00ac(y \u2264 z)\"\n    hence \"menor x (inserta y (z#zs)) = \n           menor x (z # inserta y zs)\" by simp\n    also have \"\u2026 = (x \u2264 z \u2227 menor x (inserta y zs))\" by simp\n    also have \"\u2026 = (x \u2264 z \u2227 x \u2264 y \u2227 menor x zs)\" using HI by simp\n    also have \"\u2026 = (x \u2264 y \u2227 menor x (z#zs))\" by auto\n    finally show ?thesis by simp\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 6. Demostrar que al insertar un elemento la lista obtenida\n  est\u00e1 ordenada syss lo estaba la original.\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ordenada_inserta:\n  \"ordenada (inserta a xs) = ordenada xs\"\nby (induct xs) (auto simp add: menor_menor menor_inserta)\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ordenada_inserta_2:\n  \"ordenada (inserta a xs) = ordenada xs\"\nproof (induct xs)\n  show \"ordenada (inserta a []) = ordenada []\" by simp\nnext\n  fix x xs\n  assume HI: \"ordenada (inserta a xs) = ordenada xs\" \n  show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\" \n  proof (cases \"a \u2264 x\")\n    assume \"a \u2264 x\"\n    hence \"ordenada (inserta a (x # xs)) = \n           ordenada (a # x # xs)\" by simp\n    also have \"\u2026 = (menor a (x#xs) \u2227 ordenada (x # xs))\" by simp\n    also have \"\u2026 = ordenada (x # xs)\"  \n      using `a \u2264 x`  by (auto simp add: menor_menor)\n    finally show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\" \n      by simp\n  next\n    assume \"\u00ac(a \u2264 x)\"\n    hence \"ordenada (inserta a (x # xs)) = \n           ordenada (x # inserta a xs)\" by simp\n    also have \"\u2026 = (menor x (inserta a xs) \u2227 ordenada (inserta a xs))\" \n      by simp\n    also have \"\u2026 = (menor x (inserta a xs) \u2227 ordenada xs)\" \n      using HI by simp\n    also have \"\u2026 = (menor x xs \u2227 ordenada xs)\" \n      using `\u00ac(a \u2264 x)` by (simp add: menor_inserta)\n    also have \"\u2026 = ordenada (x # xs)\" by simp\n    finally show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\" \n      by simp\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 7. Demostrar que, para toda lista xs, (ordena xs) est\u00e1\n  ordenada. \n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\ntheorem ordenada_ordena:\n  \"ordenada (ordena xs)\"\nby (induct xs) (auto simp add: ordenada_inserta)\n\n-- \"La demostraci\u00f3n estructurada es\"\ntheorem ordenada_ordena_2:\n  \"ordenada (ordena xs)\"\nproof (induct xs) \n  show \"ordenada (ordena [])\" by simp\nnext\n  fix x xs\n  assume \"ordenada (ordena xs)\" \n  then have \"ordenada (inserta x (ordena xs))\" \n    by (simp add: ordenada_inserta)  \n  then show \"ordenada (ordena (x # xs))\" by simp\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Nota. El teorema anterior no garantiza que ordena sea correcta, ya que\n  puede que (ordena xs) no tenga los mismos elementos que xs. Por\n  ejemplo, si se define (ordena xs) como [] se tiene que (ordena xs)\n  est\u00e1 ordenada pero no es una ordenaci\u00f3n de xs. \n\n  Para garantizarlo, definimos la funci\u00f3n cuenta.\n  ------------------------------------------------------------------ *}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 8. Definir la funci\u00f3n\n     cuenta :: int list \u21d2 int \u21d2 nat\n  tal que (cuenta xs y) es el n\u00famero de veces que aparece el elemento y\n  en la lista xs. Por ejemplo, \n     cuenta [1,3,4,3,5] 3 = 2\n  ------------------------------------------------------------------ *}\n\nfun cuenta :: \"int list \u21d2 int \u21d2 nat\" where\n  \"cuenta []     y = 0\"\n| \"cuenta (x#xs) y = (if x=y then Suc(cuenta xs y) else cuenta xs y)\"\n\nvalue \"cuenta [1,3,4,3,5] 3\" -- \"= 2\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 9. Demostrar que el n\u00famero de veces que aparece y en \n  (inserta x xs) es \n  * uno m\u00e1s el n\u00famero de veces que aparece en xs, si y = x; \n  * el n\u00famero de veces que aparece en xs, si y \u2260 x; \n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma cuenta_inserta:\n  \"cuenta (inserta x xs) y =\n   (if x=y then Suc (cuenta xs y) else cuenta xs y)\"\nby (induct xs) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 10. Demostrar que el n\u00famero de veces que aparece y en \n  (ordena xs) es el n\u00famero de veces que aparece en xs.\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\ntheorem cuenta_ordena:\n  \"cuenta (ordena xs) y = cuenta xs y\"\nby (induct xs) (auto simp add: cuenta_inserta)\n\n-- \"La demostraci\u00f3n estructurada es\"\ntheorem cuenta_ordena_2:\n  \"cuenta (ordena xs) y = cuenta xs y\"\nproof (induct xs)\n  show \"cuenta (ordena []) y = cuenta [] y\" by simp\nnext\n  fix x xs\n  assume HI: \"cuenta (ordena xs) y = cuenta xs y\"\n  show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" \n  proof (cases \"x = y\")\n    assume \"x = y\"\n    have \"cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y\" by simp\n    also have \"\u2026 = Suc (cuenta (ordena xs) y)\" using `x = y` by (simp add: cuenta_inserta) \n    also have \"\u2026 = Suc (cuenta xs y)\" using HI by simp\n    also have \"\u2026 = cuenta (x # xs) y\" using `x = y` by simp\n    finally show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" by simp\n  next\n    assume \"x \u2260 y\"\n    have \"cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y\" by simp\n    also have \"\u2026 = cuenta (ordena xs) y\" using `x \u2260 y` by (simp add: cuenta_inserta) \n    also have \"\u2026 = cuenta xs y\" using HI by simp\n    also have \"\u2026 = cuenta (x # xs) y\" using `x \u2260 y` by simp\n    finally show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" by simp\n  qed\nqed\n\nend\n<\/pre>\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 la correcci\u00f3n del algoritmo de ordenaci\u00f3n por inserci\u00f3n. La correspondiente teor\u00eda Isabelle\/HOL se muestra 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":[240],"tags":[144,307],"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\/4624"}],"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=4624"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4624\/revisions"}],"predecessor-version":[{"id":4626,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4624\/revisions\/4626"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4624"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4624"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4624"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}