{"id":4627,"date":"2014-11-27T20:57:21","date_gmt":"2014-11-27T19:57:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4627"},"modified":"2014-11-28T13:58:22","modified_gmt":"2014-11-28T12:58:22","slug":"ra2014-verificacion-de-la-ordenacion-por-mezcla-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2014-verificacion-de-la-ordenacion-por-mezcla-con-isabellehol\/","title":{"rendered":"RA2014: Verificaci\u00f3n de la ordenaci\u00f3n por mezcla con 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\/m-ra-14\">Razonamiento autom\u00e1tico<\/a> se ha estudiado c\u00f3mo demostrar la correcci\u00f3n del algoritmo de ordenaci\u00f3n por mezcla.<\/p>\n<p>La correspondiente teor\u00eda Isabelle\/HOL se muestra a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* T5b: Verificaci\u00f3n de la ordenaci\u00f3n por mezcla *}\n\ntheory T5b\nimports Main\nbegin\n\ntext {*\n  En esta relaci\u00f3n de ejercicios se define el algoritmo de ordenaci\u00f3n de\n  listas por mezcla y se demuestra que es correcto.\n*}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 1. 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 2. 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 3. Definir la funci\u00f3n\n     cuenta :: int list => int => 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 => int => 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\nsection {* Ordenaci\u00f3n por mezcla *}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 4. Definir la funci\u00f3n\n     mezcla :: int list \u21d2 int list \u21d2 int list\n  tal que (mezcla xs ys) es la lista obtenida mezclando las listas\n  ordenadas xs e ys. Por ejemplo, \n     mezcla [1,2,5] [3,5,7] = [1,2,3,5,5,7]\n  ------------------------------------------------------------------ *}\n\nfun mezcla :: \"int list \u21d2 int list \u21d2 int list\" where\n  \"mezcla [] ys = ys\" \n| \"mezcla xs [] = xs\" \n| \"mezcla (x # xs) (y # ys) = (if x \u2264 y\n                               then x # mezcla xs (y # ys)\n                               else y # mezcla (x # xs) ys)\"\n\nvalue \"mezcla [1,2,5] [3,5,7]\" -- \"= [1,2,3,5,5,7]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 5. Definir la funci\u00f3n\n     ordenaM :: int list \u21d2 int list\n  tal que (ordenaM xs) es la lista obtenida ordenando la lista xs\n  mediante mezclas; es decir, la divide en dos mitades, las ordena y las\n  mezcla. Por ejemplo, \n     ordenaM [3,2,5,2] = [2,2,3,5]\n  ------------------------------------------------------------------ *}\n\nfun ordenaM :: \"int list \u21d2 int list\" where\n  \"ordenaM [] = []\" \n| \"ordenaM [x] = [x]\" \n| \"ordenaM xs = \n     (let mitad = length xs div 2 in\n      mezcla (ordenaM (take mitad xs)) \n             (ordenaM (drop mitad xs)))\"\n\nvalue \"ordenaM [3,2,5,2]\" -- \"= [2,2,3,5]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 6. Sea x \u2264 y. Si y es menor o igual que todos los elementos\n  de xs, entonces x es menor o igual que todos los elementos de xs\n  ------------------------------------------------------------------ *}\n\nlemma menor_menor: \n  \"x \u2264 y \u27f9 menor y xs \u27f6 menor x xs\"\nby (induct xs) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 7. Demostrar que el n\u00famero de veces que aparece n en la\n  mezcla de dos listas es igual a la suma del n\u00famero de apariciones en\n  cada una de las listas\n  ------------------------------------------------------------------ *}\n\nlemma cuenta_mezcla: \n  \"cuenta (mezcla xs ys) n = cuenta xs n + cuenta ys n\"\nby (induct xs ys rule: mezcla.induct) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 8. Demostrar que si x es menor que todos los elementos de\n  ys y de zs, entonces tambi\u00e9n lo es de su mezcla.\n  ------------------------------------------------------------------ *}\n\nlemma menor_mezcla:\n  assumes \"menor x ys\" \n          \"menor x zs\" \n  shows   \"menor x (mezcla ys zs)\"\nusing assms \nby (induct ys zs rule: mezcla.induct) simp_all\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 9. Demostrar que la mezcla de dos listas ordenadas es una\n  lista ordenada. \n  Indicaci\u00f3n: Usar los siguientes lemas\n  \u00b7 linorder_not_le: (\u00ac x \u2264 y) = (y < x)\n  \u00b7 order_less_le:   (x < y) = (x \u2264 y \u2227 x \u2260 y)\n  ------------------------------------------------------------------ *}\n\nlemma ordenada_mezcla:\n  assumes \"ordenada xs\" \n          \"ordenada ys\" \n  shows   \"ordenada (mezcla xs ys)\"\nusing assms \nby (induct xs ys rule: mezcla.induct) \n   (auto simp add: menor_mezcla\n                   menor_menor\n                   linorder_not_le \n                   order_less_le)\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 10. Demostrar que si x es mayor que 1, entonces el m\u00ednimo de\n  x y su mitad es menor que x.\n  Indicaci\u00f3n: Usar los siguientes lemas\n  \u00b7 min_def:         min a b = (if a \u2264 b then a else b)\n  \u00b7 linorder_not_le: (\u00ac x \u2264 y) = (y < x)\n  ------------------------------------------------------------------ *}\n\nlemma min_mitad: \n  \"1 < x \u27f9 min x (x div 2::int) < x\"\nby (simp add: min_def linorder_not_le)\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 11. Demostrar que si x es mayor que 1, entonces x menos su\n  mitad es menor que x. \n  ------------------------------------------------------------------ *}\n\nlemma menos_mitad: \n  \"1 < x \u27f9 x - x div (2::int) < x\"\nby arith\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 11. Demostrar que (ordenaM xs) est\u00e1 ordenada.\n  ------------------------------------------------------------------ *}\n\ntheorem ordenada_ordenaM:\n  \"ordenada (ordenaM xs)\"\nby (induct xs rule: ordenaM.induct) \n   (auto simp add: ordenada_mezcla)\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 12. Demostrar que el n\u00famero de apariciones de un elemento en\n  la concatenaci\u00f3n de dos listas es la suma del n\u00famero de apariciones en\n  cada una.\n  ------------------------------------------------------------------ *}\n\nlemma cuenta_conc: \n  \"cuenta (xs @ ys) x = cuenta xs x + cuenta ys x\"\nby (induct xs) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 13. Demostrar que las listas xs y (ordenaM xs) tienen los\n  mismos elementos.\n  ------------------------------------------------------------------ *}\n\ntheorem cuenta_ordenaM: \n  \"cuenta (ordenaM xs) x = cuenta xs x\"\nby (induct xs rule: ordenaM.induct) \n   (auto simp add: cuenta_mezcla \n                   cuenta_conc [symmetric])\n   \nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda 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 mezcla. 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\/4627"}],"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=4627"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4627\/revisions"}],"predecessor-version":[{"id":4628,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4627\/revisions\/4628"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4627"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4627"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4627"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}