Conjuntos, funciones y relaciones - Historial de revisiones

Jalonso en 14:53 29 may 2019

2019-05-29T14:53:19Z

Jalonso en 06:48 9 may 2019

2019-05-09T06:48:59Z

Mostrar los cambios

Jalonso en 11:14 7 feb 2019

2019-02-07T11:14:39Z

Jalonso en 11:10 7 feb 2019

2019-02-07T11:10:56Z

Página nueva

<source lang="isabelle">
chapter {* Tema 10: Conjuntos, funciones y relaciones *}

theory T10_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
</source>

@@ Línea 219: / Línea 219: @@
       (* 1. ∀x∈{}. x ≤ sumaConj {}
 . ⋀x F. ⟦finite F; x ∉ F; ∀x∈F. x ≤ sumaConj F⟧
                   ⟹ ∀xa∈insert x F. xa ≤ sumaConj (insert x F) *)
     apply auto
@@ Línea 246: / Línea 249: @@
        assume "y = x"
        then have "y ≤ x + (sumaConj F)" by simp
-       also have "… = sumaConj (insert x F)" using fF xF by simp
+       also have "… = sumaConj (insert x F)"  by (simp add: fF xF)
        finally show ?thesis .
      next
@@ Línea 337: / Línea 340: @@
    apply (simp add: Pares_def Impares_def)
      (* ⟦∃m. x = 2 * m; ∃m. x = Suc (2 * m)⟧ ⟹ False *)
-   apply arith
+   apply presburger
      (* *)
    done
@@ Línea 343: / Línea 360: @@
 ― ‹Demostración automática›
 lemma "x ∉ (Pares ∩ Impares)"
-   by (auto simp add: Pares_def Impares_def, arith)
+   by (auto simp add: Pares_def Impares_def, presburger)
 ― ‹Demostración declarativa›
@@ Línea 349: / Línea 366: @@
 proof
    fix x assume S: "x ∈ (Pares ∩ Impares)"
-   then have "x ∈ Pares" by (rule IntD1)
+   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" by (rule IntD2)
+   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
+   from p and q show "False" by presburger
 qed
-― ‹2ª demostración declarativa›
+― ‹2ª demostración declarativa sin implícitos ni presburger›
 lemma "x ∉ (Pares ∩ Impares)"
 proof
    fix x assume S: "x ∈ (Pares ∩ Impares)"
-   then have "x ∈ Pares" ..
+   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" ..
+   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
+   from p and q show "False" by (simp add: Suc_double_not_eq_double)
 qed
@@ Línea 494: / Línea 511: @@
    "inj f ⟹ (f ∘ g = f ∘ h) = (g = h)"
    apply (simp add: inj_on_def fun_eq_iff)
    apply auto
    done
@@ Línea 501: / Línea 544: @@
    assumes "inj f"
    shows "(f ∘ g = f ∘ h) = (g = h)"
-using assms
+  using assms
-by (auto simp add: inj_on_def fun_eq_iff)
+  by (auto simp add: inj_on_def fun_eq_iff)
 ― ‹Demostración declarativa›
@@ Línea 538: / Línea 581: @@
 next
    assume "g = h"
-   then show "f ∘ g = f ∘ h" by auto
+   then show "f ∘ g = f ∘ h" by simp
 qed

← Revisión anterior	Revisión del 11:14 7 feb 2019
(Sin diferencias)