En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo trabajar en Isabelle/HOL con conjuntos, funciones y relaciones.
La clase se ha basado en la siguiente teoría Isabelle/HOL
chapter {* Tema 12: Conjuntos, funciones y relaciones *} theory T12_Conjuntos_funciones_y_relaciones imports Main begin section {* Conjuntos *} subsection {* Operaciones con conjuntos *} text {* Nota. La teoría elemental de conjuntos es HOL/Set.thy. Nota. En un conjunto todos los elemento son del mismo tipo (por ejemplo, del tipo τ) y el conjunto tiene tipo (en el ejemplo, "τ set"). Reglas de la intersección: · IntI: ⟦c ∈ A; c ∈ B⟧ ⟹ c ∈ A ∩ B · IntD1: c ∈ A ∩ B ⟹ c ∈ A · IntD2: c ∈ A ∩ B ⟹ c ∈ B Nota. Propiedades del complementario: · Compl_iff: (c ∈ - A) = (c ∉ A) · Compl_Un: - (A ∪ B) = - A ∩ - B Nota. El conjunto vacío se representa por {} y el universal por UNIV. Nota. Propiedades de la diferencia y del complementario: · Diff_disjoint: A ∩ (B - A) = {} · Compl_partition: A ∪ - A = UNIV Nota. Reglas de la relación de subconjunto: · subsetI: (⋀x. x ∈ A ⟹ x ∈ B) ⟹ A ⊆ B · subsetD: ⟦A ⊆ B; c ∈ A⟧ ⟹ c ∈ B *} text {* Ejemplo: A ∪ B ⊆ C syss A ⊆ C ∧ B ⊆ C. *} lemma "(A ∪ B ⊆ C) = (A ⊆ C ∧ B ⊆ C)" by blast text {* Ejemplo: A ⊆ -B syss B ⊆ -A. *} lemma "(A ⊆ -B) = (B ⊆ -A)" by blast text {* Principio de extensionalidad de conjuntos: · set_eqI: (⋀x. (x ∈ A) = (x ∈ B)) ⟹ A = B Reglas de la igualdad de conjuntos: · equalityI: ⟦A ⊆ B; B ⊆ A⟧ ⟹ A = B · equalityD1: A = B ⟹ A ⊆ B · equalityD2: A = B ⟹ B ⊆ A · equalityE: ⟦A = B; ⟦A ⊆ B; B ⊆ A⟧ ⟹ P⟧ ⟹ P *} text {* Lema. [Analogía entre intersección y conjunción] "x ∈ A ∩ B" syss "x ∈ A" y "x ∈ B". *} lemma "(x ∈ A ∩ B) = (x ∈ A ∧ x ∈ B)" by simp text {* Lema. [Analogía entre unión y disyunción] x ∈ A ∪ B syss x ∈ A ó x ∈ B. *} lemma "(x ∈ A ∪ B) = (x ∈ A ∨ x ∈ B)" by simp text {* Lema. [Analogía entre subconjunto e implicación] A ⊆ B syss para todo x, si x ∈ A entonces x ∈ B. *} lemma "(A ⊆ B) = (∀ x. x ∈ A ⟶ x ∈ B)" by auto text {* Lema. [Analogía entre complementario y negación] x pertenece al complementario de A syss x no pertenece a A. *} lemma "(x ∈ -A) = (x ∉ A)" by simp subsection {* Notación de conjuntos finitos *} text {* Nota. La teoría de conjuntos finitos es HOL/Finite_Set.thy. Nota. Los conjuntos finitos se definen por inducción a partir de las siguientes reglas inductivas: · El conjunto vacío es un conjunto finito. · emptyI: "finite {}" · Si se le añade un elemento a un conjunto finito se obtiene otro conjunto finito. · insertI: "finite A ⟹ finite (insert a A)" A continuación se muestran ejemplos de conjuntos finitos. *} lemma "insert 2 {} = {2} ∧ insert 3 {2} = {2,3} ∧ insert 2 {2,3} = {2,3} ∧ {2,3} = {3,2,3,2,2}" by auto text {* Nota. Los conjuntos finitos se representan con la notación conjuntista habitual: los elementos entre llaves y separados por comas. *} text {* Ejemplo: {a,b} ∪ {c,d} = {a,b,c,d} *} lemma "{a,b} ∪ {c,d} = {a,b,c,d}" by blast text {* Ejemplo de conjetura falsa y su refutación. *} lemma "{a,b} ∩ {b,c} = {b}" oops text {* Ejemplo con la conjetura corregida. *} lemma "{a,b} ∩ {b,c} = (if a = c then {a,b} else {b})" by auto text {* Sumas de conjuntos finitos: · ∑A es la suma de los elementos del conjunto finito A. Por ejemplo, value "∑{1,2,3}::int" -- "= 6" · (setsum f A) es la suma de la aplicación de f a los elementos del conjunto finito A, Por ejemplo, value "setsum (λx. x*x) {1,2,3}::int" -- "= 14" *} text {* Ejemplos de definiciones recursivas sobre conjuntos finitos: Sea A un conjunto finito de números naturales. · sumaConj A es la suma de los elementos A. · sumaCuadradosConj A es la suma de los cuadrados de los elementos A. *} definition sumaConj :: "nat set ⇒ nat" where "sumaConj S ≡ ∑S" value "sumaConj {2,5,3}" ― ‹= 10› value "∑{2::nat,5,3}" ― ‹= 10› definition sumaCuadradosConj :: "nat set ⇒ nat" where "sumaCuadradosConj S ≡ ∑x∈S. x*x" value "sumaCuadradosConj {2,5,3}" ― ‹= 38› text {* Nota. Para simplificar lo que sigue, declaramos las anteriores definiciones como reglas de simplificación. *} declare sumaConj_def [simp] declare sumaCuadradosConj_def [simp] text {* Ejemplos de evaluación de las anteriores definiciones recursivas. *} lemma "sumaConj {1,2,3,4} = 10 ∧ sumaCuadradosConj {1,2,3,4} = 30" by simp text {* Inducción sobre conjuntos finitos: Para demostrar que todos los conjuntos finitos tienen una propiedad P basta probar que · El conjunto vacío tiene la propiedad P. · Si a un conjunto finito que tiene la propiedad P se le añade un nuevo elemento, el conjunto obtenido sigue teniendo la propiedad P. En forma de regla · finite_induct: ⟦finite F; P {}; ⋀x F. ⟦finite F; x ∉ F; P F⟧ ⟹ P ({x} ∪ F)⟧ ⟹ P F *} text {* Ejemplo de inducción sobre conjuntos finitos: Sea S un conjunto finito de números naturales. Entonces todos los elementos de S son menores o iguales que la suma de los elementos de S. *} ― ‹La demostración automática es› lemma "finite S ⟹ ∀x∈S. x ≤ sumaConj S" by (induct rule: finite_induct) auto ― ‹La demostración estructurada es› lemma sumaConj_acota: "finite S ⟹ ∀x∈S. x ≤ sumaConj S" proof (induct rule: finite_induct) show "∀x ∈ {}. x ≤ sumaConj {}" by simp next fix x and F assume fF: "finite F" and xF: "x ∉ F" and HI: "∀ x∈F. x ≤ sumaConj F" show "∀y ∈ insert x F. y ≤ sumaConj (insert x F)" proof fix y assume "y ∈ insert x F" show "y ≤ sumaConj (insert x F)" proof (cases "y = x") assume "y = x" then have "y ≤ x + (sumaConj F)" by simp also have "… = sumaConj (insert x F)" using fF xF by simp finally show ?thesis . next assume "y ≠ x" then have "y ∈ F" using `y ∈ insert x F` by simp then have "y ≤ sumaConj F" using HI by blast also have "… ≤ x + (sumaConj F)" by simp also have "… = sumaConj (insert x F)" using fF xF by simp finally show ?thesis . qed qed qed subsection {* Definiciones por comprensión *} text {* El conjunto de los elementos que cumple la propiedad P se representa por {x. P}. Reglas de comprensión (relación entre colección y pertenencia): · mem_Collect_eq: (a ∈ {x. P x}) = P a · Collect_mem_eq: {x. x ∈ A} = A *} text {* Ejemplo de comprensión: {x. P x ∨ x ∈ A} = {x. P x} ∪ A *} lemma "{x. P x ∨ x ∈ A} = {x. P x} ∪ A" by blast text {* Ejemplo de comprensión: {x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x} *} lemma "{x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x}" by blast text {* Ejemplo con la sintaxis general de comprensión. {p*q | p q. p ∈ prime ∧ q ∈ prime} = {z. ∃p q. z = p*q ∧ p ∈ prime ∧ q ∈ prime} *} lemma "{p*q | p q. p ∈ prime ∧ q ∈ prime} = {z. ∃p q. z = p*q ∧ p ∈ prime ∧ q ∈ prime}" by blast text {* En HOL, la notación conjuntista es azúcar sintáctica: · x ∈ A es equivalente a A(x). · {x. P} es equivalente a λx. P. *} text {* Ejemplo de definición por comprensión: El conjunto de los pares es el de los números n para los que existe un m tal que n = 2*m. *} definition Pares :: "nat set" where "Pares ≡ {n. ∃m. n = 2*m }" text {* Ejemplo. Los números 2 y 34 son pares. *} lemma "2 ∈ Pares ∧ 34 ∈ Pares" by (simp add: Pares_def) text {* Definición. El conjunto de los impares es el de los números n para los que existe un m tal que n = 2*m + 1. *} definition Impares :: "nat set" where "Impares ≡ {n. ∃m. n = 2*m + 1}" text {* Ejemplo con las reglas de intersección y comprensión: El conjunto de los pares es disjunto con el de los impares. *} ― ‹La demostración detallada es› lemma "x ∉ (Pares ∩ Impares)" proof fix x assume S: "x ∈ (Pares ∩ Impares)" then have "x ∈ Pares" by (rule IntD1) then have "∃m. x = 2 * m" by (simp only: Pares_def mem_Collect_eq) then obtain p where p: "x = 2 * p" .. from S have "x ∈ Impares" by (rule IntD2) then have "∃ m. x = 2 * m + 1" by (simp only: Impares_def mem_Collect_eq) then obtain q where q: "x = 2 * q + 1" .. from p and q show "False" by arith qed ― ‹La demostración estructurada es› lemma "x ∉ (Pares ∩ Impares)" proof fix x assume S: "x ∈ (Pares ∩ Impares)" then have "x ∈ Pares" .. then have "∃m. x = 2 * m" by (simp only: Pares_def mem_Collect_eq) then obtain p where p: "x = 2 * p" .. from S have "x ∈ Impares" .. then have "∃ m. x = 2 * m + 1" by (simp only: Impares_def mem_Collect_eq) then obtain q where q: "x = 2 * q + 1" .. from p and q show "False" by arith qed ― ‹La demostración automática es› lemma "x ∉ (Pares ∩ Impares)" by (auto simp add: Pares_def Impares_def, arith) subsection {* Cuantificadores acotados *} text {* Reglas de cuantificador universal acotado ("bounded"): · ballI: (⋀x. x ∈ A ⟹ P x) ⟹ ∀x∈A. P x · bspec: ⟦∀x∈A. P x; x ∈ A⟧ ⟹ P x Reglas de cuantificador existencial acotado ("bounded"): · bexI: ⟦P x; x ∈ A⟧ ⟹ ∃x∈A. P x · bexE: ⟦∃x∈A. P x; ⋀x. ⟦x ∈ A; P x⟧ ⟹ Q⟧ ⟹ Q Reglas de la unión indexada: · UN_iff: (b ∈ (⋃x∈A. B x)) = (∃x∈A. b ∈ B x) · UN_I: ⟦a ∈ A; b ∈ B a⟧ ⟹ b ∈ (⋃x∈A. B x) · UN_E: ⟦b ∈ (⋃x∈A. B x); ⋀x. ⟦x ∈ A; b ∈ B x⟧ ⟹ R⟧ ⟹ R Reglas de la unión de una familia: · Union_def: ⋃S = (⋃x∈S. x) · Union_iff: (A ∈ ⋃C) = (∃X∈C. A ∈ X) Reglas de la intersección indexada: · INT_iff: (b ∈ (⋂x∈A. B x)) = (∀x∈A. b ∈ B x) · INT_I: (⋀x. x ∈ A ⟹ b ∈ B x) ⟹ b ∈ (⋂x∈A. B x) · INT_E: ⟦b ∈ (⋂x∈A. B x); b ∈ B a ⟹ R; a ∉ A ⟹ R⟧ ⟹ R Reglas de la intersección de una familia: · Inter_def: ⋂S = (⋂x∈S. x) · Inter_iff: (A ∈ ⋂C) = (∀X∈C. A ∈ X) Abreviaturas: · "Collect P" es lo mismo que "{x. P}". · "All P" es lo mismo que "∀x. P x". · "Ex P" es lo mismo que "∃x. P x". · "Ball A P" es lo mismo que "∀x∈A. P x". · "Bex A P" es lo mismo que "∃x∈A. P x". *} subsection {* Conjuntos finitos y cardinalidad *} text {* El número de elementos de un conjunto finito A es el cardinal de A y se representa por "card A". *} text {* Ejemplos de cardinales de conjuntos finitos. *} lemma "card {} = 0 ∧ card {4} = 1 ∧ card {4,1} = 2 ∧ x ≠ y ⟹ card {x,y} = 2" by simp text {* Propiedades de cardinales: · Cardinal de la unión de conjuntos finitos: card_Un_Int: ⟦finite A; finite B⟧ ⟹ card A + card B = card (A ∪ B) + card (A ∩ B)" · Cardinal del conjunto potencia: card_Pow: finite A ⟹ card (Pow A) = 2 ^ card A *} section {* Funciones *} text {* La teoría de funciones es HOL/Fun.thy. *} subsection {* Nociones básicas de funciones *} text {* Principio de extensionalidad para funciones: · ext: (⋀x. f x = g x) ⟹ f = g Actualización de funciones · fun_upd_apply: (f(x := y)) z = (if z = x then y else f z) · fun_upd_upd: f(x := y, x := z) = f(x := z) Función identidad · id_def: id ≡ λx. x Composición de funciones: · o_def: f ∘ g = (λx. f (g x)) Asociatividad de la composición: · o_assoc: f ∘ (g ∘ h) = (f ∘ g) ∘ h *} subsection {* Funciones inyectivas, suprayectivas y biyectivas *} text {* Función inyectiva sobre A: · inj_on_def: inj_on f A ≡ ∀x∈A. ∀y∈A. f x = f y ⟶ x = y Nota. "inj f" es una abreviatura de "inj_on f UNIV". Función suprayectiva: · surj_def: surj f ≡ ∀y. ∃x. y = f x Función biyectiva: · bij_def: bij f ≡ inj f ∧ surj f Propiedades de las funciones inversas: · inv_f_f: inj f ⟹ inv f (f x) = x · surj_f_inv_f: surj f ⟹ f (inv f y) = y · inv_inv_eq: bij f ⟹ inv (inv f) = f Igualdad de funciones (por extensionalidad): · fun_eq_iff: (f = g) = (∀x. f x = g x) *} text {* Ejemplo de lema de demostración de propiedades de funciones: Una función inyectiva puede cancelarse en el lado izquierdo de la composición de funciones. *} ― ‹La demostración detallada es› lemma assumes "inj f" shows "(f ∘ g = f ∘ h) = (g = h)" proof assume "f ∘ g = f ∘ h" show "g = h" proof fix x have "(f ∘ g)(x) = (f ∘ h)(x)" using `f ∘ g = f ∘ h` by simp then have "f(g(x)) = f(h(x))" by simp then show "g(x) = h(x)" using `inj f` by (simp add:inj_on_def) qed next assume "g = h" show "f ∘ g = f ∘ h" proof fix x have "(f ∘ g) x = f(g(x))" by simp also have "… = f(h(x))" using `g = h` by simp also have "… = (f ∘ h) x" by simp finally show "(f ∘ g) x = (f ∘ h) x" by simp qed qed ― ‹La demostración estructurada es› lemma assumes "inj f" shows "(f ∘ g = f ∘ h) = (g = h)" proof assume "f ∘ g = f ∘ h" then show "g = h" using `inj f` by (simp add: inj_on_def fun_eq_iff) next assume "g = h" then show "f ∘ g = f ∘ h" by auto qed ― ‹La demostración automática es› lemma assumes "inj f" shows "(f ∘ g = f ∘ h) = (g = h)" using assms by (auto simp add: inj_on_def fun_eq_iff) subsubsection {* Función imagen *} text {* Imagen de un conjunto mediante una función: · image_def: f ` A = {y. (∃x∈A. y = f x)} Propiedades de la imagen: · image_compose: (f ∘ g)`r = f`g`r · image_Un: f`(A ∪ B) = f`A ∪ f`B · image_Int: inj f ⟹ f`(A ∩ B) = f`A ∩ f`B" *} text {* Ejemplo de demostración de propiedades de la imagen: f`A ∪ g`A = (⋃x∈A. {f x, g x}) *} lemma "f`A ∪ g`A = (⋃x∈A. {f x, g x})" by auto text {* Ejemplo de demostración de propiedades de la imagen: f`{(x,y). P x y} = {f(x,y) | x y. P x y} *} lemma "f`{(x,y). P x y} = {f(x,y) | x y. P x y}" by auto text {* El rango de una función ("range f") es la imagen del universo ("f`UNIV"). Imagen inversa de un conjunto: · vimage_def: f -` B ≡ {x. f x ∈ B} Propiedad de la imagen inversa de un conjunto: · vimage_Compl: f -` (-A) = -(f -` A) *} section {* Relaciones *} subsection {* Relaciones básicas *} text {* La teoría de relaciones es HOL/Relation.thy. Las relaciones son conjuntos de pares. Relación identidad: · Id_def: Id ≡ {p. ∃x. p = (x,x)} Composición de relaciones: · rel_comp_def: r O s ≡ {(x,z). ∃y. (x, y) ∈ r ∧ (y, z) ∈ s} Propiedades: · R_O_Id: R O Id = R · rel_comp_mono: ⟦r' ⊆ r; s' ⊆ s⟧ ⟹ (r' O s') ⊆ (r O s) Imagen inversa de una relación: · converse_iff: ((a,b) ∈ r^-1) = ((b,a) ∈ r) Propiedad de la imagen inversa de una relación: · converse_rel_comp: (r O s)^-1 = s^-1 O r^-1 Imagen de un conjunto mediante una relación: · Image_iff: (b ∈ r``A) = (∃x:A. (x, b) ∈ r) Dominio de una relación: · Domain_iff: (a ∈ Domain r) = (∃y. (a, y) ∈ r) Rango de una relación: · Range_iff: (a ∈ Range r) = (∃y. (y,a) ∈ r) *} end |