{"id":4611,"date":"2014-11-20T20:31:06","date_gmt":"2014-11-20T19:31:06","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4611"},"modified":"2014-11-28T14:01:52","modified_gmt":"2014-11-28T13:01:52","slug":"ra2014-ejercicios-de-cuantificadores-sobre-listas-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2014-ejercicios-de-cuantificadores-sobre-listas-con-isabellehol\/","title":{"rendered":"RA2014: Ejercicios de cuantificadores sobre listas 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 comentado las soluciones de la 5\u00aa relaci\u00f3n de ejercicios cuyo objetivo es demostrar con Isabelle\/HOL propiedades de programas con cuantificadores sobre listas.<\/p>\n<p>Los ejercicios y sus soluciones se muestran a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* R5: Cuantificadores sobre listas *}\n\ntheory R5\nimports Main \nbegin\n        \ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 1. Definir la funci\u00f3n \n     todos :: ('a \u21d2 bool) \u21d2 'a list \u21d2 bool\n  tal que (todos p xs) se verifica si todos los elementos de la lista \n  xs cumplen la propiedad p. Por ejemplo, se verifica \n     todos (\u03bbx. 1 < length x) [[2,1,4],[1,3]]\n     \u00actodos (\u03bbx. 1 < length x) [[2,1,4],[3]]\n\n  Nota: La funci\u00f3n todos es equivalente a la predefinida list_all. \n  --------------------------------------------------------------------- \n*}\n\nfun todos :: \"('a \u21d2 bool) \u21d2 'a list \u21d2 bool\" where\n  \"todos p []     = True\"\n| \"todos p (y#ys) = ((p y) \u2227 (todos p ys))\"\n\nvalue \"todos (\u03bbx. 1 < length x) [[2,1,4],[1,3]]\" -- \"= True\"\nvalue \"todos (\u03bbx. 1 < length x) [[2,1,4],[3]]\"   -- \"= False\"\n\ntext {* \n  --------------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n \n     algunos :: ('a \u21d2 bool) \u21d2 'a list \u21d2 bool\n  tal que (algunos p xs) se verifica si algunos elementos de la lista \n  xs cumplen la propiedad p. Por ejemplo, se verifica \n     algunos (\u03bbx. 1 < length x) [[2,1,4],[3]]\n     \u00acalgunos (\u03bbx. 1 < length x) [[],[3]]\"\n\n  Nota: La funci\u00f3n algunos es equivalente a la predefinida list_ex. \n  --------------------------------------------------------------------- \n*}\n\nfun algunos  :: \"('a \u21d2 bool) \u21d2 'a list \u21d2 bool\" where\n  \"algunos p []     = False\"\n| \"algunos p (x#xs) = ((p x) \u2228 (algunos p xs))\"\n\nvalue \"algunos (\u03bbx. 1 < length x) [[2,1,4],[3]]\" -- \"= True\"\nvalue \"algunos (\u03bbx. 1 < length x) [[],[3]]\"      -- \"= False\"\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 3.1. Demostrar o refutar autom\u00e1ticamente \n     todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\"\nby (induct xs) auto\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 3.2. Demostrar o refutar detalladamente\n     todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\"\nproof (induct xs)\n  show \"todos (\u03bbx. P x \u2227 Q x) [] = (todos P [] \u2227 todos Q [])\" by simp\nnext\n  fix a xs \n  assume \"todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\"\n  thus \"todos (\u03bbx. P x \u2227 Q x) (a#xs) = (todos P (a#xs) \u2227 todos Q (a#xs))\"\n    by auto\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\"\nproof (induct xs)\n  show \"todos (\u03bbx. P x \u2227 Q x) [] = (todos P [] \u2227 todos Q [])\" by simp\nnext\n  fix a xs \n  assume HI: \"todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\"\n  show \"todos (\u03bbx. P x \u2227 Q x) (a#xs) = (todos P (a#xs) \u2227 todos Q (a#xs))\"\n  proof -\n    have \"todos (\u03bbx. P x \u2227 Q x) (a#xs) = \n         ((P a) \u2227 (Q a) \u2227 todos (\u03bbx. P x \u2227 Q x) xs)\" by simp\n    also have \"\u2026 = ((P a) \u2227 (Q a) \u2227 todos P xs \u2227 todos Q xs)\" using HI by simp\n    also have \"\u2026 = (((P a) \u2227 todos P xs) \u2227 ((Q a) \u2227 todos Q xs))\" by auto\n    also have \"\u2026 = (todos P (a#xs) \u2227 todos Q (a#xs))\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 4.1. Demostrar o refutar autom\u00e1ticamente \n     todos P (x @ y) = (todos P x \u2227 todos P y)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma todos_append:\n  \"todos P (x @ y) = (todos P x \u2227 todos P y)\"\nby (induct x) simp_all\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 4.2. Demostrar o refutar detalladamente\n     todos P (x @ y) = (todos P x \u2227 todos P y)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma todos_append_2: \n  \"todos P (x @ y) = (todos P x \u2227 todos P y)\"\nproof (induct x)\n  show \"todos P ([] @ y) = (todos P [] \u2227 todos P y)\" by simp\nnext\n  fix a x\n  assume \"todos P (x @ y) = (todos P x \u2227 todos P y)\"\n  thus \"todos P ((a#x) @ y) = (todos P (a#x) \u2227 todos P y)\"\n    by auto\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma todos_append_3: \n  \"todos P (x @ y) = (todos P x \u2227 todos P y)\"\nproof (induct x)\n  show \"todos P ([] @ y) = (todos P [] \u2227 todos P y)\" by simp\nnext\n  fix a x\n  assume HI: \"todos P (x @ y) = (todos P x \u2227 todos P y)\"\n  show \"todos P ((a#x) @ y) = (todos P (a#x) \u2227 todos P y)\"\n  proof -\n    have \"todos P ((a#x) @ y) = ((P a) \u2227 todos P (x@y))\" by simp\n    also have \"\u2026 = ((P a) \u2227 todos P x \u2227 todos P y)\" using HI by simp\n    also have \"\u2026 = (todos P (a#x) \u2227 todos P y)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 5.1. Demostrar o refutar autom\u00e1ticamente \n     todos P (rev xs) = todos P xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"todos P (rev xs) = todos P xs\"\nby (induct xs) (auto simp add: todos_append)\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 5.2. Demostrar o refutar detalladamente\n     todos P (rev xs) = todos P xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"todos P (rev xs) = todos P xs\"\nproof (induct xs)\n  show \"todos P (rev []) = todos P []\" by simp\nnext\n  fix a xs\n  assume \"todos P (rev xs) = todos P xs\"\n  thus \"todos P (rev (a#xs)) = todos P (a#xs)\" \n    by (auto simp add: todos_append)\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"todos P (rev xs) = todos P xs\"\nproof (induct xs)\n  show \"todos P (rev []) = todos P []\" by simp\nnext\n  fix a xs\n  assume HI: \"todos P (rev xs) = todos P xs\"\n  show \"todos P (rev (a#xs)) = todos P (a#xs)\"\n  proof -\n    have \"todos P (rev (a#xs)) = todos P ((rev xs)@[a])\" by simp \n    also have \"\u2026 = (todos P (rev xs) \u2227 todos P [a])\" \n      by (simp add: todos_append)\n    also have \"\u2026 = (todos P xs \u2227 todos P [a])\" using HI by simp\n    also have \"\u2026 = (todos P [a] \u2227 todos P xs)\" by auto\n    also have \"\u2026 = (P a \u2227 todos P xs)\" by simp\n    also have \"\u2026 = todos P (a#xs)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 6. Demostrar o refutar:\n    algunos (\u03bbx. P x \u2227 Q x) xs = (algunos P xs \u2227 algunos Q xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"Se busca un contraejemplo con nitpick\"\nlemma \"algunos (\u03bbx. P x \u2227 Q x) xs = (algunos P xs \u2227 algunos Q xs)\"\nnitpick\noops\n\ntext {*\n  El contraejemplo encontrado es\n     Nitpick found a counterexample for card 'a = 3:\n     \n     Free variables:\n       P = (\u03bbx. _)(a\u21d81\u21d9 := True, a\u21d82\u21d9 := True, a\u21d83\u21d9 := False)\n       Q = (\u03bbx. _)(a\u21d81\u21d9 := False, a\u21d82\u21d9 := False, a\u21d83\u21d9 := True)\n       xs = [a\u21d83\u21d9, a\u21d82\u21d9]\n*}\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 7.1. Demostrar o refutar autom\u00e1ticamente\n     algunos P (map f xs) = algunos (P \u2218 f) xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"algunos P (map f xs) = algunos (P o f) xs\"\nby (induct xs) simp_all\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"algunos P (map f xs) = algunos (P \u2218 f) xs\"\nproof (induct xs)\n  show \"algunos P (map f []) = algunos (P \u2218 f) []\" by simp\nnext\n  fix a xs\n  assume \"algunos P (map f xs) = algunos (P \u2218 f) xs\"\n  thus \"algunos P (map f (a#xs)) = algunos (P \u2218 f) (a#xs)\" by auto\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 7.2. Demostrar o refutar detalladamente\n     algunos P (map f xs) = algunos (P \u2218 f) xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"algunos P (map f xs) = algunos (P \u2218 f) xs\"\nproof (induct xs)\n  show \"algunos P (map f []) = algunos (P \u2218 f) []\" by simp\nnext\n  fix a xs\n  assume HI: \"algunos P (map f xs) = algunos (P \u2218 f) xs\"\n  show \"algunos P (map f (a#xs)) = algunos (P \u2218 f) (a#xs)\"\n  proof -\n    have \"algunos P (map f (a#xs)) = algunos P ((f a)#(map f xs))\" by simp\n    also have \"\u2026 = ((P (f a)) \u2228 (algunos P (map f xs)))\" by simp\n    also have \"\u2026 = (((P \u2218 f) a) \u2228 (algunos (P \u2218 f) xs))\" using HI by simp\n    also have \"\u2026 = algunos (P \u2218 f) (a#xs)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 8.1. Demostrar o refutar autom\u00e1ticamente \n     algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma algunos_append:\n  \"algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\"\nby (induct xs) simp_all\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 8.2. Demostrar o refutar detalladamente\n     algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma algunos_append_2: \n  \"algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\"\nproof (induct xs)\n  show \"algunos P ([] @ ys) = (algunos P [] \u2228 algunos P ys)\" by simp\nnext\n  fix a xs\n  assume \"algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\"\n  thus \"algunos P ((a#xs) @ ys) = (algunos P (a#xs) \u2228 algunos P ys)\"\n    by auto\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma algunos_append_3: \n  \"algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\"\nproof (induct xs)\n  show \"algunos P ([] @ ys) = (algunos P [] \u2228 algunos P ys)\" by simp\nnext\n  fix a xs\n  assume HI: \"algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\"\n  show \"algunos P ((a#xs) @ ys) = (algunos P (a#xs) \u2228 algunos P ys)\"\n  proof -\n    have \"algunos P ((a#xs) @ ys) = algunos P (a#(xs @ ys))\" by simp\n    also have \"\u2026 = ((P a) \u2228 algunos P (xs @ ys))\" by simp\n    also have \"\u2026 = ((P a) \u2228 algunos P xs \u2228 algunos P ys)\" using HI by simp\n    also have \"\u2026 = (algunos P (a#xs) \u2228 algunos P ys)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 9.1. Demostrar o refutar autom\u00e1ticamente\n     algunos P (rev xs) = algunos P xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"algunos P (rev xs) = algunos P xs\"\nby (induct xs) (auto simp add: algunos_append)\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 9.2. Demostrar o refutar detalladamente\n     algunos P (rev xs) = algunos P xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"algunos P (rev xs) = algunos P xs\"\nproof (induct xs)\n show \"algunos P (rev []) = algunos P []\" by simp\nnext\n  fix a xs\n  assume \"algunos P (rev xs) = algunos P xs\"\n  thus \"algunos P (rev (a#xs)) = algunos P (a#xs)\" \n    by (auto simp add: algunos_append)\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"algunos P (rev xs) = algunos P xs\"\nproof (induct xs)\n show \"algunos P (rev []) = algunos P []\" by simp\nnext\n  fix a xs\n  assume HI: \"algunos P (rev xs) = algunos P xs\"\n  show \"algunos P (rev (a#xs)) = algunos P (a#xs)\"\n  proof -\n    have \"algunos P (rev (a#xs)) = algunos P ((rev xs) @ [a])\" by simp\n    also have \"\u2026 = (algunos P (rev xs) \u2228 algunos P [a])\" \n      by (simp add: algunos_append)\n    also have \"\u2026 = (algunos P xs \u2228 algunos P [a])\" using HI by simp\n    also have \"\u2026 = (algunos P xs \u2228 P a)\" by simp\n    also have \"\u2026 = (P a \u2228 algunos P xs)\" by auto\n    also have \"\u2026 = algunos P (a#xs)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 10. Encontrar un t\u00e9rmino no trivial Z tal que sea cierta la \n  siguiente ecuaci\u00f3n:\n     algunos (\u03bbx. P x \u2228 Q x) xs = Z\n  y demostrar la equivalencia de forma autom\u00e1tica y detallada.\n  --------------------------------------------------------------------- \n*}\n\ntext {*\n  Soluci\u00f3n: La ecuaci\u00f3n se verifica eligiendo como Z el t\u00e9rmino  \n     algunos P xs \u2228 algunos Q xs\n  En efecto,\n*}\n\nlemma \"algunos (\u03bbx. P x \u2228 Q x) xs = (algunos P xs \u2228 algunos Q xs)\"\nby (induct xs) auto\n\n-- \"De forma estructurada\"\nlemma \"algunos (\u03bbx. P x \u2228 Q x) xs = (algunos P xs \u2228 algunos Q xs)\"\nproof (induct xs)\n  show \"algunos  (\u03bbx. P x \u2228 Q x) [] = (algunos P [] \u2228 algunos Q [])\" by simp\nnext\n  fix a xs\n  assume \"algunos (\u03bbx. (P x \u2228 Q x)) xs = (algunos P xs \u2228 algunos Q xs)\"\n  thus \"algunos (\u03bbx. P x \u2228 Q x) (a#xs) = (algunos P (a#xs) \u2228 algunos Q (a#xs))\"\n    by auto\nqed\n\n-- \"De forma detallada\"\nlemma \"algunos (\u03bbx. P x \u2228 Q x) xs = (algunos P xs \u2228 algunos Q xs)\"\nproof (induct xs)\n  show \"algunos  (\u03bbx. P x \u2228 Q x) [] = (algunos P [] \u2228 algunos Q [])\" by simp\nnext\n  fix a xs\n  assume HI: \"algunos (\u03bbx. (P x \u2228 Q x)) xs = (algunos P xs \u2228 algunos Q xs)\"\n  show \"algunos (\u03bbx. P x \u2228 Q x) (a#xs) = (algunos P (a#xs) \u2228 algunos Q (a#xs))\"\n  proof -\n    have \"algunos (\u03bbx. P x \u2228 Q x) (a#xs) = \n      ((P a) \u2228 (Q a) \u2228 algunos (\u03bbx. P x \u2228 Q x) xs)\" by simp\n    also have \"\u2026 = ((P a) \u2228 (Q a) \u2228 algunos P xs \u2228 algunos Q xs)\" \n      using HI by simp\n    also have \"\u2026 = (((P a) \u2228 algunos P xs) \u2228 ((Q a) \u2228 algunos Q xs))\" by auto\n    also have \"\u2026 = (algunos P (a#xs) \u2228 algunos Q (a#xs))\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 11.1. Demostrar o refutar autom\u00e1ticamente\n     algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\"\nby (induct xs) simp_all\n     \ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 11.2. Demostrar o refutar detalladamente\n     algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\"\nproof (induct xs)\n  show \"algunos P [] = (\u00ac todos (\u03bbx. (\u00ac P x)) [])\" by simp\nnext\n  fix a xs\n  assume \"algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\"\n  thus \"algunos P (a#xs) = (\u00ac todos (\u03bbx. (\u00ac P x)) (a#xs))\"\n    by auto\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\"\nproof (induct xs)\n  show \"algunos P [] = (\u00ac todos (\u03bbx. (\u00ac P x)) [])\" by simp\nnext\n  fix a xs\n  assume HI: \"algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\"\n  show \"algunos P (a#xs) = (\u00ac todos (\u03bbx. (\u00ac P x)) (a#xs))\"\n  proof - \n    have \"algunos P (a#xs) = ((P a) \u2228 algunos P xs)\" by simp\n    also have \"\u2026 = ((P a) \u2228 \u00ac todos (\u03bbx. (\u00ac P x)) xs)\" using HI by simp\n    also have \"\u2026 = (\u00ac (\u00ac (P a) \u2227 todos (\u03bbx. (\u00ac P x)) xs))\" by simp\n    also have \"\u2026 = (\u00ac todos (\u03bbx. (\u00ac P x)) (a#xs))\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 12. Definir la funcion primitiva recursiva \n     estaEn :: 'a \u21d2 'a list \u21d2 bool\n  tal que (estaEn x xs) se verifica si el elemento x est\u00e1 en la lista\n  xs. Por ejemplo, \n     estaEn (2::nat) [3,2,4] = True\n     estaEn (1::nat) [3,2,4] = False\n  --------------------------------------------------------------------- \n*}\n\nfun estaEn :: \"'a \u21d2 'a list \u21d2 bool\" where\n  \"estaEn x []     = False\"\n| \"estaEn x (a#xs) = (x=a \u2228 estaEn x xs)\"  \n\nvalue \"estaEn (2::nat) [3,2,4]\" -- \"= True\"\nvalue \"estaEn (1::nat) [3,2,4]\" -- \"= False\"\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 13. Expresar la relaci\u00f3n existente entre estaEn y  algunos. \n  Demostrar dicha relaci\u00f3n de forma autom\u00e1tica y detallada.\n  --------------------------------------------------------------------- \n*}\n\ntext {*\n  Soluci\u00f3n: La relaci\u00f3n es \n     estaEn y xs = algunos (\u03bbx. x=y) xs\n  En efecto,  \n*}\n\nlemma estaEn_algunos:\n  \"estaEn y xs = algunos (\u03bbx. x=y) xs\"\nby (induct xs) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma estaEn_algunos_2:\n  \"estaEn y xs = algunos (\u03bbx. x=y) xs\"\nproof (induct xs)\n  show \"estaEn y [] = algunos (\u03bbx. x=y) []\" by simp\nnext\n  fix a xs\n  assume \"estaEn y xs = algunos (\u03bbx. x=y) xs\"\n  thus \"estaEn y (a#xs) = algunos (\u03bbx. x=y) (a#xs)\" by auto\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma estaEn_algunos_3:\n  \"estaEn y xs = algunos (\u03bbx. x=y) xs\"\nproof (induct xs)\n  show \"estaEn y [] = algunos (\u03bbx. x=y) []\" by simp\nnext\n  fix a xs\n  assume HI: \"estaEn y xs = algunos (\u03bbx. x=y) xs\"\n  show \"estaEn y (a#xs) = algunos (\u03bbx. x=y) (a#xs)\"\n  proof -\n    have \"estaEn y (a#xs) = (y=a \u2228 estaEn y xs)\" by simp\n    also have \"\u2026 = (y=a \u2228 algunos (\u03bbx. x=y) xs)\" using HI by simp\n    also have \"\u2026 = (a=y \u2228 algunos (\u03bbx. x=y) xs)\" by auto\n    also have \"\u2026 = algunos (\u03bbx. x=y) (a#xs)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {* \n  --------------------------------------------------------------------- \n  Ejercicio 14. Definir la funci\u00f3n primitiva recursiva \n     sinDuplicados :: 'a list \u21d2 bool\n  tal que (sinDuplicados xs) se verifica si la lista xs no contiene\n  duplicados. Por ejemplo,  \n     sinDuplicados [1::nat,4,2]   = True\n     sinDuplicados [1::nat,4,2,4] = False\n  --------------------------------------------------------------------- \n*}\n\nfun uplicados :: \"'a list \u21d2 bool\" where\n  \"uplicados [] = True\"\n| \"uplicados (a#xs) = ((\u00ac estaEn a xs) \u2227 uplicados xs)\"\n\nvalue \"sinDuplicados [1::nat,4,2]\"   -- \"= True\"\nvalue \"sinDuplicados [1::nat,4,2,4]\" -- \"= False\"\n\ntext {* \n  --------------------------------------------------------------------- \n  Ejercicio 15. Definir la funci\u00f3n primitiva recursiva \n     borraDuplicados :: 'a list \u21d2 bool\n  tal que (borraDuplicados xs) es la lista obtenida eliminando los\n  elementos duplicados de la lista xs. Por ejemplo, \n     borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]\n\n  Nota: La funci\u00f3n borraDuplicados es equivalente a la predefinida remdups. \n  --------------------------------------------------------------------- \n*}\n\nfun borraDuplicados :: \"'a list \u21d2 'a list\" where\n  \"borraDuplicados []     = []\"\n| \"borraDuplicados (a#xs) = (if estaEn a xs \n                             then borraDuplicados xs \n                             else (a#borraDuplicados xs))\"\n\nvalue \"borraDuplicados [1::nat,2,4,2,3]\" -- \"= [1,4,2,3]\"\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 16.1. Demostrar o refutar autom\u00e1ticamente\n     length (borraDuplicados xs) \u2264 length xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma length_borraDuplicados:\n  \"length (borraDuplicados xs) \u2264 length xs\"\nby (induct xs) simp_all\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 16.2. Demostrar o refutar detalladamente\n     length (borraDuplicados xs) \u2264 length xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma length_borraDuplicados_2: \n  \"length (borraDuplicados xs) \u2264 length xs\"\nproof (induct xs)\n  show \"length (borraDuplicados []) \u2264 length []\" by simp\nnext\n  fix a xs\n  assume HI: \"length (borraDuplicados xs) \u2264 length xs\"\n  thus \"length (borraDuplicados (a#xs)) \u2264 length (a#xs)\"\n  proof (cases)\n    assume \"estaEn a xs\"\n    thus \"length (borraDuplicados (a#xs)) \u2264 length (a#xs)\" \n      using HI by auto\n  next\n    assume \"(\u00ac estaEn a xs)\"\n    thus \"length (borraDuplicados (a#xs)) \u2264 length (a#xs)\" \n      using HI by auto\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma length_borraDuplicados_3: \n  \"length (borraDuplicados xs) \u2264 length xs\"\nproof (induct xs)\n  show \"length (borraDuplicados []) \u2264 length []\" by simp\nnext\n  fix a xs\n  assume HI: \"length (borraDuplicados xs) \u2264 length xs\"\n  show \"length (borraDuplicados (a#xs)) \u2264 length (a#xs)\"\n  proof (cases)\n    assume \"estaEn a xs\"\n    hence \"length (borraDuplicados (a#xs)) = length (borraDuplicados xs)\" \n      by simp\n    also have \"\u2026 \u2264 length xs\" using HI by simp\n    also have \"\u2026 \u2264 length (a#xs)\" by simp\n    finally show ?thesis .\n  next\n    assume \"(\u00ac estaEn a xs)\"\n    hence \"length (borraDuplicados (a#xs)) = length (a#(borraDuplicados xs))\"\n      by simp\n    also have \"\u2026 = 1 + length (borraDuplicados xs)\" by simp\n    also have \"\u2026 \u2264 1 + length xs\" using HI by simp\n    also have \"\u2026 = length (a#xs)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 17.1. Demostrar o refutar autom\u00e1ticamente\n     estaEn a (borraDuplicados xs) = estaEn a xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma estaEn_borraDuplicados: \n  \"estaEn a (borraDuplicados xs) = estaEn a xs\"\nby (induct xs) auto\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 17.2. Demostrar o refutar detalladamente\n     estaEn a (borraDuplicados xs) = estaEn a xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma estaEn_borraDuplicados_2: \n  \"estaEn a (borraDuplicados xs) = estaEn a xs\"\nproof (induct xs)\n  show \"estaEn a (borraDuplicados []) = estaEn a []\" by simp\nnext\n  fix b xs\n  assume HI: \"estaEn a (borraDuplicados xs) = estaEn a xs\"\n  show \"estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)\"\n  proof (rule iffI)\n    assume c1: \"estaEn a (borraDuplicados (b#xs))\"\n    show \"estaEn a (b#xs)\"\n    proof (cases)\n      assume \"estaEn b xs\"\n      thus \"estaEn a (b#xs)\" using c1 HI by auto\n    next\n      assume \"\u00ac estaEn b xs\"\n      thus \"estaEn a (b#xs)\" using c1 HI by auto\n    qed\n  next\n    assume c2: \"estaEn a (b#xs)\"\n    show \"estaEn a (borraDuplicados (b#xs))\"\n    proof (cases)\n      assume \"a=b\"\n      thus \"estaEn a (borraDuplicados (b#xs))\" using HI by auto\n    next\n      assume \"a\u2260b\"\n      thus \"estaEn a (borraDuplicados (b#xs))\" using `a\u2260b` c2 HI by auto\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma estaEn_borraDuplicados_3: \n  \"estaEn a (borraDuplicados xs) = estaEn a xs\"\nproof (induct xs)\n  show \"estaEn a (borraDuplicados []) = estaEn a []\" by simp\nnext\n  fix b xs\n  assume HI: \"estaEn a (borraDuplicados xs) = estaEn a xs\"\n  show \"estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)\"\n  proof (rule iffI)\n    assume c1: \"estaEn a (borraDuplicados (b#xs))\"\n    show \"estaEn a (b#xs)\"\n    proof (cases)\n      assume \"estaEn b xs\"\n      hence \"estaEn a (borraDuplicados xs)\" using c1 by simp\n      hence \"estaEn a xs\" using HI by simp\n      thus \"estaEn a (b#xs)\" by simp\n    next\n      assume \"\u00ac estaEn b xs\"\n      hence \"estaEn a (b#(borraDuplicados xs))\" using c1 by simp\n      hence \"a=b \u2228 (estaEn a (borraDuplicados xs))\" by simp\n      hence \"a=b \u2228 (estaEn a xs)\" using HI by simp\n      thus \"estaEn a (b#xs)\" by simp\n    qed\n  next\n    assume c2: \"estaEn a (b#xs)\"\n    show \"estaEn a (borraDuplicados (b#xs))\"\n    proof (cases)\n      assume \"a=b\"\n      thus \"estaEn a (borraDuplicados (b#xs))\" using HI by auto\n    next\n      assume \"a\u2260b\"\n      hence \"estaEn a xs\" using c2 by simp\n      hence \"estaEn a (borraDuplicados xs)\" using HI by simp\n      thus \"estaEn a (borraDuplicados (b#xs))\" using `a\u2260b` by simp\n    qed\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 18.1. Demostrar o refutar autom\u00e1ticamente\n     sinDuplicados (borraDuplicados xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica\"\nlemma sinDuplicados_borraDuplicados:\n  \"sinDuplicados (borraDuplicados xs)\"\nby (induct xs) (auto simp add: estaEn_borraDuplicados)\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 18.2. Demostrar o refutar detalladamente\n     sinDuplicados (borraDuplicados xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma sinDuplicados_borraDuplicados_2:\n  \"sinDuplicados (borraDuplicados xs)\"\nproof (induct xs)\n  show \"sinDuplicados (borraDuplicados [])\" by simp\nnext\n  fix a xs\n  assume HI: \"sinDuplicados (borraDuplicados xs)\"\n  show \"sinDuplicados (borraDuplicados (a#xs))\"\n  proof (cases)\n    assume \"estaEn a xs\"\n    thus \"sinDuplicados (borraDuplicados (a#xs))\" using HI by simp\n  next\n    assume \"\u00ac estaEn a xs\"\n    thus \"sinDuplicados (borraDuplicados (a#xs))\" \n      using `\u00ac estaEn a xs` HI \n      by (auto simp add: estaEn_borraDuplicados)\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma sinDuplicados_borraDuplicados_3:\n  \"sinDuplicados (borraDuplicados xs)\"\nproof (induct xs)\n  show \"sinDuplicados (borraDuplicados [])\" by simp\nnext\n  fix a xs\n  assume HI: \"sinDuplicados (borraDuplicados xs)\"\n  show \"sinDuplicados (borraDuplicados (a#xs))\"\n  proof (cases)\n    assume \"estaEn a xs\"\n    thus \"sinDuplicados (borraDuplicados (a#xs))\" using HI by simp\n  next\n    assume \"\u00ac estaEn a xs\"\n    hence \"\u00ac (estaEn a xs) \u2227 sinDuplicados (borraDuplicados xs)\" \n      using HI by simp\n    hence \"\u00ac estaEn a (borraDuplicados xs) \u2227 \n           sinDuplicados (borraDuplicados xs)\" \n      by (simp add: estaEn_borraDuplicados)\n    hence \"sinDuplicados (a#borraDuplicados xs)\" by simp\n    thus \"sinDuplicados (borraDuplicados (a#xs))\" \n      using `\u00ac estaEn a xs` by simp\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 19. Demostrar o refutar:\n    borraDuplicados (rev xs) = rev (borraDuplicados xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"Se busca un contraejemplo con\"\nlemma \"borraDuplicados (rev xs) = rev (borraDuplicados xs)\"\nquickcheck\noops\n\ntext {*\n  El contraejemplo encontrado es\n     xs = [3, 2, 3]\n  En efecto,\n      borraDuplicados (rev xs) = borraDuplicados (rev [3,2,3]) = [2,3] \n      rev (borraDuplicados xs) = rev (borraDuplicados [3,2,3]) = [3,2] \n*}\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 comentado las soluciones de la 5\u00aa relaci\u00f3n de ejercicios cuyo objetivo es demostrar con Isabelle\/HOL propiedades de programas con cuantificadores sobre listas. Los ejercicios y sus soluciones se muestran 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\/4611"}],"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=4611"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4611\/revisions"}],"predecessor-version":[{"id":4629,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4611\/revisions\/4629"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4611"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4611"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4611"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}