RA2014: Conjuntos, funciones y relaciones

En 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

header {* Tema 9: Conjuntos, funciones y relaciones *}

theory T9
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_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   
*}

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}" 
nitpick
oops

text {*
  Ejemplo con la 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"

value "sumaConj {2,5,3}" -- "= 10"

definition productoConj :: "nat set ⇒ nat" where
  "productoConj S ≡ ∏S"

definition sumaCuadradosConj :: "nat set ⇒ nat" where
  "sumaCuadradosConj S ≡ setsum (λx. x*x) S"

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 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   
*}

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"
      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   
*}

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)"
  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

-- "La demostración estructurada es"
lemma "x ∉ (Pares ∩ Impares)"
proof 
  fix x assume S: "x ∈ (Pares ∩ Impares)"
  hence "x ∈ Pares" ..
  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" ..
  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

-- "La demostración automática es"
lemma "x ∉ (Pares ∩ Impares)"
by (auto simp add: Pares_def Impares_def mem_Collect_eq, 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
    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

-- "La demostración estructurada es"
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: inj_on_def fun_eq_iff) 
next
  assume "g = h" 
  thus "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\<^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 {*
  Se desea demostrar que la clausura reflexiva y transitiva conmuta con
  la inversa (cl_rtrans_inversa). Para demostrarlo introducimos dos lemas
  auxiliares: cl_rtrans_inversaD y cl_rtrans_inversaI.
*}

-- "La demostración detallada del primer lema es"
lemma cl_rtrans_inversaD: 
  "(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

-- "La demostración automática del primer lema es"
lemma  cl_rtrans_inversaD2: 
  "(x,y) ∈ (r¯¹)\<^sup>* ⟹ (y,x) ∈ r\<^sup>*"
by (induct rule: rtrancl_induct) 
   (auto simp add: rtrancl_refl rtrancl_trans)

-- "La demostración detallada del segundo lema es"
lemma cl_rtrans_inversaI: 
  "(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

-- "La demostración detalla del teorema es"
theorem cl_rtrans_inversa: 
  "(r¯¹)\<^sup>* = (r\<^sup>*)¯¹"
proof
  show "(r¯¹)\<^sup>* ⊆ (r\<^sup>*)¯¹" by (auto simp add:cl_rtrans_inversaD)
next
  show "(r\<^sup>*)¯¹ ⊆ (r¯¹)\<^sup>*" by (auto simp add:cl_rtrans_inversaI)
qed

-- "La demostración automática del teorema es"
theorem "(r¯¹)\<^sup>* = (r\<^sup>*)¯¹"
by (auto intro: cl_rtrans_inversaI dest: cl_rtrans_inversaD)

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 definido por
  · less_than = pred_nat\<^bsup>+\<^esup>
  donde pred_nat está definida por 
  · pred_nat = {(m, n). n = Suc m}

  La caracterización de less_than es
  · less_than_iff: ((x,y) ∈ less_than) = (x < y)

  La relación less_than está bien fundamentada
  · 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 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
*}

section {* Puntos fijos *}

text {*
  La teoría de los puntos fijos se aplican a las funciones monótonas.

  Las funciones monótonas está definida (en Orderings.thy) por
  · mono_def: mono f ≡ ∀A B. A ≤ B ⟶ f A ≤ f B 

  Las reglas de introducción y eliminación de la monotonicidad son:
  . monoI: (⋀A B. A ≤ B ⟹ f A ≤ f B) ⟹ mono f
  · monoD: ⟦mono f ⟹ A ≤ B⟧ ⟹ f A ≤ f B

  El menor punto fijo de un operador está definido en la teoría
  Inductive.thy, para los retículos completos, por
  · lfp_def: lfp f = Inf {u. f u ≤ u}

  El menor punto fijo de una función monótona es un punto fijo:
  · lfp_unfold: mono f ⟹ lfp f = f (lfp f)

  La regla de inducción del menor punto fijo es
  · lfp_induct_set: ⟦ a ∈ lfp(f);
                      mono(f); 
                      ⋀x. ⟦ x ∈ f(lfp(f) ⋂ {x. P(x)}) ⟧ ⟹ P(x) ⟧
                    ⟹ P(a)
*}

text {*
  El mayor punto fijo de un operador está definido en la teoría
  Inductive.thy, para los retículos completos, por
  · gfp_def: gfp f = Sup {u. u ≤ f u}

  El menor punto fijo de una función monótona es un punto fijo:
  · gfp_unfold: mono f ⟹ gfp f = f (gfp f)

  La regla de inducción del menor punto fijo es
  · coinduct_set: ⟦ mono(f);  
                    a ∈ X;  
                    X ⊆ f(X ⋃ gfp(f)) ⟧ 
                  ⟹ a ∈ gfp(f)
*}

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

292

293

294

295

296

297

298

299

300

301

302

303

304

305

306

307

308

309

310

311

312

313

314

315

316

317

318

319

320

321

322

323

324

325

326

327

328

329

330

331

332

333

334

335

336

337

338

339

340

341

342

343

344

345

346

347

348

349

350

351

352

353

354

355

356

357

358

359

360

361

362

363

364

365

366

367

368

369

370

371

372

373

374

375

376

377

378

379

380

381

382

383

384

385

386

387

388

389

390

391

392

393

394

395

396

397

398

399

400

401

402

403

404

405

406

407

408

409

410

411

412

413

414

415

416

417

418

419

420

421

422

423

424

425

426

427

428

429

430

431

432

433

434

435

436

437

438

439

440

441

442

443

444

445

446

447

448

449

450

451

452

453

454

455

456

457

458

459

460

461

462

463

464

465

466

467

468

469

470

471

472

473

474

475

476

477

478

479

480

481

482

483

484

485

486

487

488

489

490

491

492

493

494

495

496

497

498

499

500

501

502

503

504

505

506

507

508

509

510

511

512

513

514

515

516

517

518

519

520

521

522

523

524

525

526

527

528

529

530

531

532

533

534

535

536

537

538

539

540

541

542

543

544

545

546

547

548

549

550

551

552

553

554

555

556

557

558

559

560

561

562

563

564

565

566

567

568

569

570

571

572

573

574

575

576

577

578

579

580

581

582

583

584

585

586

587

588

589

590

591

592

593

594

595

596

597

598

599

600

601

602

603

604

605

606

607

608

609

610

611

612

613

614

615

616

617

618

619

620

621

622

623

624

625

626

627

628

629

630

631

632

633

634

635

636

637

638

639

640

641

642

643

644

645

646

647

648

649

650

651

652

653

654

655

656

657

658

659

660

661

662

663

664

665

666

667

668

669

670

671

672

673

674

675

676

677

678

679

680

681

682

683

684

685

686

687

688

689

690

691

692

693

694

695

696

697

698

699

700

701

702

703

704

705

706

707

708

709

710

711

712

713

714

715

716

717

718

719

720

721

722

723

724

725

726

727

728

729

730

731

732

733

734

735

736

737

738

739

740

741

742

743

744

745

746

747

748

749

750

751

752

753

754

755

756

757

758

759

760

761

header {* Tema 9: Conjuntos, funciones y relaciones *}

theory T9

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_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

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}"

nitpick

oops

text {*

Ejemplo con la 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"

value "sumaConj {2,5,3}" -- "= 10"

definition productoConj :: "nat set ⇒ nat" where

"productoConj S ≡ ∏S"

definition sumaCuadradosConj :: "nat set ⇒ nat" where

"sumaCuadradosConj S ≡ setsum (λx. x*x) S"

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 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

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

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 .

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

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)"

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

-- "La demostración estructurada es"

lemma "x ∉ (Pares ∩ Impares)"

proof

fix x assume S: "x ∈ (Pares ∩ Impares)"

hence "x ∈ Pares" ..

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" ..

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

-- "La demostración automática es"

lemma "x ∉ (Pares ∩ Impares)"

by (auto simp add: Pares_def Impares_def mem_Collect_eq, 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

hence "f(g(x)) = f(h(x))" by simp

thus "g(x) = h(x)" using `inj f` by (simp add:inj_on_def)

qed

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

-- "La demostración estructurada es"

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: inj_on_def fun_eq_iff)

assume "g = h"

thus "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\<^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 {*

Se desea demostrar que la clausura reflexiva y transitiva conmuta con

la inversa (cl_rtrans_inversa). Para demostrarlo introducimos dos lemas

auxiliares: cl_rtrans_inversaD y cl_rtrans_inversaI.

-- "La demostración detallada del primer lema es"

lemma cl_rtrans_inversaD:

"(x,y) ∈ (r¯¹)\<^sup>* ⟹ (y,x) ∈ r\<^sup>*"

proof (induct rule:rtrancl_induct)

show "(x,x) ∈ r\<^sup>*" by (rule rtrancl_refl)

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

show "(y,x) ∈ r\<^sup>*" using `(y,x) ∈ r\<^sup>*` by simp

qed

-- "La demostración automática del primer lema es"

lemma cl_rtrans_inversaD2:

"(x,y) ∈ (r¯¹)\<^sup>* ⟹ (y,x) ∈ r\<^sup>*"

by (induct rule: rtrancl_induct)

(auto simp add: rtrancl_refl rtrancl_trans)

-- "La demostración detallada del segundo lema es"

lemma cl_rtrans_inversaI:

"(y,x) ∈ r\<^sup>* ⟹ (x,y) ∈ (r¯¹)\<^sup>*"

proof (induct rule: rtrancl_induct)

show "(y,y) ∈ (r¯¹)\<^sup>*" by (rule rtrancl_refl)

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

show "(u,y) ∈ (r¯¹)\<^sup>*" using `(u,y) ∈ (r¯¹)\<^sup>*` by simp

qed

-- "La demostración detalla del teorema es"

theorem cl_rtrans_inversa:

"(r¯¹)\<^sup>* = (r\<^sup>*)¯¹"

proof

show "(r¯¹)\<^sup>* ⊆ (r\<^sup>*)¯¹" by (auto simp add:cl_rtrans_inversaD)

show "(r\<^sup>*)¯¹ ⊆ (r¯¹)\<^sup>*" by (auto simp add:cl_rtrans_inversaI)

qed

-- "La demostración automática del teorema es"

theorem "(r¯¹)\<^sup>* = (r\<^sup>*)¯¹"

by (auto intro: cl_rtrans_inversaI dest: cl_rtrans_inversaD)

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 definido por

· less_than = pred_nat\<^bsup>+\<^esup>

donde pred_nat está definida por

· pred_nat = {(m, n). n = Suc m}

La caracterización de less_than es

· less_than_iff: ((x,y) ∈ less_than) = (x < y)

La relación less_than está bien fundamentada

· 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 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

section {* Puntos fijos *}

text {*

La teoría de los puntos fijos se aplican a las funciones monótonas.

Las funciones monótonas está definida (en Orderings.thy) por

· mono_def: mono f ≡ ∀A B. A ≤ B ⟶ f A ≤ f B

Las reglas de introducción y eliminación de la monotonicidad son:

. monoI: (⋀A B. A ≤ B ⟹ f A ≤ f B) ⟹ mono f

· monoD: ⟦mono f ⟹ A ≤ B⟧ ⟹ f A ≤ f B

El menor punto fijo de un operador está definido en la teoría

Inductive.thy, para los retículos completos, por

· lfp_def: lfp f = Inf {u. f u ≤ u}

El menor punto fijo de una función monótona es un punto fijo:

· lfp_unfold: mono f ⟹ lfp f = f (lfp f)

La regla de inducción del menor punto fijo es

· lfp_induct_set: ⟦ a ∈ lfp(f);

mono(f);

⋀x. ⟦ x ∈ f(lfp(f) ⋂ {x. P(x)}) ⟧ ⟹ P(x) ⟧

⟹ P(a)

text {*

El mayor punto fijo de un operador está definido en la teoría

Inductive.thy, para los retículos completos, por

· gfp_def: gfp f = Sup {u. u ≤ f u}

El menor punto fijo de una función monótona es un punto fijo:

· gfp_unfold: mono f ⟹ gfp f = f (gfp f)

La regla de inducción del menor punto fijo es

· coinduct_set: ⟦ mono(f);

a ∈ X;

X ⊆ f(X ⋃ gfp(f)) ⟧

⟹ a ∈ gfp(f)

end

Se puede imprimir o compartir con