Diferencia entre revisiones de «Tema 12: Conjuntos, funciones y relaciones»
De Demostración asistida por ordenador (2011-12)
(Página creada con '<source lang="isar"> header {* Tema 12: Conjuntos, funciones y relaciones *} theory Tema_12 imports Main begin section {* Conjuntos *} subsection {* Operaciones con conjunto...') |
|||
Línea 14: | Línea 14: | ||
Nota. En un conjunto todos los elemento son del mismo tipo (por | Nota. En un conjunto todos los elemento son del mismo tipo (por | ||
− | ejemplo, del tipo | + | ejemplo, del tipo τ) y el conjunto tiene tipo (en el ejemplo, "τ set"). |
Reglas de la intersección: | Reglas de la intersección: | ||
− | · IntI: | + | · IntI: ⟦c ∈ A; c ∈ B⟧ ⟹ c ∈ A ∩ B |
− | · IntD1: c | + | · IntD1: c ∈ A ∩ B ⟹ c ∈ A |
− | · IntD2: c | + | · IntD2: c ∈ A ∩ B ⟹ c ∈ B |
Nota. Propiedades del complementario: | Nota. Propiedades del complementario: | ||
− | · Compl_iff: (c | + | · Compl_iff: (c ∈ - A) = (c ∉ A) |
− | · Compl_Un: - (A | + | · Compl_Un: - (A ∪ B) = - A ∩ - B |
Nota. El conjunto vacío se representa por {} y el universal por UNIV. | Nota. El conjunto vacío se representa por {} y el universal por UNIV. | ||
Nota. Propiedades de la \textbf{diferencia} y del complementario: | Nota. Propiedades de la \textbf{diferencia} y del complementario: | ||
− | · Diff_disjoint: A | + | · Diff_disjoint: A ∩ (B - A) = {} |
− | · Compl_partition: A | + | · Compl_partition: A ∪ - A = UNIV |
Nota. Reglas de la relación de \textbf{subconjunto}: | Nota. Reglas de la relación de \textbf{subconjunto}: | ||
− | · subsetI: ( | + | · subsetI: (⋀x. x ∈ A ⟹ x ∈ B) ⟹ A ⊆ B |
− | · subsetD: | + | · subsetD: ⟦A ⊆ B; c ∈ A⟧ ⟹ c ∈ B |
Nota. Ejemplo trivial. | Nota. Ejemplo trivial. | ||
*} | *} | ||
− | lemma "(A | + | lemma "(A ∪ B ⊆ C) = (A ⊆ C ∧ B ⊆ C)" |
by blast | by blast | ||
Línea 45: | Línea 45: | ||
*} | *} | ||
− | lemma "(A | + | lemma "(A ⊆ -B) = (B ⊆ -A)" |
by blast | by blast | ||
text {* | text {* | ||
Principio de extensionalidad de conjuntos: | Principio de extensionalidad de conjuntos: | ||
− | · set_ext: ( | + | · set_ext: (⋀x. (x ∈ A) = (x ∈ B)) ⟹ A = B |
Reglas de la igualdad de conjuntos: | Reglas de la igualdad de conjuntos: | ||
− | · equalityI: | + | · equalityI: ⟦A ⊆ B; B ⊆ A⟧ ⟹ A = B |
− | · equalityE: | + | · equalityE: ⟦A = B; ⟦A ⊆ B; B ⊆ A⟧ ⟹ P⟧ ⟹ P |
Lema. [Analogía entre intersección y conjunción] | Lema. [Analogía entre intersección y conjunción] | ||
− | "x | + | "x ∈ A ∩ B" syss "x ∈ A" y "x ∈ B". |
*} | *} | ||
− | lemma "(x | + | lemma "(x ∈ A ∩ B) = (x ∈ A ∧ x ∈ B)" |
by simp | by simp | ||
text {* | text {* | ||
Lema. [Analogía entre unión y disyunción] | Lema. [Analogía entre unión y disyunción] | ||
− | "x | + | "x ∈ A ∪ B" syss "x ∈ A" ó "x ∈ B". |
*} | *} | ||
− | lemma "(x | + | lemma "(x ∈ A ∪ B) = (x ∈ A ∨ x ∈ B)" |
by simp | by simp | ||
text {* | text {* | ||
Lema. [Analogía entre subconjunto e implicación] | Lema. [Analogía entre subconjunto e implicación] | ||
− | "(A | + | "(A ⊆ B)" syss para todo "x", si "x ∈ A" entonces "x ∈ B". |
*} | *} | ||
− | lemma "(A | + | lemma "(A ⊆ B) = (∀ x. x ∈ A ⟶ x ∈ B)" |
by auto | by auto | ||
Línea 84: | Línea 84: | ||
*} | *} | ||
− | lemma "(x | + | lemma "(x ∈ -A) = (x ∉ A)" |
by simp | by simp | ||
Línea 98: | Línea 98: | ||
· Si se le añade un elemento a un conjunto finito se obtiene otro | · Si se le añade un elemento a un conjunto finito se obtiene otro | ||
conjunto finito. | conjunto finito. | ||
− | · insertI: "finite A | + | · insertI: "finite A ⟹ finite (insert a A)" |
A continuación se muestran ejemplos de conjuntos finitos. | A continuación se muestran ejemplos de conjuntos finitos. | ||
Línea 104: | Línea 104: | ||
lemma | lemma | ||
− | "insert 2 {} = {2} | + | "insert 2 {} = {2} ∧ |
− | insert 3 {2} = {2,3} | + | insert 3 {2} = {2,3} ∧ |
− | insert 2 {2,3} = {2,3} | + | insert 2 {2,3} = {2,3} ∧ |
{2,3} = {3,2,3,2,2}" | {2,3} = {3,2,3,2,2}" | ||
by auto | by auto | ||
Línea 117: | Línea 117: | ||
*} | *} | ||
− | lemma "{a,b} | + | lemma "{a,b} ∪ {c,d} = {a,b,c,d}" |
by blast | by blast | ||
Línea 124: | Línea 124: | ||
*} | *} | ||
− | lemma "{a,b} | + | lemma "{a,b} ∩ {b,c} = {b}" |
refute | refute | ||
oops | oops | ||
Línea 132: | Línea 132: | ||
*} | *} | ||
− | lemma "{a,b} | + | lemma "{a,b} ∩ {b,c} = (if a=c then {a,b} else {b})" |
by auto | by auto | ||
Línea 141: | Línea 141: | ||
· (setprod f A) es producto de la aplicación de f a los elementos del | · (setprod f A) es producto de la aplicación de f a los elementos del | ||
conjunto finito A, | conjunto finito A, | ||
− | · | + | · ∑A es la suma de los elementos del conjunto finito A, |
− | · | + | · ∏A es el producto de los elementos del conjunto finito A. |
Ejemplos de definiciones recursivas sobre conjuntos finitos: | Ejemplos de definiciones recursivas sobre conjuntos finitos: | ||
Línea 151: | Línea 151: | ||
*} | *} | ||
− | definition sumaConj :: "nat set | + | definition sumaConj :: "nat set ⇒ nat" where |
− | "sumaConj S | + | "sumaConj S ≡ ∑S" |
− | definition productoConj :: "nat set | + | definition productoConj :: "nat set ⇒ nat" where |
− | "productoConj S | + | "productoConj S ≡ ∏S" |
− | definition sumaCuadradosConj :: "nat set | + | definition sumaCuadradosConj :: "nat set ⇒ nat" where |
− | "sumaCuadradosConj S | + | "sumaCuadradosConj S ≡ setsum (λx. x*x) S" |
text {* | text {* | ||
Línea 174: | Línea 174: | ||
lemma | lemma | ||
− | "sumaConj {1,2,3,4} = 10 | + | "sumaConj {1,2,3,4} = 10 ∧ |
− | productoConj {1,2,3} = productoConj {3,2} | + | productoConj {1,2,3} = productoConj {3,2} ∧ |
sumaCuadradosConj {1,2,3,4} = 30" | sumaCuadradosConj {1,2,3,4} = 30" | ||
by simp | by simp | ||
Línea 186: | Línea 186: | ||
elemento, el conjunto obtenido sigue teniendo la propiedad P. | elemento, el conjunto obtenido sigue teniendo la propiedad P. | ||
En forma de regla | En forma de regla | ||
− | · finite_induct: | + | · finite_induct: ⟦finite F; |
P {}; | P {}; | ||
− | + | ⋀x F. ⟦finite F; x ∉ F; P F⟧ ⟹ P ({x} ∪ F)⟧ | |
− | + | ⟹ P F | |
Lema. [Ejemplo de inducción sobre conjuntos finitos] | Lema. [Ejemplo de inducción sobre conjuntos finitos] | ||
Línea 198: | Línea 198: | ||
*} | *} | ||
− | lemma "finite S | + | lemma "finite S ⟹ ∀x∈S. x ≤ sumaConj S" |
by (induct rule: finite_induct) auto | by (induct rule: finite_induct) auto | ||
Línea 205: | Línea 205: | ||
*} | *} | ||
− | lemma sumaConj_acota: "finite S | + | lemma sumaConj_acota: "finite S ⟹ ∀x∈S. x ≤ sumaConj S" |
proof (induct rule: finite_induct) | proof (induct rule: finite_induct) | ||
− | show " | + | show "∀x∈{}. x ≤ sumaConj {}" by simp |
next | next | ||
fix x and F | fix x and F | ||
assume fF: "finite F" | assume fF: "finite F" | ||
− | and xF: "x | + | and xF: "x ∉ F" |
− | and HI: " | + | and HI: "∀ x∈F. x ≤ sumaConj F" |
− | show " | + | show "∀y∈insert x F. y ≤ sumaConj (insert x F)" |
proof | proof | ||
fix y | fix y | ||
− | assume "y | + | assume "y ∈ insert x F" |
− | show "y | + | show "y ≤ sumaConj (insert x F)" |
proof (cases "y = x") | proof (cases "y = x") | ||
assume "y = x" | assume "y = x" | ||
− | hence "y | + | hence "y ≤ x + (sumaConj F)" by simp |
− | also have " | + | also have "… = sumaConj (insert x F)" using fF xF by simp |
finally show ?thesis . | finally show ?thesis . | ||
next | next | ||
− | assume "y | + | assume "y ≠ x" |
− | hence "y | + | hence "y ∈ F" using `y ∈ insert x F` by simp |
− | hence "y | + | hence "y ≤ sumaConj F" using HI by blast |
− | also have " | + | also have "… ≤ x + (sumaConj F)" by simp |
− | also have " | + | also have "… = sumaConj (insert x F)" using fF xF by simp |
finally show ?thesis . | finally show ?thesis . | ||
qed | qed | ||
Línea 241: | Línea 241: | ||
Reglas de comprensión (relación entre colección y pertenencia): | Reglas de comprensión (relación entre colección y pertenencia): | ||
− | · mem_Collect_eq: (a | + | · mem_Collect_eq: (a ∈ {x. P x}) = P a |
− | · Collect_mem_eq: {x. x | + | · Collect_mem_eq: {x. x ∈ A} = A |
Dos lemas triviales. | Dos lemas triviales. | ||
*} | *} | ||
− | lemma "{x. P x | + | lemma "{x. P x ∨ x ∈ A} = {x. P x} ∪ A" |
by blast | by blast | ||
− | lemma "{x. P x | + | lemma "{x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x}" |
by blast | by blast | ||
Línea 258: | Línea 258: | ||
lemma | lemma | ||
− | "{p*q | p q. p | + | "{p*q | p q. p ∈ prime ∧ q ∈ prime} = |
− | {z. | + | {z. ∃p q. z = p*q ∧ p ∈ prime ∧ q ∈ prime}" |
by blast | by blast | ||
text {* | text {* | ||
En HOL, la notación conjuntista es azúcar sintáctica: | En HOL, la notación conjuntista es azúcar sintáctica: | ||
− | · x | + | · x ∈ A es equivalente a A(x). |
− | · {x. P} es equivalente a | + | · {x. P} es equivalente a λx. P. |
*} | *} | ||
Línea 275: | Línea 275: | ||
definition Pares :: "nat set" where | definition Pares :: "nat set" where | ||
− | "Pares | + | "Pares ≡ {n. ∃ m. n = 2*m }" |
text {* | text {* | ||
Línea 282: | Línea 282: | ||
lemma | lemma | ||
− | "2 | + | "2 ∈ Pares ∧ |
− | 34 | + | 34 ∈ Pares" |
by (simp add: Pares_def) | by (simp add: Pares_def) | ||
Línea 292: | Línea 292: | ||
definition Impares :: "nat set" where | definition Impares :: "nat set" where | ||
− | "Impares | + | "Impares ≡ {n. ∃ m. n = 2*m + 1 }" |
text {* | text {* | ||
Línea 299: | Línea 299: | ||
*} | *} | ||
− | lemma "x | + | lemma "x ∉ (Pares ∩ Impares)" |
proof | proof | ||
− | fix x assume S: "x | + | fix x assume S: "x ∈ (Pares ∩ Impares)" |
− | hence "x | + | hence "x ∈ Pares" by (rule IntD1) |
− | hence " | + | hence "∃ m. x = 2 * m" by (simp only: Pares_def mem_Collect_eq) |
then obtain p where p: "x = 2 * p" .. | then obtain p where p: "x = 2 * p" .. | ||
− | from S have "x | + | from S have "x ∈ Impares" by (rule IntD2) |
− | hence " | + | hence "∃ m. x = 2 * m + 1" by (simp only: Impares_def mem_Collect_eq) |
then obtain q where q: "x = 2 * q + 1" .. | then obtain q where q: "x = 2 * q + 1" .. | ||
Línea 317: | Línea 317: | ||
text {* | text {* | ||
Reglas de cuantificador universal acotado ("bounded"): | Reglas de cuantificador universal acotado ("bounded"): | ||
− | · ballI: ( | + | · ballI: (⋀x. x ∈ A ⟹ P x) ⟹ ∀x∈A. P x |
− | · bspec: | + | · bspec: ⟦∀x∈A. P x; x ∈ A⟧ ⟹ P x |
Reglas de cuantificador existencial acotado ("bounded"): | Reglas de cuantificador existencial acotado ("bounded"): | ||
− | · bexI: | + | · bexI: ⟦P x; x ∈ A⟧ ⟹ ∃x∈A. P x |
− | · bexE: | + | · bexE: ⟦∃x∈A. P x; ⋀x. ⟦x ∈ A; P x⟧ ⟹ Q⟧ ⟹ Q |
Reglas de la unión indexada: | Reglas de la unión indexada: | ||
− | · UN_iff: (b | + | · UN_iff: (b ∈ (⋃x∈A. B x)) = (∃x∈A. b ∈ B x) |
− | · UN_I: | + | · UN_I: ⟦a ∈ A; b ∈ B a⟧ ⟹ b ∈ (⋃x∈A. B x) |
− | · UN_E: | + | · UN_E: ⟦b ∈ (⋃x∈A. B x); ⋀x. ⟦x ∈ A; b ∈ B x⟧ ⟹ R⟧ ⟹ R |
Reglas de la unión de una familia: | Reglas de la unión de una familia: | ||
− | · Union_def: | + | · Union_def: ⋃S = (⋃x∈S. x) |
− | · Union_iff: (A | + | · Union_iff: (A ∈ ⋃C) = (∃X∈C. A ∈ X) |
Reglas de la intersección indexada: | Reglas de la intersección indexada: | ||
− | · INT_iff: (b | + | · INT_iff: (b ∈ (⋂x∈A. B x)) = (∀x∈A. b ∈ B x) |
− | · INT_I: ( | + | · INT_I: (⋀x. x ∈ A ⟹ b ∈ B x) ⟹ b ∈ (⋂x∈A. B x) |
− | · INT_E: | + | · INT_E: ⟦b ∈ (⋂x∈A. B x); b ∈ B a ⟹ R; a ∉ A ⟹ R⟧ ⟹ R |
Reglas de la intersección de una familia: | Reglas de la intersección de una familia: | ||
− | · Inter_def: | + | · Inter_def: ⋂S = (⋂x∈S. x) |
− | · Inter_iff: (A | + | · Inter_iff: (A ∈ ⋂C) = (∀X∈C. A ∈ X) |
Abreviaturas: | Abreviaturas: | ||
· "Collect P" es lo mismo que "{x. P}". | · "Collect P" es lo mismo que "{x. P}". | ||
− | · "All P" es lo mismo que " | + | · "All P" es lo mismo que "∀x. P x". |
− | · "Ex P" es lo mismo que " | + | · "Ex P" es lo mismo que "∃x. P x". |
− | · "Ball P" es lo mismo que " | + | · "Ball P" es lo mismo que "∀x∈A. P x". |
− | · "Bex P" es lo mismo que " | + | · "Bex P" es lo mismo que "∃x∈A. P x". |
*} | *} | ||
Línea 360: | Línea 360: | ||
lemma | lemma | ||
− | "card {} = 0 | + | "card {} = 0 ∧ |
− | card {4} = 1 | + | card {4} = 1 ∧ |
− | card {4,1} = 2 | + | card {4,1} = 2 ∧ |
− | x | + | x ≠ y ⟹ card {x,y} = 2" |
by simp | by simp | ||
Línea 369: | Línea 369: | ||
Propiedades de cardinales: | Propiedades de cardinales: | ||
· Cardinal de la unión de conjuntos finitos: | · Cardinal de la unión de conjuntos finitos: | ||
− | card_Un_Int: | + | card_Un_Int: ⟦finite A; finite B⟧ |
− | + | ⟹ card A + card B = card (A ∪ B) + card (A ∩ B)" | |
· Cardinal del conjunto potencia: | · Cardinal del conjunto potencia: | ||
− | card_Pow: finite A | + | card_Pow: finite A ⟹ card (Pow A) = 2 ^ card A |
*} | *} | ||
Línea 385: | Línea 385: | ||
text {* | text {* | ||
Principio de extensionalidad para funciones: | Principio de extensionalidad para funciones: | ||
− | · ext: ( | + | · ext: (⋀x. f x = g x) ⟹ f = g |
Actualización de funciones | Actualización de funciones | ||
Línea 392: | Línea 392: | ||
Función identidad | Función identidad | ||
− | · id_def: id | + | · id_def: id ≡ λx. x |
Composición de funciones: | Composición de funciones: | ||
− | · o_def: f | + | · o_def: f ∘ g = (λx. f (g x)) |
Asociatividad de la composición: | Asociatividad de la composición: | ||
− | · o_assoc: f | + | · o_assoc: f ∘ (g ∘ h) = (f ∘ g) ∘ h |
*} | *} | ||
Línea 405: | Línea 405: | ||
text {* | text {* | ||
Función inyectiva sobre A: | Función inyectiva sobre A: | ||
− | · inj_on_def: inj_on f 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". | Nota. "inj f" es una abreviatura de "inj_on f UNIV". | ||
Función suprayectiva: | Función suprayectiva: | ||
− | · surj_def: surj f | + | · surj_def: surj f ≡ ∀y. ∃x. y = f x |
Función biyectiva: | Función biyectiva: | ||
− | · bij_def: bij f | + | · bij_def: bij f ≡ inj f ∧ surj f |
Propiedades de las funciones inversas: | Propiedades de las funciones inversas: | ||
− | · inv_f_f: inj f | + | · inv_f_f: inj f ⟹ inv f (f x) = x |
− | · surj_f_inv_f: surj f | + | · surj_f_inv_f: surj f ⟹ f (inv f y) = y |
− | · inv_inv_eq: bij f | + | · inv_inv_eq: bij f ⟹ inv (inv f) = f |
Igualdad de funciones (por extensionalidad): | Igualdad de funciones (por extensionalidad): | ||
− | · fun_eq_iff: (f = g) = ( | + | · fun_eq_iff: (f = g) = (∀x. f x = g x) |
Lema. Una función inyectiva puede cancelarse en el lado izquierdo de | Lema. Una función inyectiva puede cancelarse en el lado izquierdo de | ||
Línea 429: | Línea 429: | ||
lemma | lemma | ||
assumes "inj f" | assumes "inj f" | ||
− | shows "(f | + | shows "(f ∘ g = f ∘ h) = (g = h)" |
proof | proof | ||
− | assume "f | + | assume "f ∘ g = f ∘ h" |
thus "g = h" using `inj f` by (simp add:fun_eq_iff inj_on_def) | thus "g = h" using `inj f` by (simp add:fun_eq_iff inj_on_def) | ||
next | next | ||
assume "g = h" | assume "g = h" | ||
− | thus "f | + | thus "f ∘ g = f ∘ h" by auto |
qed | qed | ||
Línea 444: | Línea 444: | ||
lemma | lemma | ||
assumes "inj f" | assumes "inj f" | ||
− | shows "(f | + | shows "(f ∘ g = f ∘ h) = (g = h)" |
proof | proof | ||
− | assume "f | + | assume "f ∘ g = f ∘ h" |
show "g = h" | show "g = h" | ||
proof | proof | ||
fix x | fix x | ||
− | have "(f | + | have "(f ∘ g)(x) = (f ∘ h)(x)" using `f ∘ g = f ∘ h` by simp |
hence "f(g(x)) = f(h(x))" by simp | hence "f(g(x)) = f(h(x))" by simp | ||
thus "g(x) = h(x)" using `inj f` by (simp add:inj_on_def) | thus "g(x) = h(x)" using `inj f` by (simp add:inj_on_def) | ||
Línea 456: | Línea 456: | ||
next | next | ||
assume "g = h" | assume "g = h" | ||
− | show "f | + | show "f ∘ g = f ∘ h" |
proof | proof | ||
fix x | fix x | ||
− | have "(f | + | have "(f ∘ g) x = f(g(x))" by simp |
− | also have " | + | also have "… = f(h(x))" using `g = h` by simp |
− | also have " | + | also have "… = (f ∘ h) x" by simp |
− | finally show "(f | + | finally show "(f ∘ g) x = (f ∘ h) x" by simp |
qed | qed | ||
qed | qed | ||
Línea 470: | Línea 470: | ||
text {* | text {* | ||
Imagen de un conjunto mediante una función: | Imagen de un conjunto mediante una función: | ||
− | · image_def: f ` A = {y. ( | + | · image_def: f ` A = {y. (∃x∈A. y = f x) |
Propiedades de la imagen: | Propiedades de la imagen: | ||
− | · image_compose: (f | + | · image_compose: (f ∘ g)`r = f`g`r |
− | · image_Un: f`(A | + | · image_Un: f`(A ∪ B) = f`A ∪ f`B |
− | · image_Int: inj f | + | · image_Int: inj f ⟹ f`(A ∩ B) = f`A ∩ f`B" |
Ejemplos de demostraciones triviales de propiedades de la imagen. | Ejemplos de demostraciones triviales de propiedades de la imagen. | ||
*} | *} | ||
− | lemma "f`A | + | lemma "f`A ∪ g`A = (⋃x∈A. {f x, g x})" |
by auto | by auto | ||
Línea 490: | Línea 490: | ||
Imagen inversa de un conjunto: | Imagen inversa de un conjunto: | ||
− | · vimage_def: f -` B | + | · vimage_def: f -` B ≡ {x. f x : B} |
Propiedad de la imagen inversa de un conjunto: | Propiedad de la imagen inversa de un conjunto: | ||
Línea 506: | Línea 506: | ||
Relación identidad: | Relación identidad: | ||
− | · Id_def: Id | + | · Id_def: Id ≡ {p. ∃x. p = (x,x)} |
Composición de relaciones: | Composición de relaciones: | ||
− | · rel_comp_def: r O s | + | · rel_comp_def: r O s ≡ {(x,z). EX y. (x, y) ∈ r & (y, z) ∈ s} |
Propiedades: | Propiedades: | ||
· R_O_Id: R O Id = R | · R_O_Id: R O Id = R | ||
− | · rel_comp_mono: | + | · rel_comp_mono: ⟦r' ⊆ r; s' ⊆ s⟧ ⟹ (r' O s') ⊆ (r O s) |
Imagen inversa de una relación: | Imagen inversa de una relación: | ||
− | · converse_iff: ((a,b) | + | · converse_iff: ((a,b) ∈ r\<^bsup>\<^sup>-1\<^esup>) = ((b,a) ∈ r) |
Propiedad de la imagen inversa de una relación: | Propiedad de la imagen inversa de una relación: | ||
Línea 522: | Línea 522: | ||
Imagen de un conjunto mediante una relación: | Imagen de un conjunto mediante una relación: | ||
− | · Image_iff: (b | + | · Image_iff: (b ∈ r``A) = (∃x:A. (x, b) ∈ r) |
Dominio de una relación: | Dominio de una relación: | ||
− | · Domain_iff: (a | + | · Domain_iff: (a ∈ Domain r) = (∃y. (a, y) ∈ r) |
Rango de una relación: | Rango de una relación: | ||
− | · Range_iff: (a | + | · Range_iff: (a ∈ Range r) = (∃y. (y,a) ∈ r) |
*} | *} | ||
Línea 543: | Línea 543: | ||
La clausura reflexiva y transitiva de la relación r es la menor | La clausura reflexiva y transitiva de la relación r es la menor | ||
solución de la ecuación: | solución de la ecuación: | ||
− | · rtrancl_unfold: r\<^sup>* = Id | + | · rtrancl_unfold: r\<^sup>* = Id ∪ (r\<^sup>* O r) |
Propiedades básicas de la clausura reflexiva y transitiva: | Propiedades básicas de la clausura reflexiva y transitiva: | ||
− | · rtrancl_refl: (a, a) | + | · rtrancl_refl: (a, a) ∈ r\<^sup>* |
− | · r_into_rtrancl: p | + | · r_into_rtrancl: p ∈ r ⟹ p ∈ r\<^sup>* |
− | · rtrancl_trans: | + | · rtrancl_trans: ⟦(a, b) ∈ r\<^sup>*; (b, c) ∈ r\<^sup>*⟧ ⟹ (a, c) ∈ r\<^sup>* |
Inducción sobre la clausura reflexiva y transitiva | Inducción sobre la clausura reflexiva y transitiva | ||
− | · rtrancl_induct: | + | · rtrancl_induct: ⟦(a,b) ∈ r\<^sup>*; |
P b; | P b; | ||
− | + | ⋀y z. ⟦(y, z) ∈ r; (z, b) ∈ r\<^sup>*; P z⟧ ⟹ P y⟧ | |
− | + | ⟹ P a"} | |
Idempotencia de la clausura reflexiva y transitiva: | Idempotencia de la clausura reflexiva y transitiva: | ||
Línea 560: | Línea 560: | ||
Reglas de introducción de la clausura transitiva: | Reglas de introducción de la clausura transitiva: | ||
− | · r_into_trancl': p | + | · r_into_trancl': p ∈ r ⟹ p ∈ r\<^sup>+ |
− | · trancl_trans: | + | · trancl_trans: ⟦(a, b) ∈ r\<^sup>+; (b, c) ∈ r\<^sup>+⟧ ⟹ (a, c) ∈ r\<^sup>+ |
Ejemplo de propiedad: | Ejemplo de propiedad: | ||
− | · trancl\_converse: ( | + | · trancl\_converse: (r¯¹)\<^sup>+ = (r\<^sup>+)¯¹ |
*} | *} | ||
Línea 576: | Línea 576: | ||
*} | *} | ||
− | lemma rtrancl_converseD: "(x,y) | + | lemma rtrancl_converseD: "(x,y) ∈ (r¯¹)\<^sup>* ⟹ (y,x) ∈ r\<^sup>*" |
proof (induct rule:rtrancl_induct) | proof (induct rule:rtrancl_induct) | ||
− | show "(x,x) | + | show "(x,x) ∈ r\<^sup>*" by (rule rtrancl_refl) |
next | next | ||
fix y z | fix y z | ||
− | assume "(x,y) | + | assume "(x,y) ∈ (r¯¹)\<^sup>*" and "(y,z) ∈ r¯¹" and "(y,x) ∈ r\<^sup>*" |
− | show "(z,x) | + | show "(z,x) ∈ r\<^sup>*" |
proof (rule rtrancl_trans) | proof (rule rtrancl_trans) | ||
− | show "(z,y) | + | show "(z,y) ∈ r\<^sup>*" using `(y,z) ∈ r¯¹` by simp |
next | next | ||
− | show "(y,x) | + | show "(y,x) ∈ r\<^sup>*" using `(y,x) ∈ r\<^sup>*` by simp |
qed | qed | ||
qed | qed | ||
− | lemma rtrancl_converseI: "(y,x) | + | lemma rtrancl_converseI: "(y,x) ∈ r\<^sup>* ⟹ (x,y) ∈ (r¯¹)\<^sup>*" |
proof (induct rule:rtrancl_induct) | proof (induct rule:rtrancl_induct) | ||
− | show "(y,y) | + | show "(y,y) ∈ (r¯¹)\<^sup>*" by (rule rtrancl_refl) |
next | next | ||
fix u z | fix u z | ||
− | assume "(y,u) | + | assume "(y,u) ∈ r\<^sup>*" and "(u,z) ∈ r" and "(u,y) ∈ (r¯¹)\<^sup>*" |
− | show "(z,y) | + | show "(z,y) ∈ (r¯¹)\<^sup>*" |
proof (rule rtrancl_trans) | proof (rule rtrancl_trans) | ||
− | show "(z,u) | + | show "(z,u) ∈ (r¯¹)\<^sup>*" using `(u,z) ∈ r` by auto |
next | next | ||
− | show "(u,y) | + | show "(u,y) ∈ (r¯¹)\<^sup>*" using `(u,y) ∈ (r¯¹)\<^sup>*` by simp |
qed | qed | ||
qed | qed | ||
− | theorem rtrancl_converse: "( | + | theorem rtrancl_converse: "(r¯¹)\<^sup>* = (r\<^sup>*)¯¹" |
proof | proof | ||
− | show "( | + | show "(r¯¹)\<^sup>* ⊆ (r\<^sup>*)¯¹" by (auto simp add:rtrancl_converseD) |
next | next | ||
− | show "(r\<^sup>*) | + | show "(r\<^sup>*)¯¹ ⊆ (r¯¹)\<^sup>*" by (auto simp add:rtrancl_converseI) |
qed | qed | ||
Línea 615: | Línea 615: | ||
*} | *} | ||
− | theorem "( | + | theorem "(r¯¹)\<^sup>* = (r\<^sup>*)¯¹" |
by (auto intro: rtrancl_converseI dest: rtrancl_converseD) | by (auto intro: rtrancl_converseI dest: rtrancl_converseD) | ||
Línea 626: | Línea 626: | ||
La relación-objeto "less_than" es el orden de los naturales que es | La relación-objeto "less_than" es el orden de los naturales que es | ||
bien fundamentada: | bien fundamentada: | ||
− | · less_than_iff: ((x,y) | + | · less_than_iff: ((x,y) ∈ less_than) = (x < y) |
· wf_less_than: wf less_than | · wf_less_than: wf less_than | ||
Notas sobre medidas: | Notas sobre medidas: | ||
· Imagen inversa de una relación mediante una función: | · Imagen inversa de una relación mediante una función: | ||
− | · inv_image_def: inv_image r f | + | · inv_image_def: inv_image r f ≡ {(x,y). (f x,f y) ∈ r |
· Conservación de la buena fundamentación:\\ | · Conservación de la buena fundamentación:\\ | ||
− | · wf_inv_image: wf r | + | · wf_inv_image: wf r ⟹ wf (inv_image r f) |
· Definición de la \textbf{medida}:\\ | · Definición de la \textbf{medida}:\\ | ||
− | · measure_def: measure | + | · measure_def: measure ≡ inv_image less_than |
· Buena fundamentación de la medida:\\ | · Buena fundamentación de la medida:\\ | ||
· wf_measure: wf (measure f) | · wf_measure: wf (measure f) | ||
Línea 643: | Línea 643: | ||
Notas sobre el producto lexicográfico: | Notas sobre el producto lexicográfico: | ||
· Definición del producto lexicográfico (lex_prod_def)": | · Definición del producto lexicográfico (lex_prod_def)": | ||
− | ra <*lex*> rb | + | ra <*lex*> rb ≡ {((a,b),(a',b')). (a,a') ∈ ra ∨ |
− | (a = a' | + | (a = a' ∧ (b,b') ∈ rb)} |
· Conservación de la buena fundamentación: | · Conservación de la buena fundamentación: | ||
− | · wf_lex_prod: | + | · wf_lex_prod: ⟦wf ra; wf rb⟧ ⟹ wf (ra <*lex*> rb) |
El orden de multiconjuntos está en la teoría HOL/Library/Multiset.thy. | El orden de multiconjuntos está en la teoría HOL/Library/Multiset.thy. | ||
Inducción sobre relaciones bien fundamentadas: | Inducción sobre relaciones bien fundamentadas: | ||
− | · wf_induct: | + | · wf_induct: ⟦wf r; ⋀x. (⋀y. (y,x) ∈ r ⟹ P y) ⟹ P x⟧ ⟹ P a |
*} | *} | ||
end | end | ||
</source> | </source> |
Revisión actual del 21:07 31 ene 2012
header {* Tema 12: Conjuntos, funciones y relaciones *}
theory Tema_12
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 \textbf{diferencia} y del complementario:
· Diff_disjoint: A ∩ (B - A) = {}
· Compl_partition: A ∪ - A = UNIV
Nota. Reglas de la relación de \textbf{subconjunto}:
· subsetI: (⋀x. x ∈ A ⟹ x ∈ B) ⟹ A ⊆ B
· subsetD: ⟦A ⊆ B; c ∈ A⟧ ⟹ c ∈ B
Nota. Ejemplo trivial.
*}
lemma "(A ∪ B ⊆ C) = (A ⊆ C ∧ B ⊆ C)"
by blast
text {*
Nota. Otro ejemplo trivial.
*}
lemma "(A ⊆ -B) = (B ⊆ -A)"
by blast
text {*
Principio de extensionalidad de conjuntos:
· set_ext: (⋀x. (x ∈ A) = (x ∈ B)) ⟹ A = B
Reglas de la igualdad de conjuntos:
· equalityI: ⟦A ⊆ B; B ⊆ A⟧ ⟹ A = B
· equalityE: ⟦A = B; ⟦A ⊆ B; B ⊆ A⟧ ⟹ P⟧ ⟹ P
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.
Nota. Lema trivial.
*}
lemma "{a,b} ∪ {c,d} = {a,b,c,d}"
by blast
text {*
Nota. Conjetura falsa.
*}
lemma "{a,b} ∩ {b,c} = {b}"
refute
oops
text {*
Nota. Conjetura corregida.
*}
lemma "{a,b} ∩ {b,c} = (if a=c then {a,b} else {b})"
by auto
text {*
Sumas y productos de conjuntos finitos:
· (setsum f A) es la suma de la aplicación de f a los elementos del
conjunto finito A,
· (setprod f A) es producto de la aplicación de f a los elementos del
conjunto finito A,
· ∑A es la suma de los elementos del conjunto finito A,
· ∏A es el producto de los elementos del conjunto finito A.
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.
· productoConj A es el producto de los elementos de A.
· sumaCuadradosconj A es la suma de los cuadrados de los elementos A.
*}
definition sumaConj :: "nat set ⇒ nat" where
"sumaConj S ≡ ∑S"
definition productoConj :: "nat set ⇒ nat" where
"productoConj S ≡ ∏S"
definition sumaCuadradosConj :: "nat set ⇒ nat" where
"sumaCuadradosConj S ≡ setsum (λx. x*x) S"
text {*
Nota. Para simplificar lo que sigue, declaramos las anteriores
definiciones como reglas de simplificación.
*}
declare sumaConj_def[simp]
declare productoConj_def[simp]
declare sumaCuadradosConj_def[simp]
text {*
Ejemplos de evaluación de las anteriores definiciones recursivas.
*}
lemma
"sumaConj {1,2,3,4} = 10 ∧
productoConj {1,2,3} = productoConj {3,2} ∧
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
Lema. [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.
Demostración automática:
*}
lemma "finite S ⟹ ∀x∈S. x ≤ sumaConj S"
by (induct rule: finite_induct) auto
text {*
Demostración estructurada:
*}
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"
hence "y ≤ x + (sumaConj F)" by simp
also have "… = sumaConj (insert x F)" using fF xF by simp
finally show ?thesis .
next
assume "y ≠ x"
hence "y ∈ F" using `y ∈ insert x F` by simp
hence "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
Dos lemas triviales.
*}
lemma "{x. P x ∨ x ∈ A} = {x. P x} ∪ A"
by blast
lemma "{x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x}"
by blast
text {*
Nota. Ejemplo con la sintaxis general de comprensión.
*}
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 {*
Definición. [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 {*
Lema. [Ejemplo con las reglas de intersección y comprensión]
El conjunto de los pares es disjunto con el de los impares.
*}
lemma "x ∉ (Pares ∩ Impares)"
proof
fix x assume S: "x ∈ (Pares ∩ Impares)"
hence "x ∈ Pares" by (rule IntD1)
hence "∃ 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)
hence "∃ 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
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 P" es lo mismo que "∀x∈A. P x".
· "Bex 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".
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)
Lema. Una función inyectiva puede cancelarse en el lado izquierdo de
la composición de funciones.
*}
lemma
assumes "inj f"
shows "(f ∘ g = f ∘ h) = (g = h)"
proof
assume "f ∘ g = f ∘ h"
thus "g = h" using `inj f` by (simp add:fun_eq_iff inj_on_def)
next
assume "g = h"
thus "f ∘ g = f ∘ h" by auto
qed
text {*
Una demostración más detallada es la siguiente
*}
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
hence "f(g(x)) = f(h(x))" by simp
thus "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
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"
Ejemplos de demostraciones triviales de propiedades de la imagen.
*}
lemma "f`A ∪ g`A = (⋃x∈A. {f x, g x})"
by auto
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). EX 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\<^bsup>\<^sup>-1\<^esup>) = ((b,a) ∈ r)
Propiedad de la imagen inversa de una relación:
· converse_rel_comp: (r O s)\<^bsup>-1\<^esup> = s\<^bsup>-1\<^esup> O r\<^bsup>-1\<^esup>
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)
*}
subsection {* Clausura reflexiva y transitiva *}
text {*
La teoría de la clausura reflexiva y transitiva de una relación es
HOL/Transitive_Closure.thy.
Potencias de relaciones:
· R ^^ 0 = Id
· R ^^ (Suc n) = (R ^^ n) O R
La clausura reflexiva y transitiva de la relación r es la menor
solución de la ecuación:
· rtrancl_unfold: r\<^sup>* = Id ∪ (r\<^sup>* O r)
Propiedades básicas de la clausura reflexiva y transitiva:
· rtrancl_refl: (a, a) ∈ r\<^sup>*
· r_into_rtrancl: p ∈ r ⟹ p ∈ r\<^sup>*
· rtrancl_trans: ⟦(a, b) ∈ r\<^sup>*; (b, c) ∈ r\<^sup>*⟧ ⟹ (a, c) ∈ r\<^sup>*
Inducción sobre la clausura reflexiva y transitiva
· rtrancl_induct: ⟦(a,b) ∈ r\<^sup>*;
P b;
⋀y z. ⟦(y, z) ∈ r; (z, b) ∈ r\<^sup>*; P z⟧ ⟹ P y⟧
⟹ P a"}
Idempotencia de la clausura reflexiva y transitiva:
· rtrancl_idemp: (r\<^sup>* )\<^sup>* = r\<^sup>*
Reglas de introducción de la clausura transitiva:
· r_into_trancl': p ∈ r ⟹ p ∈ r\<^sup>+
· trancl_trans: ⟦(a, b) ∈ r\<^sup>+; (b, c) ∈ r\<^sup>+⟧ ⟹ (a, c) ∈ r\<^sup>+
Ejemplo de propiedad:
· trancl\_converse: (r¯¹)\<^sup>+ = (r\<^sup>+)¯¹
*}
subsection {* Una demostración elemental *}
text {*
El teorema que se desea demostrar es que la clausura reflexiva y
transitiva conmuta con la inversa (rtrancl_converse). Para
demostrarlo introducimos dos lemas auxiliares: rtrancl_converseD y
rtrancl_converseI.
*}
lemma rtrancl_converseD: "(x,y) ∈ (r¯¹)\<^sup>* ⟹ (y,x) ∈ r\<^sup>*"
proof (induct rule:rtrancl_induct)
show "(x,x) ∈ r\<^sup>*" by (rule rtrancl_refl)
next
fix y z
assume "(x,y) ∈ (r¯¹)\<^sup>*" and "(y,z) ∈ r¯¹" and "(y,x) ∈ r\<^sup>*"
show "(z,x) ∈ r\<^sup>*"
proof (rule rtrancl_trans)
show "(z,y) ∈ r\<^sup>*" using `(y,z) ∈ r¯¹` by simp
next
show "(y,x) ∈ r\<^sup>*" using `(y,x) ∈ r\<^sup>*` by simp
qed
qed
lemma rtrancl_converseI: "(y,x) ∈ r\<^sup>* ⟹ (x,y) ∈ (r¯¹)\<^sup>*"
proof (induct rule:rtrancl_induct)
show "(y,y) ∈ (r¯¹)\<^sup>*" by (rule rtrancl_refl)
next
fix u z
assume "(y,u) ∈ r\<^sup>*" and "(u,z) ∈ r" and "(u,y) ∈ (r¯¹)\<^sup>*"
show "(z,y) ∈ (r¯¹)\<^sup>*"
proof (rule rtrancl_trans)
show "(z,u) ∈ (r¯¹)\<^sup>*" using `(u,z) ∈ r` by auto
next
show "(u,y) ∈ (r¯¹)\<^sup>*" using `(u,y) ∈ (r¯¹)\<^sup>*` by simp
qed
qed
theorem rtrancl_converse: "(r¯¹)\<^sup>* = (r\<^sup>*)¯¹"
proof
show "(r¯¹)\<^sup>* ⊆ (r\<^sup>*)¯¹" by (auto simp add:rtrancl_converseD)
next
show "(r\<^sup>*)¯¹ ⊆ (r¯¹)\<^sup>*" by (auto simp add:rtrancl_converseI)
qed
text {*
Puede demostrarse de manera más corta como sigue:
*}
theorem "(r¯¹)\<^sup>* = (r\<^sup>*)¯¹"
by (auto intro: rtrancl_converseI dest: rtrancl_converseD)
section {* Relaciones bien fundamentadas e inducción *}
text {*
La teoría de las relaciones bien fundamentadas es
HOL/Wellfounded_Relations.thy.
La relación-objeto "less_than" es el orden de los naturales que es
bien fundamentada:
· less_than_iff: ((x,y) ∈ less_than) = (x < y)
· wf_less_than: wf less_than
Notas sobre medidas:
· Imagen inversa de una relación mediante una función:
· inv_image_def: inv_image r f ≡ {(x,y). (f x,f y) ∈ r
· Conservación de la buena fundamentación:\\
· wf_inv_image: wf r ⟹ wf (inv_image r f)
· Definición de la \textbf{medida}:\\
· measure_def: measure ≡ inv_image less_than
· Buena fundamentación de la medida:\\
· wf_measure: wf (measure f)
*}
text {*
Notas sobre el producto lexicográfico:
· Definición del producto lexicográfico (lex_prod_def)":
ra <*lex*> rb ≡ {((a,b),(a',b')). (a,a') ∈ ra ∨
(a = a' ∧ (b,b') ∈ rb)}
· Conservación de la buena fundamentación:
· wf_lex_prod: ⟦wf ra; wf rb⟧ ⟹ wf (ra <*lex*> rb)
El orden de multiconjuntos está en la teoría HOL/Library/Multiset.thy.
Inducción sobre relaciones bien fundamentadas:
· wf_induct: ⟦wf r; ⋀x. (⋀y. (y,x) ∈ r ⟹ P y) ⟹ P x⟧ ⟹ P a
*}
end