Demostración asistida por ordenador (2011-12) Demostración asistida por ordenador (2011-12)

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 \<tau>) y el conjunto tiene tipo (en el ejemplo, "\<tau> set"). 

  Reglas de la intersección:
  · IntI:  \<lbrakk>c \<in> A; c \<in> B\<rbrakk> \<Longrightarrow> c \<in> A \<inter> B
  · IntD1: c \<in> A \<inter> B \<Longrightarrow> c \<in> A
  · IntD2: c \<in> A \<inter> B \<Longrightarrow> c \<in> B

  Nota. Propiedades del complementario:
  · Compl_iff: (c \<in> - A) = (c \<notin> A)
  · Compl_Un:  - (A \<union> B) = - A \<inter> - 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 \<inter> (B - A) = {}
  · Compl_partition: A \<union> - A = UNIV

  Nota. Reglas de la relación de \textbf{subconjunto}:
  · subsetI: (\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B
  · subsetD: \<lbrakk>A \<subseteq> B; c \<in> A\<rbrakk> \<Longrightarrow> c \<in> B

  Nota. Ejemplo trivial.
*}

lemma "(A \<union> B \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
by blast

text {* 
  Nota. Otro ejemplo trivial.
*}

lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
by blast

text {*
  Principio de extensionalidad de conjuntos:
  · set_ext: (\<And>x. (x \<in> A) = (x \<in> B)) \<Longrightarrow> A = B

  Reglas de la igualdad de conjuntos:
  · equalityI: \<lbrakk>A \<subseteq> B; B \<subseteq> A\<rbrakk> \<Longrightarrow> A = B
  · equalityE: \<lbrakk>A = B; \<lbrakk>A \<subseteq> B; B \<subseteq> A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P

  Lema. [Analogía entre intersección y conjunción]
  "x \<in> A \<inter> B" syss "x \<in> A" y "x \<in> B".
*}

lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)" 
by simp

text {*
  Lema. [Analogía entre unión y disyunción]
  "x \<in> A \<union> B" syss "x \<in> A" ó "x \<in> B".
*}

lemma "(x \<in> A \<union> B) = (x \<in> A \<or> x \<in> B)" 
by simp

text {*
  Lema. [Analogía entre subconjunto e implicación]
  "(A \<subseteq> B)" syss para todo "x", si "x \<in> A" entonces "x \<in> B".
*}

lemma "(A \<subseteq> B) = (\<forall> x. x \<in> A \<longrightarrow> x \<in> 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 \<in> -A) = (x \<notin> 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 \<Longrightarrow> finite (insert a A)"

  A continuación se muestran ejemplos de conjuntos finitos.
*}

lemma 
  "insert 2 {} = {2} \<and>
  insert 3 {2} = {2,3} \<and>
  insert 2 {2,3} = {2,3} \<and>
  {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} \<union> {c,d} = {a,b,c,d}" 
by blast

text {*
  Nota. Conjetura falsa.
*}

lemma "{a,b} \<inter> {b,c} = {b}" 
refute
oops

text {*
  Nota. Conjetura corregida.
*}

lemma "{a,b} \<inter> {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,  
  · \<Sum>A es la suma de los elementos del conjunto finito A,
  · \<Prod>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 \<Rightarrow> nat" where
  "sumaConj S \<equiv> \<Sum>S"

definition productoConj :: "nat set \<Rightarrow> nat" where
  "productoConj S \<equiv> \<Prod>S"

definition sumaCuadradosConj :: "nat set \<Rightarrow> nat" where
  "sumaCuadradosConj S \<equiv> setsum (\<lambda>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 \<and>
  productoConj {1,2,3} = productoConj {3,2} \<and> 
  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: \<lbrakk>finite F; 
                    P {}; 
                    \<And>x F. \<lbrakk>finite F; x \<notin> F; P F\<rbrakk> \<Longrightarrow> P ({x} \<union> F)\<rbrakk> 
                   \<Longrightarrow> 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 \<Longrightarrow> \<forall>x\<in>S. x \<le> sumaConj S"
by (induct rule: finite_induct) auto

text {*
  Demostración estructurada:
*}

lemma sumaConj_acota: "finite S \<Longrightarrow> \<forall>x\<in>S. x \<le> sumaConj S"
proof (induct rule: finite_induct)
  show "\<forall>x\<in>{}. x \<le> sumaConj {}" by simp
next
  fix x and F
  assume fF: "finite F" 
     and xF: "x \<notin> F" 
     and HI: "\<forall> x\<in>F. x \<le> sumaConj F"
  show "\<forall>y\<in>insert x F. y \<le> sumaConj (insert x F)"
  proof 
    fix y 
    assume "y \<in> insert x F"
    show "y \<le> sumaConj (insert x F)"
    proof (cases "y = x")
      assume "y = x"
      hence "y \<le> x + (sumaConj F)" by simp
      also have "\<dots> = sumaConj (insert x F)" using fF xF by simp
      finally show ?thesis .
    next
      assume "y \<noteq> x"
      hence "y \<in> F" using `y \<in> insert x F` by simp
      hence "y \<le> sumaConj F" using HI by blast
      also have "\<dots> \<le> x + (sumaConj F)" by simp
      also have "\<dots> = 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 \<in> {x. P x}) = P a
  · Collect_mem_eq: {x. x \<in> A} = A
  
  Dos lemas triviales.
*}

lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
by blast

lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
by blast

text {*
  Nota. Ejemplo con la sintaxis general de comprensión.
*}

lemma 
  "{p*q | p q. p \<in> prime \<and> q \<in> prime} = 
   {z. \<exists>p q. z = p*q \<and> p \<in> prime \<and> q \<in> prime}"
by blast

text {*
   En HOL, la notación conjuntista es azúcar sintáctica:
   · x \<in> A  es equivalente a A(x).
   · {x. P} es equivalente a \<lambda>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 \<equiv> {n. \<exists> m. n = 2*m }"

text {*
  Ejemplo. Los números 2 y 34 son pares.
*}

lemma 
  "2 \<in> Pares \<and>
  34 \<in> 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 \<equiv> {n. \<exists> 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 \<notin> (Pares \<inter> Impares)"
proof 
  fix x assume S: "x \<in> (Pares \<inter> Impares)"
  hence "x \<in> Pares" by (rule IntD1)
  hence "\<exists> m. x = 2 * m" by (simp only: Pares_def mem_Collect_eq)
  then obtain p where p: "x = 2 * p" .. 

  from S have "x \<in> Impares" by (rule IntD2)
  hence "\<exists> 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: (\<And>x. x \<in> A \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<in>A. P x
  · bspec: \<lbrakk>\<forall>x\<in>A. P x; x \<in> A\<rbrakk> \<Longrightarrow> P x

  Reglas de cuantificador existencial acotado ("bounded"):
  · bexI: \<lbrakk>P x; x \<in> A\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. P x
  · bexE: \<lbrakk>\<exists>x\<in>A. P x; \<And>x. \<lbrakk>x \<in> A; P x\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q

  Reglas de la unión indexada:
  · UN_iff: (b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)
  · UN_I:   \<lbrakk>a \<in> A; b \<in> B a\<rbrakk> \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)
  · UN_E:   \<lbrakk>b \<in> (\<Union>x\<in>A. B x); \<And>x. \<lbrakk>x \<in> A; b \<in> B x\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R

  Reglas de la unión de una familia:
  · Union_def: \<Union>S = (\<Union>x\<in>S. x)
  · Union_iff: (A \<in> \<Union>C) = (\<exists>X\<in>C. A \<in> X)

  Reglas de la intersección indexada:
  · INT_iff: (b \<in> (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. b \<in> B x)
  · INT_I:   (\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)
  · INT_E:   \<lbrakk>b \<in> (\<Inter>x\<in>A. B x); b \<in> B a \<Longrightarrow> R; a \<notin> A \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R

  Reglas de la intersección de una familia:
  · Inter_def: \<Inter>S = (\<Inter>x\<in>S. x)
  · Inter_iff: (A \<in> \<Inter>C) = (\<forall>X\<in>C. A \<in> X)

  Abreviaturas:
  · "Collect P" es lo mismo que "{x. P}".
  · "All P"     es lo mismo que "\<forall>x. P x".
  · "Ex P"      es lo mismo que "\<exists>x. P x".
  · "Ball P"    es lo mismo que "\<forall>x\<in>A. P x".
  · "Bex P"     es lo mismo que "\<exists>x\<in>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 \<and>
   card {4} = 1 \<and>
   card {4,1} = 2 \<and>
   x \<noteq> y \<Longrightarrow> card {x,y} = 2" 
by simp

text {* 
  Propiedades de cardinales:
  · Cardinal de la unión de conjuntos finitos:
    card_Un_Int: \<lbrakk>finite A; finite B\<rbrakk> 
                 \<Longrightarrow> card A + card B = card (A \<union> B) + card (A \<inter> B)" 
  · Cardinal del conjunto potencia: 
    card_Pow: finite A \<Longrightarrow> 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: (\<And>x. f x = g x) \<Longrightarrow> 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 \<equiv> \<lambda>x. x

  Composición de funciones:
  · o_def: f \<circ> g = (\<lambda>x. f (g x))

  Asociatividad de la composición:
  · o_assoc: f \<circ> (g \<circ> h) = (f \<circ> g) \<circ> h
*}

subsection {* Funciones inyectivas, suprayectivas y biyectivas *}

text {*
  Función inyectiva sobre A:
  · inj_on_def: inj_on f A \<equiv> \<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y

  Nota. "inj f" es una abreviatura de "inj_on f UNIV".

  Función suprayectiva:
  · surj_def: surj f \<equiv> \<forall>y. \<exists>x. y = f x

  Función biyectiva:
  · bij_def: bij f \<equiv> inj f \<and> surj f

  Propiedades de las funciones inversas:
  · inv_f_f:      inj f \<Longrightarrow> inv f (f x) = x
  · surj_f_inv_f: surj f \<Longrightarrow> f (inv f y) = y
  · inv_inv_eq:   bij f \<Longrightarrow> inv (inv f) = f

  Igualdad de funciones (por extensionalidad):
  · fun_eq_iff: (f = g) = (\<forall>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 \<circ> g = f \<circ> h) = (g = h)"
proof 
  assume "f \<circ> g = f \<circ> h" 
  thus "g = h" using `inj f` by (simp add:fun_eq_iff inj_on_def) 
next
  assume "g = h" 
  thus "f \<circ> g = f \<circ> h" by auto
qed

text {*
  Una demostración más detallada es la siguiente
*}

lemma 
  assumes "inj f"
  shows "(f \<circ> g = f \<circ> h) = (g = h)"
proof 
  assume "f \<circ> g = f \<circ> h"
  show "g = h"
  proof
    fix x
    have "(f \<circ> g)(x) = (f \<circ> h)(x)" using `f \<circ> g = f \<circ> 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 \<circ> g = f \<circ> h"
  proof
    fix x
    have "(f \<circ> g) x = f(g(x))" by simp
    also have "\<dots> = f(h(x))" using `g = h` by simp
    also have "\<dots> = (f \<circ> h) x" by simp
    finally show "(f \<circ> g) x = (f \<circ> h) x" by simp
  qed
qed

subsubsection {* Función imagen *}

text {*
  Imagen de un conjunto mediante una función:
  · image_def: f ` A = {y. (\<exists>x\<in>A. y = f x)

  Propiedades de la imagen:
  · image_compose: (f \<circ> g)`r = f`g`r
  · image_Un:      f`(A \<union> B) = f`A \<union> f`B 
  · image_Int:     inj f \<Longrightarrow> f`(A \<inter> B) = f`A \<inter> f`B" 

  Ejemplos de demostraciones triviales de propiedades de la imagen.
*}

lemma "f`A \<union> g`A = (\<Union>x\<in>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 \<equiv> {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 \<equiv> {p. \<exists>x. p = (x,x)}

  Composición de relaciones:
  · rel_comp_def: r O s \<equiv> {(x,z). EX y. (x, y) \<in> r & (y, z) \<in> s}

  Propiedades:
  · R_O_Id:        R O Id = R
  · rel_comp_mono: \<lbrakk>r' \<subseteq> r; s' \<subseteq> s\<rbrakk> \<Longrightarrow> (r' O s') \<subseteq> (r O s)

  Imagen inversa de una relación:
  · converse_iff: ((a,b) \<in> r\<^bsup>\<^sup>-1\<^esup>) = ((b,a) \<in> 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 \<in> r``A) = (\<exists>x:A. (x, b) \<in> r)

  Dominio de una relación:
  · Domain_iff: (a \<in> Domain r) = (\<exists>y. (a, y) \<in> r)

  Rango de una relación:
  · Range_iff: (a \<in> Range r) = (\<exists>y. (y,a) \<in> 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 \<union> (r\<^sup>* O r)
  
  Propiedades básicas de la clausura reflexiva y transitiva:
  · rtrancl_refl:   (a, a) \<in> r\<^sup>*
  · r_into_rtrancl: p \<in> r \<Longrightarrow> p \<in> r\<^sup>*
  · rtrancl_trans:  \<lbrakk>(a, b) \<in> r\<^sup>*; (b, c) \<in> r\<^sup>*\<rbrakk> \<Longrightarrow> (a, c) \<in> r\<^sup>*
  
  Inducción sobre la clausura reflexiva y transitiva
  · rtrancl_induct: \<lbrakk>(a,b) \<in> r\<^sup>*; 
                     P b; 
                     \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; P z\<rbrakk> \<Longrightarrow> P y\<rbrakk>
                    \<Longrightarrow> 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 \<in> r \<Longrightarrow> p \<in> r\<^sup>+
  · trancl_trans:   \<lbrakk>(a, b) \<in> r\<^sup>+; (b, c) \<in> r\<^sup>+\<rbrakk> \<Longrightarrow> (a, c) \<in> r\<^sup>+

  Ejemplo de propiedad:
  · trancl\_converse: (r\<inverse>)\<^sup>+ = (r\<^sup>+)\<inverse>
*}

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) \<in> (r\<inverse>)\<^sup>* \<Longrightarrow> (y,x) \<in> r\<^sup>*"
proof (induct rule:rtrancl_induct)
  show "(x,x) \<in> r\<^sup>*" by (rule rtrancl_refl) 
next
  fix y z
  assume "(x,y) \<in> (r\<inverse>)\<^sup>*" and "(y,z) \<in> r\<inverse>" and "(y,x) \<in> r\<^sup>*"
  show "(z,x) \<in> r\<^sup>*"
  proof (rule rtrancl_trans)
    show "(z,y) \<in> r\<^sup>*" using `(y,z) \<in> r\<inverse>` by simp
  next
    show "(y,x) \<in> r\<^sup>*" using `(y,x) \<in> r\<^sup>*` by simp
  qed
qed

lemma rtrancl_converseI: "(y,x) \<in> r\<^sup>* \<Longrightarrow> (x,y) \<in> (r\<inverse>)\<^sup>*"
proof (induct rule:rtrancl_induct)
  show "(y,y) \<in> (r\<inverse>)\<^sup>*" by (rule rtrancl_refl) 
next
  fix u z
  assume "(y,u) \<in> r\<^sup>*" and "(u,z) \<in> r" and "(u,y) \<in> (r\<inverse>)\<^sup>*"
  show "(z,y) \<in> (r\<inverse>)\<^sup>*"
  proof (rule rtrancl_trans)
    show "(z,u) \<in> (r\<inverse>)\<^sup>*" using `(u,z) \<in> r` by auto
  next
    show "(u,y) \<in> (r\<inverse>)\<^sup>*" using `(u,y) \<in> (r\<inverse>)\<^sup>*` by simp
  qed
qed

theorem rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>"
proof
  show "(r\<inverse>)\<^sup>* \<subseteq> (r\<^sup>*)\<inverse>" by (auto simp add:rtrancl_converseD)
next
  show "(r\<^sup>*)\<inverse> \<subseteq> (r\<inverse>)\<^sup>*" by (auto simp add:rtrancl_converseI)
qed

text {*
  Puede demostrarse de manera más corta como sigue:
*}

theorem "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>"
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) \<in> 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 \<equiv> {(x,y). (f x,f y) \<in> r
  · Conservación de la buena fundamentación:\\
    · wf_inv_image: wf r \<Longrightarrow> wf (inv_image r f)
  · Definición de la \textbf{medida}:\\
    · measure_def: measure \<equiv> 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 \<equiv> {((a,b),(a',b')). (a,a') \<in> ra \<or> 
                                      (a = a' \<and> (b,b') \<in> rb)}
  · Conservación de la buena fundamentación:
    · wf_lex_prod: \<lbrakk>wf ra; wf rb\<rbrakk> \<Longrightarrow> 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: \<lbrakk>wf r; \<And>x. (\<And>y. (y,x) \<in> r \<Longrightarrow> P y) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a
*}

end