Razonamiento automático (2016-17) Razonamiento automático (2016-17)

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"

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 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"
      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, 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
    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" 
  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^-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)
*}

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^* = Id ∪ (r^* O r)
  
  Propiedades básicas de la clausura reflexiva y transitiva:
  · rtrancl_refl:   (a,a) ∈ r^*
  · r_into_rtrancl: p ∈ r ⟹ p ∈ r^*
  · rtrancl_trans:  ⟦(a,b) ∈ r^*; (b,c) ∈ r^*⟧ ⟹ (a,c) ∈ r^*
  
  Inducción sobre la clausura reflexiva y transitiva
  · rtrancl_induct: ⟦(a,b) ∈ r^*; 
                     P b; 
                     ⋀y z. ⟦(y,z) ∈ r; (z,b) ∈ r^*; P z⟧ ⟹ P y⟧
                    ⟹ P a
  
  Idempotencia de la clausura reflexiva y transitiva:
  · rtrancl_idemp: (r^*)^* = r^*
  
  Reglas de introducción de la clausura transitiva:
  · r_into_trancl': p ∈ r ⟹ p ∈ r^+
  · trancl_trans:   ⟦(a,b) ∈ r^+; (b,c) ∈ r^+⟧ ⟹ (a,c) ∈ r^+

  Ejemplo de propiedad:
  · trancl_converse: (r¯)^+ = (r^+)¯
*}

subsection {* Una demostración elemental *}

text {*
  Se desea demostrar que la clausura reflexiva y transitiva conmuta con
  la inversa (cl_rtrans_inversa). 
*}

theorem "(r¯)⇧* = (r⇧*)¯" 
oops

text {* 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¯)⇧* ⟹ (y,x) ∈ r⇧*"
proof (induct rule:rtrancl_induct)
  show "(x,x) ∈ r⇧*" by (rule rtrancl_refl) 
next
  fix y z
  assume "(x,y) ∈ (r¯)⇧*" and "(y,z) ∈ r¯" and "(y,x) ∈ r⇧*"
  show "(z,x) ∈ r⇧*"
  proof (rule rtrancl_trans)
    show "(z,y) ∈ r⇧*" using `(y,z) ∈ r¯` by simp
  next
    show "(y,x) ∈ r⇧*" using `(y,x) ∈ r⇧*` by simp
  qed   
qed

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

-- "La demostración detallada del segundo lema es"
lemma cl_rtrans_inversaI: 
  "(y,x) ∈ r⇧* ⟹ (x,y) ∈ (r¯)⇧*"
proof (induct rule: rtrancl_induct)
  show "(y,y) ∈ (r¯)⇧*" by (rule rtrancl_refl) 
next
  fix u z
  assume "(y,u) ∈ r⇧*" and "(u,z) ∈ r" and "(u,y) ∈ (r¯)⇧*"
  show "(z,y) ∈ (r¯)⇧*"
  proof (rule rtrancl_trans)
    show "(z,u) ∈ (r¯)⇧*" using `(u,z) ∈ r` by auto
  next
    show "(u,y) ∈ (r¯)⇧*" using `(u,y) ∈ (r¯)⇧*` by simp
  qed
qed

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

-- "La demostración automática del teorema es"
theorem "(r¯)⇧* = (r⇧*)¯"
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^+
  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