{"id":6478,"date":"2019-02-07T18:48:08","date_gmt":"2019-02-07T17:48:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6478"},"modified":"2019-02-09T09:03:33","modified_gmt":"2019-02-09T08:03:33","slug":"ra2018-conjuntos-funciones-y-relaciones-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2018-conjuntos-funciones-y-relaciones-en-isabelle-hol\/","title":{"rendered":"RA2018: Conjuntos, funciones y relaciones 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-18\">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\">\nchapter {* Tema 12: Conjuntos, funciones y relaciones *}\n\ntheory T12_Conjuntos_funciones_y_relaciones\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_eqI: (\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 equalityD1: A = B \u27f9 A \u2286 B\n  \u00b7 equalityD2: A = B \u27f9 B \u2286 A \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\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}\" \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 de conjuntos finitos:\n  \u00b7 \u2211A es la suma de los elementos del conjunto finito A. Por ejemplo, \n      value \"\u2211{1,2,3}::int\" -- \"= 6\"\n  \u00b7 (setsum f A) es la suma de la aplicaci\u00f3n de f a los elementos del\n    conjunto finito A,  Por ejemplo,\n       value \"setsum (\u03bbx. x*x) {1,2,3}::int\" -- \"= 14\"\n*}\n\ntext {*\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 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}\" \u2015 \u2039= 10\u203a\n\nvalue \"\u2211{2::nat,5,3}\" \u2015 \u2039= 10\u203a\n\ndefinition sumaCuadradosConj :: \"nat set \u21d2 nat\" where\n  \"sumaCuadradosConj S \u2261 \u2211x\u2208S. x*x\"\n\nvalue \"sumaCuadradosConj {2,5,3}\" \u2015 \u2039= 38\u203a\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 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   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\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \"finite S \u27f9 \u2200x\u2208S. x \u2264 sumaConj S\"\nby (induct rule: finite_induct) auto\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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      then have \"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      then have \"y \u2208 F\" using `y \u2208 insert x F` by simp\n      then have \"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\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma \"x \u2209 (Pares \u2229 Impares)\"\nproof \n  fix x assume S: \"x \u2208 (Pares \u2229 Impares)\"\n  then have \"x \u2208 Pares\" by (rule IntD1)\n  then have \"\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  then have \"\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\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma \"x \u2209 (Pares \u2229 Impares)\"\nproof \n  fix x assume S: \"x \u2208 (Pares \u2229 Impares)\"\n  then have \"x \u2208 Pares\" ..\n  then have \"\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  then have \"\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\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \"x \u2209 (Pares \u2229 Impares)\"\nby (auto simp add: Pares_def Impares_def, 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\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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    then have \"f(g(x)) = f(h(x))\" by simp\n    then show \"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\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then show \"g = h\" using `inj f` by (simp add: inj_on_def fun_eq_iff) \nnext\n  assume \"g = h\" \n  then show \"f \u2218 g = f \u2218 h\" by auto\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\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 \n  (\"f`UNIV\"). \n\n  Imagen inversa de un conjunto:\n  \u00b7 vimage_def: f -` B \u2261 {x. f x \u2208 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^-1) = ((b,a) \u2208 r)\n\n  Propiedad de la imagen inversa de una relaci\u00f3n:\n  \u00b7 converse_rel_comp: (r O s)^-1 = s^-1 O r^-1\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\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 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":"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":[322],"tags":[144,323],"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\/6478"}],"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=6478"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6478\/revisions"}],"predecessor-version":[{"id":6479,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6478\/revisions\/6479"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6478"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6478"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6478"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}