{"id":6875,"date":"2019-12-05T21:45:16","date_gmt":"2019-12-05T20:45:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6875"},"modified":"2019-12-06T11:52:23","modified_gmt":"2019-12-06T10:52:23","slug":"ra2019-ejercicios-de-cuantificadores-sobre-listas-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-ejercicios-de-cuantificadores-sobre-listas-en-isabelle-hol\/","title":{"rendered":"RA2019: Ejercicios de cuantificadores sobre listas 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\/m-ra-19\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de la 4\u00aa relaci\u00f3n de ejercicios de cuantificadores sobre listas. Para cada propiedad se dan tres demostraciones en Isabelle\/HOL: la primera autom\u00e1tica, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de HOL que se utilizan en cada paso.<\/p>\n<p>La teor\u00eda con las soluciones de los ejercicios es la siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039R4: Cuantificadores sobre listas\u203a\n\ntheory R4_Cuantificadores_sobre_listas_sol\nimports Main \nbegin\n        \ntext \u2039------------------------------------------------------------------ \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  ---------------------------------------------------------------------\u203a\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\nlemma \n  shows \"(\u03bbx. 1  <  length x) [[2,1,4],[1,3]]\"\n    and \"\u00actodos (\u03bbx. 1 < length x) [[2,1,4],[3]]\" \n  by simp+\n\ntext \u2039------------------------------------------------------------------ \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  ---------------------------------------------------------------------\u203a\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\nlemma \n  shows \"algunos (\u03bbx. 1 < length x) [[2,1,4],[3]]\"\n    and \"\u00acalgunos (\u03bbx. 1 < length x) [[],[3]]\"\n  by simp+\n\ntext \u2039------------------------------------------------------------------ \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  ---------------------------------------------------------------------\u203a\n\n(* La demostraci\u00f3n autom\u00e1tica es *) \nlemma \"todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\"\n  by (induct xs) auto\n\ntext \u2039------------------------------------------------------------------ \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  ---------------------------------------------------------------------\u203a\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 [])\" \n    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  then show \"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  have \"todos (\u03bbx. P x \u2227 Q x) [] = True\"\n    by (simp only: todos.simps(1))\n  also have \"... = (True \u2227 True)\"\n    by (simp only: conj_absorb)\n  also have \"... = (todos P [] \u2227 todos Q [])\"\n    by (simp only: todos.simps(1))\n  finally show \"todos (\u03bbx. P x \u2227 Q x) [] = (todos P [] \u2227 todos Q [])\"\n    by this\nnext\n  fix x xs\n  assume HI: \"todos (\u03bbx. P x \u2227 Q x) xs = (todos P xs \u2227 todos Q xs)\"\n  have \"todos (\u03bbx. P x \u2227 Q x) (x#xs) = ((\u03bbx. P x \u2227 Q x) x \u2227 todos (\u03bbx. P x \u2227 Q x) xs)\"\n    by (simp only: todos.simps(2))\n  also have \"... = ((\u03bbx. P x \u2227 Q x) x \u2227 (todos P xs \u2227 todos Q xs))\"\n    by (simp only: HI)\n  also have \"... = (P x \u2227 Q x \u2227 todos P xs \u2227 todos Q xs)\"\n    by (simp only: conj_assoc)\n  also have \"... = (P x \u2227 todos P xs \u2227 Q x \u2227 todos Q xs)\"\n    by (simp only: conj_left_commute)\n  also have \"... = ((P x \u2227 todos P xs) \u2227 Q x \u2227 todos Q xs)\"\n    by (simp only: conj_assoc)\n  also have \"... = (todos P (x#xs) \u2227 Q x \u2227 todos Q xs)\"\n    by (simp only: todos.simps(2))\n  also have \"... = (todos P (x#xs) \u2227 todos Q (x#xs))\"\n    by (simp only: todos.simps(2))\n  finally show \"todos (\u03bbx. P x \u2227 Q x) (x#xs) = \n                (todos P (x#xs) \u2227 todos Q (x#xs))\"\n    by this\nqed\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 4.1. Demostrar o refutar autom\u00e1ticamente \n     todos P (x @ y) = (todos P x \u2227 todos P y)\n  ---------------------------------------------------------------------\u203a\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma todos_append:\n  \"todos P (x @ y) = (todos P x \u2227 todos P y)\"\n  by (induct x) simp_all\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 4.2. Demostrar o refutar detalladamente\n     todos P (x @ y) = (todos P x \u2227 todos P y)\n  ---------------------------------------------------------------------\u203a\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)\" \n    by simp\nnext\n  fix a x\n  assume \"todos P (x @ y) = (todos P x \u2227 todos P y)\"\n  then show \"todos P ((a#x) @ y) = (todos P (a#x) \u2227 todos P y)\"\n    by simp\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 arbitrary:y)\n  fix y\n  have \"todos P ([] @ y) = todos P y\"\n    by (simp only: append.simps(1))\n  also have \"... = (True \u2227 todos P y)\"\n    by (simp only: simp_thms(22))\n  also have \"... = (todos P [] \u2227 todos P y)\"\n    by (simp only: todos.simps(1))\n  finally show \"todos P ([] @ y) = (todos P [] \u2227 todos P y)\"\n    by this\nnext\n  fix a x\n  assume HI:\"\u22c0y. todos P (x @ y) = (todos P x \u2227 todos P y)\"\n  fix y\n  have \"todos P ((a#x) @ y) = (todos P (a#(x @ y)))\"\n    by (simp only: append.simps(2))\n  also have \"... = (P a \u2227 todos P (x @ y))\"\n    by (simp only: todos.simps(2))\n  also have \"... = (P a \u2227 todos P x \u2227 todos P y)\"\n    by (simp only: HI)\n  also have \"... = ((P a \u2227 todos P x) \u2227 todos P y)\"\n    by (simp only: conj_assoc)\n  also have \"... = (todos P (a#x) \u2227 todos P y)\"\n    by (simp only: todos.simps(2))\n  finally show \"todos P ((a#x) @ y) = (todos P (a#x) \u2227 todos P y)\"\n    by this\nqed\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 5.1. Demostrar o refutar autom\u00e1ticamente \n     todos P (rev xs) = todos P xs\n  ---------------------------------------------------------------------\u203a\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"todos P (rev xs) = todos P xs\"\n  by (induct xs) (auto simp add: todos_append)\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 5.2. Demostrar o refutar detalladamente\n     todos P (rev xs) = todos P xs\n  ---------------------------------------------------------------------\u203a\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 []\" \n    by simp\nnext\n  fix a xs\n  assume \"todos P (rev xs) = todos P xs\"\n  then show \"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 []\"\n    by (simp only: rev.simps(1))\nnext\n  fix x xs\n  assume HI: \"todos P (rev xs) = todos P xs\"\n  have \"todos P (rev (x#xs)) = todos P (rev xs@[x])\"\n    by (simp only: rev.simps(2))\n  also have \"... = (todos P (rev xs) \u2227 todos P [x])\"\n    by (simp only: todos_append)\n  also have \"... = (todos P xs \u2227 todos P [x])\"\n    by (simp only: HI)\n  also have \"... = (todos P [x] \u2227 todos P xs)\"\n    by (simp only: conj_commute)\n  also have \"... = (todos P ([x]@xs))\"\n    by (simp only: todos_append)\n  also have \"... = (todos P (x#xs))\"\n    by (simp only: append.simps)\n  finally show \"todos P (rev (x#xs)) = todos P (x#xs)\"\n    by this\nqed\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 6. Demostrar o refutar:\n    algunos (\u03bbx. P x \u2227 Q x) xs = (algunos P xs \u2227 algunos Q xs)\n  ---------------------------------------------------------------------\u203a\n\nlemma \"algunos (\u03bbx. P x \u2227 Q x) xs = (algunos P xs \u2227 algunos Q xs)\"\n  quickcheck\n  oops  \n\ntext \u2039\n   Quickcheck found a counterexample:\n     P = {a\u21e91}\n     Q = {a\u21e92}\n     xs = [a\u21e91, a\u21e92]\n   Evaluated terms:\n     algunos (\u03bbx. P x \u2227 Q x) xs = False\n     algunos P xs \u2227 algunos Q xs = True\n\u203a\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 7.1. Demostrar o refutar autom\u00e1ticamente\n     algunos P (map f xs) = algunos (P \u2218 f) xs\n  ---------------------------------------------------------------------\u203a\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"algunos P (map f xs) = algunos (P o f) xs\"\n  by (induct xs) simp_all\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 7.2. Demostrar o refutar detalladamente\n     algunos P (map f xs) = algunos (P \u2218 f) xs\n  ---------------------------------------------------------------------\u203a\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) []\" \n    by simp\nnext\n  fix a xs\n  assume \"algunos P (map f xs) = algunos (P \u2218 f) xs\"\n  then show \"algunos P (map f (a#xs)) = algunos (P \u2218 f) (a#xs)\" \n    by auto\nqed\n\n(* La demostraci\u00f3n detallada es *)\nlemma \"algunos P (map f xs) = algunos (P o f) xs\"\nproof (induct xs)\n  have \"algunos P (map f []) = algunos P []\"\n    by (simp only: list.map(1))\n  also have \"... = algunos (P o f) []\"\n    by (simp only: algunos.simps(1))\n  finally show \"algunos P (map f []) = algunos (P o f) []\"\n    by this\nnext\n  fix x xs\n  assume HI: \"algunos P (map f xs) = algunos (P o f) xs\"\n  have \"algunos P (map f (x#xs)) = algunos P ((f x) # (map f xs))\"\n    by (simp only: list.map(2))\n  also have \"... = (P (f x) \u2228 algunos P (map f xs))\"\n    by (simp only: algunos.simps(2))\n  also have \"... = (P (f x) \u2228 algunos (P o f) xs)\"\n    by (simp only: HI)\n  also have \"... = ((P o f) x \u2228 algunos (P o f) xs)\"\n    by (simp only: o_apply)\n  also have \"... = algunos (P o f) (x#xs)\"\n    by (simp only: algunos.simps(2))\n  finally show \"algunos P (map f (x#xs)) = algunos (P o f) (x#xs)\"\n    by this\nqed\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 8.1. Demostrar o refutar autom\u00e1ticamente \n     algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\n  ---------------------------------------------------------------------\u203a\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma algunos_append:\n  \"algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\"\n  by (induct xs) simp_all\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 8.2. Demostrar o refutar detalladamente\n     algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\n  ---------------------------------------------------------------------\u203a\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)\" \n    by simp\nnext\n  fix a xs\n  assume \"algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\"\n  then show \"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  have \"algunos P ([] @ ys) = (algunos P ys)\"\n    by (simp only: append_Nil)\n  also have \"... = (False \u2228 algunos P ys)\"\n    by (simp only: simp_thms(32))\n  also have \"... = (algunos P [] \u2228 algunos P ys)\"\n    by (simp only: algunos.simps(1))\n  finally show \"algunos P ([] @ ys) = (algunos P [] \u2228 algunos P ys)\"\n    by this\nnext\n  fix x xs\n  assume HI: \"algunos P (xs @ ys) = (algunos P xs \u2228 algunos P ys)\"\n  have \"algunos P ((x#xs) @ ys) = algunos P (x#(xs @ ys))\"\n    by (simp only: append_Cons)\n  also have \"... = (P x \u2228 algunos P (xs @ ys))\"\n    by (simp only: algunos.simps(2))\n  also have \"... = (P x \u2228 algunos P xs \u2228 algunos P ys)\"\n    by (simp only: HI)\n  also have \"... = ((P x \u2228 algunos P xs) \u2228 algunos P ys)\"\n    by (simp only: disj_assoc)\n  also have \"... = (algunos P (x#xs) \u2228 algunos P ys)\"\n    by (simp only: algunos.simps(2))\n  finally show \"algunos P ((x#xs) @ ys) = \n                (algunos P (x#xs) \u2228 algunos P ys)\"\n    by this\nqed\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 9.1. Demostrar o refutar autom\u00e1ticamente\n     algunos P (rev xs) = algunos P xs\n  ---------------------------------------------------------------------\u203a\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"algunos P (rev xs) = algunos P xs\"\n  by (induct xs) (auto simp add: algunos_append)\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 9.2. Demostrar o refutar detalladamente\n     algunos P (rev xs) = algunos P xs\n  ---------------------------------------------------------------------\u203a\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 []\" \n    by simp\nnext\n  fix a xs\n  assume \"algunos P (rev xs) = algunos P xs\"\n  then show \"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 []\"\n    by (simp only: rev.simps(1))\nnext\n  fix x xs\n  assume HI: \"algunos P (rev xs) = algunos P xs\"\n  have \"algunos P (rev (x#xs)) = algunos P (rev xs @ [x])\"\n    by (simp only: rev.simps(2))\n  also have \"... = (algunos P (rev xs) \u2228 algunos P [x])\"\n    by (simp only: algunos_append)\n  also have \"... = (algunos P xs \u2228 algunos P [x])\"\n    by (simp only: HI)\n  also have \"... = (algunos P xs \u2228 P x \u2228 algunos P [])\"\n    by (simp only: algunos.simps(2))\n  also have \"... = (algunos P xs \u2228 P x \u2228 False)\"\n    by (simp only: algunos.simps(1))\n  also have \"... = (algunos P xs \u2228 P x)\"\n    by (simp only: simp_thms(31))\n  also have \"... = (P x \u2228 algunos P xs)\"\n    by (simp only: disj_commute)\n  also have \"... = algunos P (x#xs)\"\n    by (simp only: algunos.simps(2))\n  finally show \"algunos P (rev (x#xs)) = algunos P (x#xs)\"\n    by this\nqed\n\ntext \u2039------------------------------------------------------------------ \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  --------------------------------------------------------------------- \u203a\n\ntext \u2039Soluci\u00f3n: La ecuaci\u00f3n se verifica eligiendo como Z el t\u00e9rmino  \n     algunos P xs \u2228 algunos Q xs\n  En efecto,\u203a\n\nlemma \"algunos (\u03bbx. P x \u2228 Q x) xs = (algunos P xs \u2228 algunos Q xs)\"\n  by (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 [])\" \n    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  then show \"algunos (\u03bbx. P x \u2228 Q x) (a#xs) = \n             (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  have \"algunos (\u03bbx. P x \u2228 Q x) [] = False\"\n    by (simp only: algunos.simps(1))\n  also have \"... = (False \u2228 False)\"\n    by (simp only: simp_thms(31))\n  also have \"... = (algunos P [] \u2228 False)\"\n    by (simp only: algunos.simps(1))\n  also have \"... = (algunos P [] \u2228 algunos Q [])\"\n    by (simp only: algunos.simps(1))\n  finally show \"algunos (\u03bbx. P x \u2228 Q x) [] = \n                (algunos P [] \u2228 algunos Q [])\"\n    by this\nnext\n  fix x xs\n  assume HI:\"algunos (\u03bbx. P x \u2228 Q x) xs = (algunos P xs \u2228 algunos Q xs)\"\n  have \"algunos (\u03bbx. P x \u2228 Q x) (x#xs) =((P x \u2228 Q x) \u2228 algunos (\u03bbx. P x \u2228 Q x) xs)\"\n    by (simp only: algunos.simps(2))\n  also have \"... = ((P x \u2228 Q x) \u2228 algunos P xs \u2228 algunos Q xs)\"\n    by (simp only: HI)\n  also have \"... = (P x \u2228 Q x \u2228 algunos P xs \u2228 algunos Q xs)\"\n    by (simp only: disj_assoc)\n  also have \"... = (P x \u2228 algunos P xs \u2228 Q x \u2228 algunos Q xs)\"\n    by (simp only: disj_left_commute)\n  also have \"... = ((P x \u2228 algunos P xs) \u2228 (Q x \u2228 algunos Q xs))\"\n    by (simp only: disj_assoc)\n  also have \"... = (algunos P (x#xs) \u2228 algunos Q (x#xs))\"\n    by (simp only: algunos.simps(2))\n  finally show \"algunos (\u03bbx. P x \u2228 Q x) (x#xs) = \n                (algunos P (x#xs) \u2228 algunos Q (x#xs))\"\n    by this\nqed\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 11.1. Demostrar o refutar autom\u00e1ticamente\n     algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\n  ---------------------------------------------------------------------\u203a\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\"\n  by (induct xs) simp_all\n     \ntext \u2039------------------------------------------------------------------ \n  Ejercicio 11.2. Demostrar o refutar detalladamente\n     algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\n  ---------------------------------------------------------------------\u203a\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)) [])\" \n    by simp\nnext\n  fix a xs\n  assume \"algunos P xs = (\u00ac todos (\u03bbx. (\u00ac P x)) xs)\"\n  then show \"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 \u2039\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\u203a\n\nfun estaEn :: \"'a \u21d2 'a list \u21d2 bool\" where\n  \"estaEn x []     = False\"\n| \"estaEn x (a#xs) = (a=x \u2228 estaEn x xs)\"  \n\nvalue \"estaEn (2::nat) [3,2,4] = True\"\nvalue \"estaEn (1::nat) [3,2,4] = False\"\n\ntext \u2039------------------------------------------------------------------ \n  Ejercicio 13. Expresar la relaci\u00f3n existente entre estaEn y  algunos. \n  Demostrar dicha relaci\u00f3n de forma autom\u00e1tica y detallada.\n  ---------------------------------------------------------------------\u203a\n\ntext \u2039Soluci\u00f3n: La relaci\u00f3n es \n     estaEn y xs = algunos (\u03bbx. x=y) xs\n  En efecto,\u203a\n\nlemma \"estaEn x xs = algunos (\u03bby. y=x) xs\"\n  by (induct xs) auto\n\n(* La demostraci\u00f3n estructurada es *)\nlemma \"estaEn x xs = algunos (\u03bby. y=x) xs\"\nproof (induct xs) \n  show \"estaEn x [] = algunos (\u03bby. y=x) []\"\n    by simp\nnext\n  fix a xs\n  assume HI: \"estaEn x xs = algunos (\u03bby. y=x) xs\"\n  have \"estaEn x (a#xs) = algunos  (\u03bby. y=x) (a#xs)\"  \n    using HI by simp\n  then show \"estaEn x (a#xs) = algunos (\u03bby. y=x) (a#xs)\" \n    by simp\nqed\n\n(* La demostraci\u00f3n detallada es *)\nlemma \"estaEn x xs = algunos (\u03bby. y=x) xs\"\nproof (induct xs) \n  have \"estaEn x [] = False\"\n    by (simp only: estaEn.simps(1))\n  also have \"... = algunos (\u03bby. y=x) []\"\n    by (simp only: algunos.simps(1))\n  finally show \"estaEn x [] = algunos (\u03bby. y=x) []\"\n    by this\nnext\n  fix a xs\n  assume HI: \"estaEn x xs = algunos (\u03bby. y=x) xs\"\n  have \"estaEn x (a#xs) = ((a=x) \u2228 estaEn x xs)\"  \n    by (simp only: estaEn.simps(2))\n  also have \"... = ((a=x) \u2228 algunos  (\u03bby. y=x) xs) \" \n    using HI by (simp only :)\n  also have \"... = algunos  (\u03bby. y=x) (a#xs)\"  \n    by (simp only: algunos.simps(2))\n  finally show \"estaEn x (a#xs) = algunos (\u03bby. y=x) (a#xs)\" \n    by this\nqed\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 han comentado las soluciones de la 4\u00aa relaci\u00f3n de ejercicios de cuantificadores sobre listas. Para cada propiedad se dan tres demostraciones en Isabelle\/HOL: la primera autom\u00e1tica, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de HOL&#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":[333],"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\/6875"}],"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=6875"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6875\/revisions"}],"predecessor-version":[{"id":6880,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6875\/revisions\/6880"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6875"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6875"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6875"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}