{"id":4713,"date":"2015-01-08T22:03:37","date_gmt":"2015-01-08T21:03:37","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4713"},"modified":"2015-01-09T09:05:24","modified_gmt":"2015-01-09T08:05:24","slug":"ra2014-conjuntos-funciones-y-relacione","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2014-conjuntos-funciones-y-relacione\/","title":{"rendered":"RA2014: Conjuntos, funciones y relaciones"},"content":{"rendered":"<p>En 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 trabajar en Isabelle\/HOL con conjuntos, funciones y relaciones.<\/p>\n<p>La clase se ha basado en la siguiente teor\u00eda Isabelle\/HOL<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* Tema 9: Conjuntos, funciones y relaciones *}\n\ntheory T9\nimports Main \nbegin\n\nsection {* Conjuntos *}\n\nsubsection {* Operaciones con conjuntos *}\n\ntext {*\n  Nota. La teor\u00eda elemental de conjuntos es HOL\/Set.thy.\n\n  Nota. En un conjunto todos los elemento son del mismo tipo (por\n  ejemplo, del tipo \u03c4) y el conjunto tiene tipo (en el ejemplo, \"\u03c4 set\"). \n\n  Reglas de la intersecci\u00f3n:\n  \u00b7 IntI:  \u27e6c \u2208 A; c \u2208 B\u27e7 \u27f9 c \u2208 A \u2229 B\n  \u00b7 IntD1: c \u2208 A \u2229 B \u27f9 c \u2208 A\n  \u00b7 IntD2: c \u2208 A \u2229 B \u27f9 c \u2208 B\n\n  Nota. Propiedades del complementario:\n  \u00b7 Compl_iff: (c \u2208 - A) = (c \u2209 A)\n  \u00b7 Compl_Un:  - (A \u222a B) = - A \u2229 - B\n\n  Nota. El conjunto vac\u00edo se representa por {} y el universal por UNIV. \n\n  Nota. Propiedades de la diferencia y del complementario:\n  \u00b7 Diff_disjoint:   A \u2229 (B - A) = {}\n  \u00b7 Compl_partition: A \u222a - A = UNIV\n\n  Nota. Reglas de la relaci\u00f3n de subconjunto:\n  \u00b7 subsetI: (\u22c0x. x \u2208 A \u27f9 x \u2208 B) \u27f9 A \u2286 B\n  \u00b7 subsetD: \u27e6A \u2286 B; c \u2208 A\u27e7 \u27f9 c \u2208 B   \n*}\n\ntext {*\n  Ejemplo: A \u222a B \u2286 C syss A \u2286 C \u2227 B \u2286 C.   \n*}\n\nlemma \"(A \u222a B \u2286 C) = (A \u2286 C \u2227 B \u2286 C)\"\nby blast\n\ntext {* \n  Ejemplo: A \u2286 -B syss B \u2286 -A.   \n*}\n\nlemma \"(A \u2286 -B) = (B \u2286 -A)\"\nby blast\n\ntext {*\n  Principio de extensionalidad de conjuntos:\n  \u00b7 set_ext: (\u22c0x. (x \u2208 A) = (x \u2208 B)) \u27f9 A = B\n\n  Reglas de la igualdad de conjuntos:\n  \u00b7 equalityI: \u27e6A \u2286 B; B \u2286 A\u27e7 \u27f9 A = B\n  \u00b7 equalityE: \u27e6A = B; \u27e6A \u2286 B; B \u2286 A\u27e7 \u27f9 P\u27e7 \u27f9 P   \n*}\n\ntext {*\n  Lema. [Analog\u00eda entre intersecci\u00f3n y conjunci\u00f3n]\n  \"x \u2208 A \u2229 B\" syss \"x \u2208 A\" y \"x \u2208 B\". \n*}\n\nlemma \"(x \u2208 A \u2229 B) = (x \u2208 A \u2227 x \u2208 B)\" \nby simp\n\ntext {*\n  Lema. [Analog\u00eda entre uni\u00f3n y disyunci\u00f3n]\n  x \u2208 A \u222a B syss x \u2208 A \u00f3 x \u2208 B.   \n*}\n\nlemma \"(x \u2208 A \u222a B) = (x \u2208 A \u2228 x \u2208 B)\" \nby simp\n\ntext {*\n  Lema. [Analog\u00eda entre subconjunto e implicaci\u00f3n]\n  A \u2286 B syss para todo x, si x \u2208 A entonces x \u2208 B.   \n*}\n\nlemma \"(A \u2286 B) = (\u2200 x. x \u2208 A \u27f6 x \u2208 B)\" \nby auto\n\ntext {*\n  Lema. [Analog\u00eda entre complementario y negaci\u00f3n]\n  x pertenece al complementario de A syss x no pertenece a A.   \n*}\n\nlemma \"(x \u2208 -A) = (x \u2209 A)\" \nby simp\n\nsubsection {* Notaci\u00f3n de conjuntos finitos \n*}\n\ntext {*\n  Nota. La teor\u00eda de conjuntos finitos es HOL\/Finite_Set.thy.\n\n  Nota. Los conjuntos finitos se definen por inducci\u00f3n a partir de las\n  siguientes reglas inductivas:\n  \u00b7 El conjunto vac\u00edo es un conjunto finito.\n    \u00b7 emptyI: \"finite {}\"\n  \u00b7 Si se le a\u00f1ade un elemento a un conjunto finito se obtiene otro\n    conjunto finito. \n    \u00b7 insertI: \"finite A \u27f9 finite (insert a A)\" \n\n  A continuaci\u00f3n se muestran ejemplos de conjuntos finitos.   \n*}\n\nlemma \n  \"insert 2 {} = {2} \u2227\n   insert 3 {2} = {2,3} \u2227\n   insert 2 {2,3} = {2,3} \u2227\n   {2,3} = {3,2,3,2,2}\"\nby auto\n\ntext {*\n  Nota. Los conjuntos finitos se representan con la notaci\u00f3n conjuntista\n  habitual: los elementos entre llaves y separados por comas. \n*}\n\ntext {*\n  Ejemplo: {a,b} \u222a {c,d} = {a,b,c,d}   \n*}\n\nlemma \"{a,b} \u222a {c,d} = {a,b,c,d}\" \nby blast\n\ntext {*\n  Ejemplo de conjetura falsa y su refutaci\u00f3n. \n*}\n\nlemma \"{a,b} \u2229 {b,c} = {b}\" \nnitpick\noops\n\ntext {*\n  Ejemplo con la conjetura corregida.   \n*}\n\nlemma \"{a,b} \u2229 {b,c} = (if a=c then {a,b} else {b})\"\nby auto\n\ntext {*\n  Sumas y productos de conjuntos finitos:\n  \u00b7 (setsum f A) es la suma de la aplicaci\u00f3n de f a los elementos del\n    conjunto finito A,  \n  \u00b7 (setprod f A) es producto de la aplicaci\u00f3n de f a los elementos del\n    conjunto finito A,  \n  \u00b7 \u2211A es la suma de los elementos del conjunto finito A,\n  \u00b7 \u220fA es el producto de los elementos del conjunto finito A.\n\n  Ejemplos de definiciones recursivas sobre conjuntos finitos: \n  Sea A un conjunto finito de n\u00fameros naturales.\n  \u00b7 sumaConj A es la suma de los elementos A.\n  \u00b7 productoConj A es el producto de los elementos de A.\n  \u00b7 sumaCuadradosConj A es la suma de los cuadrados de los elementos A. \n*}\n\ndefinition sumaConj :: \"nat set \u21d2 nat\" where\n  \"sumaConj S \u2261 \u2211S\"\n\nvalue \"sumaConj {2,5,3}\" -- \"= 10\"\n\ndefinition productoConj :: \"nat set \u21d2 nat\" where\n  \"productoConj S \u2261 \u220fS\"\n\ndefinition sumaCuadradosConj :: \"nat set \u21d2 nat\" where\n  \"sumaCuadradosConj S \u2261 setsum (\u03bbx. x*x) S\"\n\nvalue \"sumaCuadradosConj {2,5,3}\" -- \"= 38\"\n\ntext {*\n  Nota. Para simplificar lo que sigue, declaramos las anteriores\n  definiciones como reglas de simplificaci\u00f3n.   \n*}\n\ndeclare sumaConj_def[simp]\ndeclare productoConj_def[simp]\ndeclare sumaCuadradosConj_def[simp]\n\ntext {*\n  Ejemplos de evaluaci\u00f3n de las anteriores definiciones recursivas.   \n*}\n\nlemma \n  \"sumaConj {1,2,3,4} = 10 \u2227\n   productoConj {1,2,3} = productoConj {3,2} \u2227 \n   sumaCuadradosConj {1,2,3,4} = 30\"\nby simp\n\ntext {*\n  Inducci\u00f3n sobre conjuntos finitos: Para demostrar que todos los\n  conjuntos finitos tienen una propiedad P basta probar que\n  \u00b7 El conjunto vac\u00edo tiene la propiedad P.\n  \u00b7 Si a un conjunto finito que tiene la propiedad P se le a\u00f1ade un\n    nuevo elemento, el conjunto obtenido sigue teniendo la propiedad P. \n  En forma de regla\n  \u00b7 finite_induct: \u27e6finite F; \n                    P {}; \n                    \u22c0x F. \u27e6finite F; x \u2209 F; P F\u27e7 \u27f9 P ({x} \u222a F)\u27e7 \n                   \u27f9 P F   \n*}\n\ntext {* \n  Ejemplo de inducci\u00f3n sobre conjuntos finitos: Sea S un conjunto finito\n  de n\u00fameros naturales. Entonces todos los elementos de S son menores o\n  iguales que la suma de los elementos de S. \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"finite S \u27f9 \u2200x\u2208S. x \u2264 sumaConj S\"\nby (induct rule: finite_induct) auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma sumaConj_acota: \n  \"finite S \u27f9 \u2200x\u2208S. x \u2264 sumaConj S\"\nproof (induct rule: finite_induct)\n  show \"\u2200x \u2208 {}. x \u2264 sumaConj {}\" by simp\nnext\n  fix x and F\n  assume fF: \"finite F\" \n     and xF: \"x \u2209 F\" \n     and HI: \"\u2200 x\u2208F. x \u2264 sumaConj F\"\n  show \"\u2200y \u2208 insert x F. y \u2264 sumaConj (insert x F)\"\n  proof \n    fix y \n    assume \"y \u2208 insert x F\"\n    show \"y \u2264 sumaConj (insert x F)\"\n    proof (cases \"y = x\")\n      assume \"y = x\"\n      hence \"y \u2264 x + (sumaConj F)\" by simp\n      also have \"\u2026 = sumaConj (insert x F)\" using fF xF by simp\n      finally show ?thesis .\n    next\n      assume \"y \u2260 x\"\n      hence \"y \u2208 F\" using `y \u2208 insert x F` by simp\n      hence \"y \u2264 sumaConj F\" using HI by blast\n      also have \"\u2026 \u2264 x + (sumaConj F)\" by simp\n      also have \"\u2026 = sumaConj (insert x F)\" using fF xF by simp\n      finally show ?thesis .\n    qed\n  qed\nqed\n\nsubsection {* Definiciones por comprensi\u00f3n *}\n\ntext {*\n  El conjunto de los elementos que cumple la propiedad P se representa\n  por {x. P}. \n\n  Reglas de comprensi\u00f3n (relaci\u00f3n entre colecci\u00f3n y pertenencia):\n  \u00b7 mem_Collect_eq: (a \u2208 {x. P x}) = P a\n  \u00b7 Collect_mem_eq: {x. x \u2208 A} = A   \n*}\n\ntext {*\n  Ejemplo de comprensi\u00f3n: {x. P x \u2228 x \u2208 A} = {x. P x} \u222a A   \n*}\n\nlemma \"{x. P x \u2228 x \u2208 A} = {x. P x} \u222a A\"\nby blast\n\ntext {*\n  Ejemplo de comprensi\u00f3n: {x. P x \u27f6 Q x} = -{x. P x} \u222a {x. Q x}   \n*}\n\nlemma \"{x. P x \u27f6 Q x} = -{x. P x} \u222a {x. Q x}\"\nby blast\n\ntext {*\n  Ejemplo con la sintaxis general de comprensi\u00f3n.   \n     {p*q | p q. p \u2208 prime \u2227 q \u2208 prime} = \n     {z. \u2203p q. z = p*q \u2227 p \u2208 prime \u2227 q \u2208 prime}   \n*}\n\nlemma \n  \"{p*q | p q. p \u2208 prime \u2227 q \u2208 prime} = \n   {z. \u2203p q. z = p*q \u2227 p \u2208 prime \u2227 q \u2208 prime}\"\nby blast\n\ntext {*\n   En HOL, la notaci\u00f3n conjuntista es az\u00facar sint\u00e1ctica:\n   \u00b7 x \u2208 A  es equivalente a A(x).\n   \u00b7 {x. P} es equivalente a \u03bbx. P.\n*}\n\ntext {*\n  Ejemplo de definici\u00f3n por comprensi\u00f3n: El conjunto de los pares es el\n  de los n\u00fameros n para los que existe un m tal que n = 2*m.\n*}\n\ndefinition Pares :: \"nat set\" where\n  \"Pares \u2261 {n. \u2203m. n = 2*m }\"\n\ntext {*\n  Ejemplo. Los n\u00fameros 2 y 34 son pares.\n*}\n\nlemma \n  \"2 \u2208 Pares \u2227\n   34 \u2208 Pares\" \nby (simp add: Pares_def)\n\ntext {*\n  Definici\u00f3n. El conjunto de los impares es el de los n\u00fameros n para los\n  que existe un m tal que n = 2*m + 1.\n*}\n\ndefinition Impares :: \"nat set\" where\n  \"Impares \u2261 {n. \u2203m. n = 2*m + 1 }\"\n\ntext {*\n  Ejemplo con las reglas de intersecci\u00f3n y comprensi\u00f3n: El conjunto de\n  los pares es disjunto con el de los impares. \n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"x \u2209 (Pares \u2229 Impares)\"\nproof \n  fix x assume S: \"x \u2208 (Pares \u2229 Impares)\"\n  hence \"x \u2208 Pares\" by (rule IntD1)\n  hence \"\u2203m. x = 2 * m\" by (simp only: Pares_def mem_Collect_eq)\n  then obtain p where p: \"x = 2 * p\" .. \n  from S have \"x \u2208 Impares\" by (rule IntD2)\n  hence \"\u2203 m. x = 2 * m + 1\" by (simp only: Impares_def mem_Collect_eq)\n  then obtain q where q: \"x = 2 * q + 1\" .. \n  from p and q show \"False\" by arith\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"x \u2209 (Pares \u2229 Impares)\"\nproof \n  fix x assume S: \"x \u2208 (Pares \u2229 Impares)\"\n  hence \"x \u2208 Pares\" ..\n  hence \"\u2203m. x = 2 * m\" by (simp only: Pares_def mem_Collect_eq)\n  then obtain p where p: \"x = 2 * p\" .. \n  from S have \"x \u2208 Impares\" ..\n  hence \"\u2203 m. x = 2 * m + 1\" by (simp only: Impares_def mem_Collect_eq)\n  then obtain q where q: \"x = 2 * q + 1\" .. \n  from p and q show \"False\" by arith\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"x \u2209 (Pares \u2229 Impares)\"\nby (auto simp add: Pares_def Impares_def mem_Collect_eq, arith)\n\nsubsection {* Cuantificadores acotados *}\n\ntext {*\n  Reglas de cuantificador universal acotado (\"bounded\"):\n  \u00b7 ballI: (\u22c0x. x \u2208 A \u27f9 P x) \u27f9 \u2200x\u2208A. P x\n  \u00b7 bspec: \u27e6\u2200x\u2208A. P x; x \u2208 A\u27e7 \u27f9 P x\n\n  Reglas de cuantificador existencial acotado (\"bounded\"):\n  \u00b7 bexI: \u27e6P x; x \u2208 A\u27e7 \u27f9 \u2203x\u2208A. P x\n  \u00b7 bexE: \u27e6\u2203x\u2208A. P x; \u22c0x. \u27e6x \u2208 A; P x\u27e7 \u27f9 Q\u27e7 \u27f9 Q\n\n  Reglas de la uni\u00f3n indexada:\n  \u00b7 UN_iff: (b \u2208 (\u22c3x\u2208A. B x)) = (\u2203x\u2208A. b \u2208 B x)\n  \u00b7 UN_I:   \u27e6a \u2208 A; b \u2208 B a\u27e7 \u27f9 b \u2208 (\u22c3x\u2208A. B x)\n  \u00b7 UN_E:   \u27e6b \u2208 (\u22c3x\u2208A. B x); \u22c0x. \u27e6x \u2208 A; b \u2208 B x\u27e7 \u27f9 R\u27e7 \u27f9 R\n\n  Reglas de la uni\u00f3n de una familia:\n  \u00b7 Union_def: \u22c3S = (\u22c3x\u2208S. x)\n  \u00b7 Union_iff: (A \u2208 \u22c3C) = (\u2203X\u2208C. A \u2208 X)\n\n  Reglas de la intersecci\u00f3n indexada:\n  \u00b7 INT_iff: (b \u2208 (\u22c2x\u2208A. B x)) = (\u2200x\u2208A. b \u2208 B x)\n  \u00b7 INT_I:   (\u22c0x. x \u2208 A \u27f9 b \u2208 B x) \u27f9 b \u2208 (\u22c2x\u2208A. B x)\n  \u00b7 INT_E:   \u27e6b \u2208 (\u22c2x\u2208A. B x); b \u2208 B a \u27f9 R; a \u2209 A \u27f9 R\u27e7 \u27f9 R\n\n  Reglas de la intersecci\u00f3n de una familia:\n  \u00b7 Inter_def: \u22c2S = (\u22c2x\u2208S. x)\n  \u00b7 Inter_iff: (A \u2208 \u22c2C) = (\u2200X\u2208C. A \u2208 X)\n\n  Abreviaturas:\n  \u00b7 \"Collect P\" es lo mismo que \"{x. P}\".\n  \u00b7 \"All P\"     es lo mismo que \"\u2200x. P x\".\n  \u00b7 \"Ex P\"      es lo mismo que \"\u2203x. P x\".\n  \u00b7 \"Ball A P\"  es lo mismo que \"\u2200x\u2208A. P x\".\n  \u00b7 \"Bex A P\"   es lo mismo que \"\u2203x\u2208A. P x\".\n*}\n\nsubsection {* Conjuntos finitos y cardinalidad *}\n\ntext {*\n  El n\u00famero de elementos de un conjunto finito A es el cardinal de A y\n  se representa por \"card A\".\n*}\n\ntext {*\n  Ejemplos de cardinales de conjuntos finitos.\n*}\n\nlemma \n  \"card {} = 0 \u2227\n   card {4} = 1 \u2227\n   card {4,1} = 2 \u2227\n   x \u2260 y \u27f9 card {x,y} = 2\" \nby simp\n\ntext {* \n  Propiedades de cardinales:\n  \u00b7 Cardinal de la uni\u00f3n de conjuntos finitos:\n    card_Un_Int: \u27e6finite A; finite B\u27e7 \n                 \u27f9 card A + card B = card (A \u222a B) + card (A \u2229 B)\" \n  \u00b7 Cardinal del conjunto potencia: \n    card_Pow: finite A \u27f9 card (Pow A) = 2 ^ card A\n*}\n\nsection {* Funciones *}\n\ntext {* \n  La teor\u00eda de funciones es HOL\/Fun.thy. \n*}\n\nsubsection {* Nociones b\u00e1sicas de funciones *}\n\ntext {*\n  Principio de extensionalidad para funciones:\n  \u00b7 ext: (\u22c0x. f x = g x) \u27f9 f = g\n\n  Actualizaci\u00f3n de funciones  \n  \u00b7 fun_upd_apply: (f(x := y)) z = (if z = x then y else f z)\n  \u00b7 fun_upd_upd:   f(x := y, x := z) = f(x := z)\n\n  Funci\u00f3n identidad\n  \u00b7 id_def: id \u2261 \u03bbx. x\n\n  Composici\u00f3n de funciones:\n  \u00b7 o_def: f \u2218 g = (\u03bbx. f (g x))\n\n  Asociatividad de la composici\u00f3n:\n  \u00b7 o_assoc: f \u2218 (g \u2218 h) = (f \u2218 g) \u2218 h\n*}\n\nsubsection {* Funciones inyectivas, suprayectivas y biyectivas *}\n\ntext {*\n  Funci\u00f3n inyectiva sobre A:\n  \u00b7 inj_on_def: inj_on f A \u2261 \u2200x\u2208A. \u2200y\u2208A. f x = f y \u27f6 x = y\n\n  Nota. \"inj f\" es una abreviatura de \"inj_on f UNIV\".\n\n  Funci\u00f3n suprayectiva:\n  \u00b7 surj_def: surj f \u2261 \u2200y. \u2203x. y = f x\n\n  Funci\u00f3n biyectiva:\n  \u00b7 bij_def: bij f \u2261 inj f \u2227 surj f\n\n  Propiedades de las funciones inversas:\n  \u00b7 inv_f_f:      inj f \u27f9 inv f (f x) = x\n  \u00b7 surj_f_inv_f: surj f \u27f9 f (inv f y) = y\n  \u00b7 inv_inv_eq:   bij f \u27f9 inv (inv f) = f\n\n  Igualdad de funciones (por extensionalidad):\n  \u00b7 fun_eq_iff: (f = g) = (\u2200x. f x = g x)\n*}\n\ntext {*\n  Ejemplo de lema de demostraci\u00f3n de propiedades de funciones: Una\n  funci\u00f3n inyectiva puede cancelarse en el lado izquierdo de la\n  composici\u00f3n de funciones. \n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \n  assumes \"inj f\"\n  shows \"(f \u2218 g = f \u2218 h) = (g = h)\"\nproof \n  assume \"f \u2218 g = f \u2218 h\"\n  show \"g = h\"\n  proof\n    fix x\n    have \"(f \u2218 g)(x) = (f \u2218 h)(x)\" using `f \u2218 g = f \u2218 h` by simp\n    hence \"f(g(x)) = f(h(x))\" by simp\n    thus \"g(x) = h(x)\" using `inj f` by (simp add:inj_on_def)\n  qed\nnext\n  assume \"g = h\"\n  show \"f \u2218 g = f \u2218 h\"\n  proof\n    fix x\n    have \"(f \u2218 g) x = f(g(x))\" by simp\n    also have \"\u2026 = f(h(x))\" using `g = h` by simp\n    also have \"\u2026 = (f \u2218 h) x\" by simp\n    finally show \"(f \u2218 g) x = (f \u2218 h) x\" by simp\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \n  assumes \"inj f\"\n  shows \"(f \u2218 g = f \u2218 h) = (g = h)\"\nproof \n  assume \"f \u2218 g = f \u2218 h\" \n  thus \"g = h\" using `inj f` by (simp add: inj_on_def fun_eq_iff) \nnext\n  assume \"g = h\" \n  thus \"f \u2218 g = f \u2218 h\" by auto\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \n  assumes \"inj f\"\n  shows \"(f \u2218 g = f \u2218 h) = (g = h)\"\nusing assms\nby (auto simp add: inj_on_def fun_eq_iff) \n\nsubsubsection {* Funci\u00f3n imagen *}\n\ntext {*\n  Imagen de un conjunto mediante una funci\u00f3n:\n  \u00b7 image_def: f ` A = {y. (\u2203x\u2208A. y = f x)\n\n  Propiedades de la imagen:\n  \u00b7 image_compose: (f \u2218 g)`r = f`g`r\n  \u00b7 image_Un:      f`(A \u222a B) = f`A \u222a f`B \n  \u00b7 image_Int:     inj f \u27f9 f`(A \u2229 B) = f`A \u2229 f`B\" \n*}\n\ntext {*\n  Ejemplo de demostraci\u00f3n de propiedades de la imagen:\n     f`A \u222a g`A = (\u22c3x\u2208A. {f x, g x})\n*}\n\nlemma \"f`A \u222a g`A = (\u22c3x\u2208A. {f x, g x})\"\nby auto\n\ntext {*\n  Ejemplo de demostraci\u00f3n de propiedades de la imagen:\n     f`{(x,y). P x y} = {f(x,y) | x y. P x y}\n*}\n\nlemma \"f`{(x,y). P x y} = {f(x,y) | x y. P x y}\"\nby auto\n\ntext {*\n  El rango de una funci\u00f3n (\"range f\") es la imagen del universo (\"f`UNIV\"). \n\n  Imagen inversa de un conjunto:\n  \u00b7 vimage_def: f -` B \u2261 {x. f x : B}\n\n  Propiedad de la imagen inversa de un conjunto:\n  \u00b7 vimage_Compl: f -` (-A) = -(f -` A)\n*}\n\nsection {* Relaciones *}\n\nsubsection {* Relaciones b\u00e1sicas *}\n\ntext {*\n  La teor\u00eda de relaciones es HOL\/Relation.thy.\n\n  Las relaciones son conjuntos de pares.\n\n  Relaci\u00f3n identidad:\n  \u00b7 Id_def: Id \u2261 {p. \u2203x. p = (x,x)}\n\n  Composici\u00f3n de relaciones:\n  \u00b7 rel_comp_def: r O s \u2261 {(x,z). \u2203y. (x, y) \u2208 r \u2227 (y, z) \u2208 s}\n\n  Propiedades:\n  \u00b7 R_O_Id:        R O Id = R\n  \u00b7 rel_comp_mono: \u27e6r' \u2286 r; s' \u2286 s\u27e7 \u27f9 (r' O s') \u2286 (r O s)\n\n  Imagen inversa de una relaci\u00f3n:\n  \u00b7 converse_iff: ((a,b) \u2208 r\\<^bsup>\\<^sup>-1\\<^esup>) = ((b,a) \u2208 r)\n\n  Propiedad de la imagen inversa de una relaci\u00f3n:\n  \u00b7 converse_rel_comp: (r O s)\\<^bsup>-1\\<^esup> = s\\<^bsup>-1\\<^esup> O r\\<^bsup>-1\\<^esup>\n\n  Imagen de un conjunto mediante una relaci\u00f3n:\n  \u00b7 Image_iff: (b \u2208 r``A) = (\u2203x:A. (x, b) \u2208 r)\n\n  Dominio de una relaci\u00f3n:\n  \u00b7 Domain_iff: (a \u2208 Domain r) = (\u2203y. (a, y) \u2208 r)\n\n  Rango de una relaci\u00f3n:\n  \u00b7 Range_iff: (a \u2208 Range r) = (\u2203y. (y,a) \u2208 r)\n*}\n\nsubsection {* Clausura reflexiva y transitiva *}\n\ntext {*\n  La teor\u00eda de la clausura reflexiva y transitiva de una relaci\u00f3n es\n  HOL\/Transitive_Closure.thy.\n\n  Potencias de relaciones:\n  \u00b7 R ^^ 0 = Id\n  \u00b7 R ^^ (Suc n) = (R ^^ n) O R\n  \n  La clausura reflexiva y transitiva de la relaci\u00f3n r es la menor\n  soluci\u00f3n de la ecuaci\u00f3n: \n  \u00b7 rtrancl_unfold: r\\<^sup>* = Id \u222a (r\\<^sup>* O r)\n  \n  Propiedades b\u00e1sicas de la clausura reflexiva y transitiva:\n  \u00b7 rtrancl_refl:   (a,a) \u2208 r\\<^sup>*\n  \u00b7 r_into_rtrancl: p \u2208 r \u27f9 p \u2208 r\\<^sup>*\n  \u00b7 rtrancl_trans:  \u27e6(a,b) \u2208 r\\<^sup>*; (b,c) \u2208 r\\<^sup>*\u27e7 \u27f9 (a,c) \u2208 r\\<^sup>*\n  \n  Inducci\u00f3n sobre la clausura reflexiva y transitiva\n  \u00b7 rtrancl_induct: \u27e6(a,b) \u2208 r\\<^sup>*; \n                     P b; \n                     \u22c0y z. \u27e6(y,z) \u2208 r; (z,b) \u2208 r\\<^sup>*; P z\u27e7 \u27f9 P y\u27e7\n                    \u27f9 P a\n  \n  Idempotencia de la clausura reflexiva y transitiva:\n  \u00b7 rtrancl_idemp: (r\\<^sup>* )\\<^sup>* = r\\<^sup>*\n  \n  Reglas de introducci\u00f3n de la clausura transitiva:\n  \u00b7 r_into_trancl': p \u2208 r \u27f9 p \u2208 r\\<^sup>+\n  \u00b7 trancl_trans:   \u27e6(a,b) \u2208 r\\<^sup>+; (b,c) \u2208 r\\<^sup>+\u27e7 \u27f9 (a,c) \u2208 r\\<^sup>+\n\n  Ejemplo de propiedad:\n  \u00b7 trancl_converse: (r\u00af\u00b9)\\<^sup>+ = (r\\<^sup>+)\u00af\u00b9\n*}\n\nsubsection {* Una demostraci\u00f3n elemental *}\n\ntext {*\n  Se desea demostrar que la clausura reflexiva y transitiva conmuta con\n  la inversa (cl_rtrans_inversa). Para demostrarlo introducimos dos lemas\n  auxiliares: cl_rtrans_inversaD y cl_rtrans_inversaI.\n*}\n\n-- \"La demostraci\u00f3n detallada del primer lema es\"\nlemma cl_rtrans_inversaD: \n  \"(x,y) \u2208 (r\u00af\u00b9)\\<^sup>* \u27f9 (y,x) \u2208 r\\<^sup>*\"\nproof (induct rule:rtrancl_induct)\n  show \"(x,x) \u2208 r\\<^sup>*\" by (rule rtrancl_refl) \nnext\n  fix y z\n  assume \"(x,y) \u2208 (r\u00af\u00b9)\\<^sup>*\" and \"(y,z) \u2208 r\u00af\u00b9\" and \"(y,x) \u2208 r\\<^sup>*\"\n  show \"(z,x) \u2208 r\\<^sup>*\"\n  proof (rule rtrancl_trans)\n    show \"(z,y) \u2208 r\\<^sup>*\" using `(y,z) \u2208 r\u00af\u00b9` by simp\n  next\n    show \"(y,x) \u2208 r\\<^sup>*\" using `(y,x) \u2208 r\\<^sup>*` by simp\n  qed   \nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica del primer lema es\"\nlemma  cl_rtrans_inversaD2: \n  \"(x,y) \u2208 (r\u00af\u00b9)\\<^sup>* \u27f9 (y,x) \u2208 r\\<^sup>*\"\nby (induct rule: rtrancl_induct) \n   (auto simp add: rtrancl_refl rtrancl_trans)\n\n-- \"La demostraci\u00f3n detallada del segundo lema es\"\nlemma cl_rtrans_inversaI: \n  \"(y,x) \u2208 r\\<^sup>* \u27f9 (x,y) \u2208 (r\u00af\u00b9)\\<^sup>*\"\nproof (induct rule: rtrancl_induct)\n  show \"(y,y) \u2208 (r\u00af\u00b9)\\<^sup>*\" by (rule rtrancl_refl) \nnext\n  fix u z\n  assume \"(y,u) \u2208 r\\<^sup>*\" and \"(u,z) \u2208 r\" and \"(u,y) \u2208 (r\u00af\u00b9)\\<^sup>*\"\n  show \"(z,y) \u2208 (r\u00af\u00b9)\\<^sup>*\"\n  proof (rule rtrancl_trans)\n    show \"(z,u) \u2208 (r\u00af\u00b9)\\<^sup>*\" using `(u,z) \u2208 r` by auto\n  next\n    show \"(u,y) \u2208 (r\u00af\u00b9)\\<^sup>*\" using `(u,y) \u2208 (r\u00af\u00b9)\\<^sup>*` by simp\n  qed\nqed\n\n-- \"La demostraci\u00f3n detalla del teorema es\"\ntheorem cl_rtrans_inversa: \n  \"(r\u00af\u00b9)\\<^sup>* = (r\\<^sup>*)\u00af\u00b9\"\nproof\n  show \"(r\u00af\u00b9)\\<^sup>* \u2286 (r\\<^sup>*)\u00af\u00b9\" by (auto simp add:cl_rtrans_inversaD)\nnext\n  show \"(r\\<^sup>*)\u00af\u00b9 \u2286 (r\u00af\u00b9)\\<^sup>*\" by (auto simp add:cl_rtrans_inversaI)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica del teorema es\"\ntheorem \"(r\u00af\u00b9)\\<^sup>* = (r\\<^sup>*)\u00af\u00b9\"\nby (auto intro: cl_rtrans_inversaI dest: cl_rtrans_inversaD)\n\nsection {* Relaciones bien fundamentadas e inducci\u00f3n *}\n\ntext {*\n  La teor\u00eda de las relaciones bien fundamentadas es \n  HOL\/Wellfounded_Relations.thy.\n\n  La relaci\u00f3n-objeto \"less_than\" es el orden de los naturales definido por\n  \u00b7 less_than = pred_nat\\<^bsup>+\\<^esup>\n  donde pred_nat est\u00e1 definida por \n  \u00b7 pred_nat = {(m, n). n = Suc m}\n\n  La caracterizaci\u00f3n de less_than es\n  \u00b7 less_than_iff: ((x,y) \u2208 less_than) = (x < y)\n\n  La relaci\u00f3n less_than est\u00e1 bien fundamentada\n  \u00b7 wf_less_than:  wf less_than\n\n  Notas sobre medidas:\n  \u00b7 Imagen inversa de una relaci\u00f3n mediante una funci\u00f3n:\n    \u00b7 inv_image_def: inv_image r f \u2261 {(x,y). (f x,f y) \u2208 r}\n  \u00b7 Conservaci\u00f3n de la buena fundamentaci\u00f3n:\n    \u00b7 wf_inv_image: wf r \u27f9 wf (inv_image r f)\n  \u00b7 Definici\u00f3n de la medida:\n    \u00b7 measure_def: measure \u2261 inv_image less_than\n  \u00b7 Buena fundamentaci\u00f3n de la medida:\n    \u00b7 wf_measure: wf (measure f)\n*}\n\ntext {*\n  Notas sobre el producto lexicogr\u00e1fico:\n  \u00b7 Definici\u00f3n del producto lexicogr\u00e1fico (lex_prod_def):\n    ra <*lex*> rb \u2261 {((a,b),(a',b')). (a,a') \u2208 ra \u2228 \n                                      (a = a' \u2227 (b,b') \u2208 rb)}\n  \u00b7 Conservaci\u00f3n de la buena fundamentaci\u00f3n:\n    \u00b7 wf_lex_prod: \u27e6wf ra; wf rb\u27e7 \u27f9 wf (ra <*lex*> rb)\n\n  El orden de multiconjuntos est\u00e1 en la teor\u00eda HOL\/Library\/Multiset.thy.\n\n  Inducci\u00f3n sobre relaciones bien fundamentadas:\n  \u00b7 wf_induct: \u27e6wf r; \u22c0x. (\u22c0y. (y,x) \u2208 r \u27f9 P y) \u27f9 P x\u27e7 \u27f9 P a\n*}\n\nsection {* Puntos fijos *}\n\ntext {*\n  La teor\u00eda de los puntos fijos se aplican a las funciones mon\u00f3tonas.\n\n  Las funciones mon\u00f3tonas est\u00e1 definida (en Orderings.thy) por\n  \u00b7 mono_def: mono f \u2261 \u2200A B. A \u2264 B \u27f6 f A \u2264 f B \n\n  Las reglas de introducci\u00f3n y eliminaci\u00f3n de la monotonicidad son:\n  . monoI: (\u22c0A B. A \u2264 B \u27f9 f A \u2264 f B) \u27f9 mono f\n  \u00b7 monoD: \u27e6mono f \u27f9 A \u2264 B\u27e7 \u27f9 f A \u2264 f B\n\n  El menor punto fijo de un operador est\u00e1 definido en la teor\u00eda\n  Inductive.thy, para los ret\u00edculos completos, por\n  \u00b7 lfp_def: lfp f = Inf {u. f u \u2264 u}\n\n  El menor punto fijo de una funci\u00f3n mon\u00f3tona es un punto fijo:\n  \u00b7 lfp_unfold: mono f \u27f9 lfp f = f (lfp f)\n\n  La regla de inducci\u00f3n del menor punto fijo es\n  \u00b7 lfp_induct_set: \u27e6 a \u2208 lfp(f);\n                      mono(f); \n                      \u22c0x. \u27e6 x \u2208 f(lfp(f) \u22c2 {x. P(x)}) \u27e7 \u27f9 P(x) \u27e7\n                    \u27f9 P(a)\n*}\n\ntext {*\n  El mayor punto fijo de un operador est\u00e1 definido en la teor\u00eda\n  Inductive.thy, para los ret\u00edculos completos, por\n  \u00b7 gfp_def: gfp f = Sup {u. u \u2264 f u}\n\n  El menor punto fijo de una funci\u00f3n mon\u00f3tona es un punto fijo:\n  \u00b7 gfp_unfold: mono f \u27f9 gfp f = f (gfp f)\n\n  La regla de inducci\u00f3n del menor punto fijo es\n  \u00b7 coinduct_set: \u27e6 mono(f);  \n                    a \u2208 X;  \n                    X \u2286 f(X \u22c3 gfp(f)) \u27e7 \n                  \u27f9 a \u2208 gfp(f)\n*}\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo trabajar en Isabelle\/HOL con conjuntos, funciones y relaciones. La clase se ha basado en la siguiente teor\u00eda Isabelle\/HOL<\/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\/4713"}],"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=4713"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4713\/revisions"}],"predecessor-version":[{"id":4715,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4713\/revisions\/4715"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4713"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4713"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4713"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}