Lógica matemática y fundamentos (2018-19) Lógica matemática y fundamentos (2018-19)

chapter {* R13: Definiciones inductivas: clausuras *}

theory R13
imports Main
begin

section {* La clausura reflexiva transitiva *}

text {*
  · Las definiciones inductivas aceptan parámetros; por tanto, permite
    expresar funciones que construyen conjuntos.

  · La relaciones binarias son conjuntos de pares; por tanto, se pueden
   definir inductivamente.
*}

text {*
  · La clausura reflexiva y transitiva de una relación r es la menor
   relación reflexiva y transitiva que contiene a r. 

  · Se representa por r*.

  · Se puede definir inductivamente, como conjunto:
    · (x,x) ∈ r*
    · Si (x,y) ∈ r e (y,z) ∈ r*, entonces (x,z) ∈ r*

  · La definición inductiva, como conjunto, se puede expresar en 
   Isabelle/HOL como sigue: 
*}

inductive_set
  crt :: "('a × 'a) set ⇒ ('a × 'a) set"   ("_*" [1000] 999)
  for r :: "('a × 'a) set"
where
  crt_refl [iff]: "(x,x) ∈ r*"
| crt_paso:       "⟦(x,y) ∈ r; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"

text {*
  Notas:
  · La sintaxis concreta permite escribir r* en lugar de (crt r).
  · La definición consta de dos reglas.
  · A la regla reflexiva se le añade el atributo iff para aumentar la
    automatización. 
  · A la regla del paso no se le añade ningún atributo, porque r* ocurre
   en la izquierda. 
  · En el resto de esta sección se demuestra que esta definición
   coincide con la menor relación reflexiva y transitiva que contiene a
   r.  
*}

text {*
  Lema. La relación r* es reflexiva.
*}

lemma "(x,x) ∈ r*"
  oops

text {*
  Lema. La relación r* contiene a r.
*}

(* La demostración aplicativa es *)
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"  
  oops

(* La demostración automática es *)
lemma r_contenida_clausura [intro]: 
  "(x,y) ∈ r ⟹ (x,y) ∈ r*"
  oops
    
(* La demostración declarativa es *)
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"  
  oops

text {*
  Notas:
  · La ventaja del lema es que se puede declarar como regla de
    introducción, porque r* ocurre sólo en la derecha.
  · Con la declaración, algunas demostraciones que usan crt_paso se
    hacen de manera automática.
*}

text {*
  El esquema de inducción de la clausura reflexiva transitiva es
  · crt.induct:
    ⟦(x1, x2) ∈ r*; 
     ⋀x. P x x; 
     ⋀x y z. ⟦(x,y) ∈ r; (y,z) ∈ r*; P y z⟧ ⟹ P x z⟧
    ⟹ P x1 x2
*}

text {*
  Lema. La relación r* es transitiva.
*}

(* La demostración aplicativa es *)
lemma "⟦(x,y) ∈ r*; (y,z) ∈ r*⟧ ⟹ (x,z) ∈ r*"
  oops

lemma "⟦ (x,y) ∈ r*; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"
  oops 

text {*
  Otra formulación del lema, con la variable y a la derecha.
*}

(* La demostración aplicativa es *)
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
  oops
  
(* La demostración automática es *)
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
  oops

(* La demostración declarativa es *)
lemma crt_trans [rule_format]:
  "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
  oops

text {*
  Notas:
  · La reformulación anterior es un caso particular de la siguiente
    heurística:
       "Para probar una fórmula por inducción sobre (x1,...,xn) ∈ R,
       poner todas las premisas conteniendo cualquiera de lax xi en la
       conclusión usando ⟶". 
  · El atributo "rule_format" transforma ⟶ en ⟹.
*}

text {*
  La relación r* está contenida en cualquier relación reflexiva y 
  transitiva que contenga a r.

  Mediante (crt2 r) se define la menor relación reflexiva y transitiva 
  que contiene a r.
*}

inductive_set
  crt2 :: "('a × 'a)set ⇒ ('a × 'a)set"
  for r :: "('a × 'a)set"
where
  "(x,y) ∈ r ⟹ (x,y) ∈ crt2 r"                      (* contiene a r *) 
| "(x,x) ∈ crt2 r"                                      (* reflexiva *)
| "⟦(x,y) ∈ crt2 r; (y,z) ∈ crt2 r⟧ ⟹ (x,z) ∈ crt2 r" (* transitiva *)

text {* Probaremos que r* coincide con (crt2 r) *}

text {*
  Lema. La relación (crt2 r) está contenida en r*.
*}

(* La demostración aplicativa es *)
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
  oops

(* La demostración automática es *)
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
  oops

(* La demostración declarativa es *)
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
  oops

text {*
  Lema. La relación r* está contenida en (crt2 r).
*}

(* La demostración aplicativa es *)
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
  oops

(* La demostración automática es *)
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
  oops

(* La demostración declarativa es *)
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
  oops


text {* ---------------------------------------------------------------- 
  Ejercicio 1. Demostrar que si (x,y) ∈ r* e (y,z) ∈ r, entonces 
  (x,z) ∈ r*
  ------------------------------------------------------------------- *}

(* Demostración aplicativa *)
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
  oops 

(* Demostración aplicativa *)
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
  oops 

(* Demostración declarativa *)
lemma crt_paso2 [rule_format]: 
  "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
   oops 

text {* ---------------------------------------------------------------- 
  Ejercicio 2. Considerar la siguiente definición de la clausura tran-
  sitiva de una relación r, y probar que es la menor relación reflexiva 
  y transitiva que contiene a r.

  Nota: Establecer los lemas necesarios.
  ------------------------------------------------------------------- *}

inductive star' :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
  refl': "star' r x x" 
| step': "star' r x y ⟹ r y z ⟹ star' r x z"

(* Demostración de que (star' r) es reflexiva *)
lemma star'Refl: "star' r x x"
  oops 

(* Demostración aplicativa de r contenida en (star' r) *)
lemma "r x y ⟹ star' r x y"
  oops

(* Demostración automática de r contenida en (star' r) *)
lemma "r x y ⟹ star' r x y"
  oops
    
    
(* Demostración declarativa de r contenida en (star' r) *)
lemma rsubsetStar': "r x y ⟹ star' r x y"
   oops 

text {* A continuación se prueba una condición suficiente para star' r *}

(* Demostración aplicativa *)
lemma 
  "⟦star' r y z; r x y⟧ ⟹ star' r x z"
  oops

(* Demostración automática *)
lemma star'_subset_star'_l1:
  "⟦star' r y z; r x y⟧ ⟹ star' r x z"
  oops 

(* Demostraciones de que  (star' r) es transitiva *)

(* Demostración aplicativa *)
lemma "⟦star' r x y; star' r y z⟧ ⟹ star' r x z"   
  oops 

(* Demostración automática *)
lemma star'Trans: 
  "⟦star' r x y; star' r y z⟧ ⟹ star' r x z"
  oops 
   
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3. Considerar la siguiente definición inductiva. Probar que 
  "star' r x y syss (∃n. iter r n x y)"
  ------------------------------------------------------------------- *}

inductive iter :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool"
for r where
  iterRefl: "iter r 0 x x"
| iterStep: "⟦iter r n x y; r y z⟧ ⟹ iter r (n+1) x z"

(* El esquema de inducción correspondiente es *)
thm iter.induct
(*
  ⟦iter ?r ?x1.0 ?x2.0 ?x3.0; 
   ⋀x. ?P 0 x x;
   ⋀n x y z. ⟦iter ?r n x y; ?P n x y; ?r y z⟧ ⟹ ?P (n + 1) x z⟧
  ⟹ ?P ?x1.0 ?x2.0 ?x3.0
*)

(* Algunos teoremas derivados son *)

thm iterRefl
(* iter ?r 0 ?x ?x *)

thm iterRefl [of r y]
(* iter r 0 y y *)

thm iterStep
(* ⟦iter ?r ?n ?x ?y; ?r ?y ?z⟧ ⟹ iter ?r (?n + 1) ?x ?z *)

thm iterStep [of r x y n z]
(* ⟦iter r x y n; r n z⟧ ⟹ iter r (x + 1) y z *)

thm iterStep [of r x y 0 y]
(* ⟦iter r x y 0; r 0 y⟧ ⟹ iter r (x + 1) y y *)

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3.1. Demostrar  
     star' r x y ⟹ (∃n. iter r n x y)
  ------------------------------------------------------------------- *}

(* Demostración aplicativa *)
lemma "star' r x y ⟹ (∃n. iter r n x y)"
  oops 

(* Demostración automática *)
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"    
  oops 

(* Demostración declarativa *)
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"    
  oops 
  
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3.2. Demostrar  
     (∃n. iter r n x y) ⟹ star' r x y
  ------------------------------------------------------------------- *}

(* En la demostración se usará el siguiente lema:
      iter r n x y ⟹ star' r x y *)

(* Demostración aplicativa del lema *) 
lemma iter_star'_subset: "iter r n x y ⟹ star' r x y"
  oops 

(* Demostración automática del lema *) 
lemma "iter r n x y ⟹ star' r x y"
  oops 

(* Demostración aplicativa *)
lemma "(∃n. iter r n x y) ⟹ star' r x y"
  oops 

(* Demostración automática *)
lemma "(∃n. iter r n x y) ⟹ star' r x y"
  oops 

(* Demostración declarativa *)
lemma assumes "(∃n. iter r n x y)"
      shows "star' r x y"
  oops 

end
chapter {* R13: Definiciones inductivas: clausuras *}

theory R13
imports Main
begin

section {* La clausura reflexiva transitiva *}

text {*
  · Las definiciones inductivas aceptan parámetros; por tanto, permite
    expresar funciones que construyen conjuntos.

  · La relaciones binarias son conjuntos de pares; por tanto, se pueden
   definir inductivamente.
*}

text {*
  · La clausura reflexiva y transitiva de una relación r es la menor
   relación reflexiva y transitiva que contiene a r. 

  · Se representa por r*.

  · Se puede definir inductivamente, como conjunto:
    · (x,x) ∈ r*
    · Si (x,y) ∈ r e (y,z) ∈ r*, entonces (x,z) ∈ r*

  · La definición inductiva, como conjunto, se puede expresar en 
   Isabelle/HOL como sigue: 
*}

inductive_set
  crt :: "('a × 'a) set ⇒ ('a × 'a) set"   ("_*" [1000] 999)
  for r :: "('a × 'a) set"
where
  crt_refl [iff]: "(x,x) ∈ r*"
| crt_paso:       "⟦(x,y) ∈ r; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"

text {*
  Notas:
  · La sintaxis concreta permite escribir r* en lugar de (crt r).
  · La definición consta de dos reglas.
  · A la regla reflexiva se le añade el atributo iff para aumentar la
    automatización. 
  · A la regla del paso no se le añade ningún atributo, porque r* ocurre
   en la izquierda. 
  · En el resto de esta sección se demuestra que esta definición
   coincide con la menor relación reflexiva y transitiva que contiene a
   r.  
*}

text {*
  Lema. La relación r* es reflexiva.
*}

lemma "(x,x) ∈ r*"
  oops

text {*
  Lema. La relación r* contiene a r.
*}

(* La demostración aplicativa es *)
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"  
  oops

(* La demostración automática es *)
lemma r_contenida_clausura [intro]: 
  "(x,y) ∈ r ⟹ (x,y) ∈ r*"
  oops
    
(* La demostración declarativa es *)
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"  
  oops

text {*
  Notas:
  · La ventaja del lema es que se puede declarar como regla de
    introducción, porque r* ocurre sólo en la derecha.
  · Con la declaración, algunas demostraciones que usan crt_paso se
    hacen de manera automática.
*}

text {*
  El esquema de inducción de la clausura reflexiva transitiva es
  · crt.induct:
    ⟦(x1, x2) ∈ r*; 
     ⋀x. P x x; 
     ⋀x y z. ⟦(x,y) ∈ r; (y,z) ∈ r*; P y z⟧ ⟹ P x z⟧
    ⟹ P x1 x2
*}

text {*
  Lema. La relación r* es transitiva.
*}

(* La demostración aplicativa es *)
lemma "⟦(x,y) ∈ r*; (y,z) ∈ r*⟧ ⟹ (x,z) ∈ r*"
  oops

lemma "⟦ (x,y) ∈ r*; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"
  oops 

text {*
  Otra formulación del lema, con la variable y a la derecha.
*}

(* La demostración aplicativa es *)
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
  oops
  
(* La demostración automática es *)
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
  oops

(* La demostración declarativa es *)
lemma crt_trans [rule_format]:
  "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
  oops

text {*
  Notas:
  · La reformulación anterior es un caso particular de la siguiente
    heurística:
       "Para probar una fórmula por inducción sobre (x1,...,xn) ∈ R,
       poner todas las premisas conteniendo cualquiera de lax xi en la
       conclusión usando ⟶". 
  · El atributo "rule_format" transforma ⟶ en ⟹.
*}

text {*
  La relación r* está contenida en cualquier relación reflexiva y 
  transitiva que contenga a r.

  Mediante (crt2 r) se define la menor relación reflexiva y transitiva 
  que contiene a r.
*}

inductive_set
  crt2 :: "('a × 'a)set ⇒ ('a × 'a)set"
  for r :: "('a × 'a)set"
where
  "(x,y) ∈ r ⟹ (x,y) ∈ crt2 r"                      (* contiene a r *) 
| "(x,x) ∈ crt2 r"                                      (* reflexiva *)
| "⟦(x,y) ∈ crt2 r; (y,z) ∈ crt2 r⟧ ⟹ (x,z) ∈ crt2 r" (* transitiva *)

text {* Probaremos que r* coincide con (crt2 r) *}

text {*
  Lema. La relación (crt2 r) está contenida en r*.
*}

(* La demostración aplicativa es *)
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
  oops

(* La demostración automática es *)
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
  oops

(* La demostración declarativa es *)
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
  oops

text {*
  Lema. La relación r* está contenida en (crt2 r).
*}

(* La demostración aplicativa es *)
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
  oops

(* La demostración automática es *)
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
  oops

(* La demostración declarativa es *)
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
  oops


text {* ---------------------------------------------------------------- 
  Ejercicio 1. Demostrar que si (x,y) ∈ r* e (y,z) ∈ r, entonces 
  (x,z) ∈ r*
  ------------------------------------------------------------------- *}

(* Demostración aplicativa *)
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
  oops 

(* Demostración aplicativa *)
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
  oops 

(* Demostración declarativa *)
lemma crt_paso2 [rule_format]: 
  "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
   oops 

text {* ---------------------------------------------------------------- 
  Ejercicio 2. Considerar la siguiente definición de la clausura tran-
  sitiva de una relación r, y probar que es la menor relación reflexiva 
  y transitiva que contiene a r.

  Nota: Establecer los lemas necesarios.
  ------------------------------------------------------------------- *}

inductive star' :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
  refl': "star' r x x" 
| step': "star' r x y ⟹ r y z ⟹ star' r x z"

(* Demostración de que (star' r) es reflexiva *)
lemma star'Refl: "star' r x x"
  oops 

(* Demostración aplicativa de r contenida en (star' r) *)
lemma "r x y ⟹ star' r x y"
  oops

(* Demostración automática de r contenida en (star' r) *)
lemma "r x y ⟹ star' r x y"
  oops
    
    
(* Demostración declarativa de r contenida en (star' r) *)
lemma rsubsetStar': "r x y ⟹ star' r x y"
   oops 

text {* A continuación se prueba una condición suficiente para star' r *}

(* Demostración aplicativa *)
lemma 
  "⟦star' r y z; r x y⟧ ⟹ star' r x z"
  oops

(* Demostración automática *)
lemma star'_subset_star'_l1:
  "⟦star' r y z; r x y⟧ ⟹ star' r x z"
  oops 

(* Demostraciones de que  (star' r) es transitiva *)

(* Demostración aplicativa *)
lemma "⟦star' r x y; star' r y z⟧ ⟹ star' r x z"   
  oops 

(* Demostración automática *)
lemma star'Trans: 
  "⟦star' r x y; star' r y z⟧ ⟹ star' r x z"
  oops 
   
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3. Considerar la siguiente definición inductiva. Probar que 
  "star' r x y syss (∃n. iter r n x y)"
  ------------------------------------------------------------------- *}

inductive iter :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool"
for r where
  iterRefl: "iter r 0 x x"
| iterStep: "⟦iter r n x y; r y z⟧ ⟹ iter r (n+1) x z"

(* El esquema de inducción correspondiente es *)
thm iter.induct
(*
  ⟦iter ?r ?x1.0 ?x2.0 ?x3.0; 
   ⋀x. ?P 0 x x;
   ⋀n x y z. ⟦iter ?r n x y; ?P n x y; ?r y z⟧ ⟹ ?P (n + 1) x z⟧
  ⟹ ?P ?x1.0 ?x2.0 ?x3.0
*)

(* Algunos teoremas derivados son *)

thm iterRefl
(* iter ?r 0 ?x ?x *)

thm iterRefl [of r y]
(* iter r 0 y y *)

thm iterStep
(* ⟦iter ?r ?n ?x ?y; ?r ?y ?z⟧ ⟹ iter ?r (?n + 1) ?x ?z *)

thm iterStep [of r x y n z]
(* ⟦iter r x y n; r n z⟧ ⟹ iter r (x + 1) y z *)

thm iterStep [of r x y 0 y]
(* ⟦iter r x y 0; r 0 y⟧ ⟹ iter r (x + 1) y y *)

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3.1. Demostrar  
     star' r x y ⟹ (∃n. iter r n x y)
  ------------------------------------------------------------------- *}

(* Demostración aplicativa *)
lemma "star' r x y ⟹ (∃n. iter r n x y)"
  oops 

(* Demostración automática *)
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"    
  oops 

(* Demostración declarativa *)
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"    
  oops 
  
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3.2. Demostrar  
     (∃n. iter r n x y) ⟹ star' r x y
  ------------------------------------------------------------------- *}

(* En la demostración se usará el siguiente lema:
      iter r n x y ⟹ star' r x y *)

(* Demostración aplicativa del lema *) 
lemma iter_star'_subset: "iter r n x y ⟹ star' r x y"
  oops 

(* Demostración automática del lema *) 
lemma "iter r n x y ⟹ star' r x y"
  oops 

(* Demostración aplicativa *)
lemma "(∃n. iter r n x y) ⟹ star' r x y"
  oops 

(* Demostración automática *)
lemma "(∃n. iter r n x y) ⟹ star' r x y"
  oops 

(* Demostración declarativa *)
lemma assumes "(∃n. iter r n x y)"
      shows "star' r x y"
  oops 

end