Rel 15 (sol)

chapter ‹ R15: Definiciones inductivas: clausuras ›

theory R15_sol
imports Main
begin

section ‹ La clausura reflexiva transitiva ›

text ‹
  · Las definiciones inductivas aceptan parámetros; por tanto, permiten
    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*"
  by (rule crt_refl)

text ‹
  Lema. La relación r* contiene a r.
›

― ‹La demostración aplicativa es ›
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"  
  apply (erule crt_paso)
    (* (y, y) ∈ r**)
  apply (rule crt_refl)
    (* *)
  done

― ‹La demostración automática es›
lemma r_contenida_clausura [intro]: 
  "(x,y) ∈ r ⟹ (x,y) ∈ r*"
  by (simp add: crt_paso) 
(* by (auto intro: crt_paso) *)
    
― ‹La demostración declarativa es› 
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"  
proof -
  assume 1: "(x, y) ∈ r"
  have  2: "(y, y) ∈ r*" by simp
  show "(x,y) ∈ r*" using 1 2 by (rule crt_paso)
  qed
  
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*"
  apply (induction rule:crt.induct)
    (* 1. ⋀x. (x, z) ∈ r* ⟹ (x, z) ∈ r*
       2. ⋀x y za. ⟦(x, y) ∈ r; (y, za) ∈ r*;
                    (za, z) ∈ r* ⟹ (y, z) ∈ r*;
                    (za, z) ∈ r*⟧
                   ⟹ (x, z) ∈ r* *)
  apply simp
    (* 1. ⋀x y za. ⟦(x, y) ∈ r; (y, za) ∈ r*;
                    (za, z) ∈ r* ⟹ (y, z) ∈ r*;
                    (za, z) ∈ r*⟧
                   ⟹ (x, z) ∈ r**)
  apply (simp add: crt_paso)
    (* *)
  done

lemma "⟦ (x,y) ∈ r*; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"
  by (induction rule: crt.induct)
     (simp_all add: crt_paso)

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*"
  apply (induction rule: crt.induct)
     (* 1. ⋀x. (x, z) ∈ r* ⟶ (x, z) ∈ r*
        2. ⋀x y za. ⟦(x, y) ∈ r; 
                     (y, za) ∈ r*;
                     (za, z) ∈ r* ⟶ (y, z) ∈ r*⟧
                    ⟹ (za, z) ∈ r* ⟶ (x, z) ∈ r* *)
   apply simp
     (* ⋀x y za. ⟦(x, y) ∈ r; 
                  (y, za) ∈ r*;
                  (za, z) ∈ r* ⟶ (y, z) ∈ r*⟧
                 ⟹ (za, z) ∈ r* ⟶ (x, z) ∈ r* *)
  apply (rule impI)
     (* ⋀x y za. ⟦(x, y) ∈ r; 
                  (y, za) ∈ r*;
                  (za, z) ∈ r* ⟶ (y, z) ∈ r*;
                  (za, z) ∈ r*⟧
                 ⟹ (za, z) ∈ r* ⟶ (x, z) ∈ r* *)
  apply (drule mp)
     (* 1. ⋀x y za. ⟦(x, y) ∈ r; (y, za) ∈ r*; (za, z) ∈ r*⟧
                    ⟹ (za, z) ∈ r*
        2. ⋀x y za. ⟦(x, y) ∈ r; 
                     (y, za) ∈ r*; 
                     (za, z) ∈ r*;
                     (y, z) ∈ r*⟧
                    ⟹ (x, z) ∈ r* *)
   apply assumption
     (* ⋀x y za. ⟦(x, y) ∈ r; 
                  (y, za) ∈ r*; 
                  (za, z) ∈ r*;
                  (y, z) ∈ r*⟧
                 ⟹ (x, z) ∈ r* *)
  apply (erule crt_paso)
     (* ⋀x y za. ⟦(y, za) ∈ r*; (za, z) ∈ r*; (y, z) ∈ r*⟧
                 ⟹ (y, z) ∈ r**)
  apply assumption
     (* *)
  done

― ‹La demostración automática es›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
  by (induction rule:crt.induct)
     (auto simp add: crt_paso)

― ‹La demostración declarativa es›
lemma crt_trans [rule_format]:
  "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
proof (induction rule:crt.induct)
  show "⋀x. (x,z) ∈ r* ⟶ (x,z) ∈ r*" by simp
next
  fix x y u
  assume H1: "(x,y) ∈ r" and
         H2: "(y,u) ∈ r*" and
         H3: "(u,z) ∈ r* ⟶ (y,z) ∈ r*"
  show "(u,z) ∈ r* ⟶ (x,z) ∈ r*"
  proof
    assume "(u,z) ∈ r*"
    with H3 have "(y,z) ∈ r*" ..
    with H1 show "(x,z) ∈ r*" by (rule crt_paso) 
  qed
qed

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*.
›

― ‹Demostración aplicativa›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
  apply (induction rule: crt2.induct)
      (*  1. ⋀x y. (x, y) ∈ r ⟹ (x, y) ∈ r*
          2. ⋀x. (x, x) ∈ r*
          3. ⋀x y z. ⟦(x, y) ∈ crt2 r; (x, y) ∈ r*;
                      (y, z) ∈ crt2 r; (y, z) ∈ r*⟧
                     ⟹ (x, z) ∈ r* *)
    apply (erule r_contenida_clausura)
      (* 1. ⋀x. (x, x) ∈ r*
         2. ⋀x y z. ⟦(x, y) ∈ crt2 r; (x, y) ∈ r*;
                     (y, z) ∈ crt2 r; (y, z) ∈ r*⟧
                    ⟹ (x, z) ∈ r* *)
   apply simp
      (* ⋀x y z. ⟦(x, y) ∈ crt2 r; (x, y) ∈ r*;
                  (y, z) ∈ crt2 r; (y, z) ∈ r*⟧
                 ⟹ (x, z) ∈ r* *)
  apply (erule crt_trans)
      (* ⋀x y z. ⟦(x, y) ∈ crt2 r; (y, z) ∈ crt2 r; (y, z) ∈ r*⟧
                 ⟹ (y, z) ∈ r* *)
  apply assumption
      (* *)
  done

― ‹ La demostración automática es ›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
  by (induction rule: crt2.induct)
     (auto simp add: r_contenida_clausura 
                     crt_trans)

― ‹ La demostración declarativa es ›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
proof (induction rule: crt2.induct)
  fix x y
  assume "(x,y) ∈ r"
  then show "(x,y) ∈ r*" by (rule r_contenida_clausura) 
next
  fix x
  show "(x,x) ∈ r*" by (rule crt_refl)
next
  fix x y z
  assume H1: "(x,y) ∈ crt2 r" and
         H2: "(x,y) ∈ r*"     and
         H3: "(y,z) ∈ crt2 r" and 
         H4: "(y,z) ∈ r*"
  show "(x,z) ∈ r*" using H2 H4 by (rule crt_trans)
qed

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

― ‹ La demostración aplicativa es ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
  apply (induction rule: crt.induct)
     (* 1. ⋀x. (x, x) ∈ crt2 r
        2. ⋀x y z. ⟦(x, y) ∈ r; (y, z) ∈ r*; (y, z) ∈ crt2 r⟧
                   ⟹ (x, z) ∈ crt2 r *)
   apply (rule crt2.intros(2))
     (* ⋀x y z. ⟦(x, y) ∈ r; (y, z) ∈ r*; (y, z) ∈ crt2 r⟧
                ⟹ (x, z) ∈ crt2 r *)
  apply (drule crt2.intros(1))
     (* ⋀x y z. ⟦(y, z) ∈ r*; (y, z) ∈ crt2 r; (x, y) ∈ crt2 r⟧
                ⟹ (x, z) ∈ crt2 r *)
  apply (drule_tac x=x and z=z in crt2.intros(3))
     (* 1. ⋀x y z. ⟦(y, z) ∈ r*; (y, z) ∈ crt2 r⟧
                   ⟹ (y, z) ∈ crt2 r
        2. ⋀x y z. ⟦(y, z) ∈ r*; (y, z) ∈ crt2 r; (x, z) ∈ crt2 r⟧
                   ⟹ (x, z) ∈ crt2 r *)
   apply assumption+
     (* *)
  done

― ‹ La demostración automática es ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
  by (induction rule: crt.induct)
     (auto intro: crt2.intros)

― ‹ La demostración declarativa es ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
proof (induction rule:crt.induct)
  fix x
  show "(x,x) ∈ crt2 r" by (rule crt2.intros(2))
next
  fix x y z
  assume H1: "(x,y) ∈ r" and 
         H2: "(y,z) ∈ r*" and 
         H3: "(y,z) ∈ crt2 r"
  have "(x,y) ∈ crt2 r" using H1 by (rule crt2.intros(1))
  then show "(x,z) ∈ crt2 r" using H3 by (rule crt2.intros(3))
qed


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*"
  apply (induction rule: crt.induct)
     (* 1. ⋀x. (x, z) ∈ r ⟶ (x, z) ∈ r*
        2. ⋀x y za. ⟦(x, y) ∈ r; 
                     (y, za) ∈ r*; 
                     (za, z) ∈ r ⟶ (y, z) ∈ r*⟧
                    ⟹ (za, z) ∈ r ⟶ (x, z) ∈ r* *)
   apply (simp add: r_contenida_clausura)
     (* ⋀x y za. ⟦(x, y) ∈ r; 
                  (y, za) ∈ r*; 
                  (za, z) ∈ r ⟶ (y, z) ∈ r*⟧
                 ⟹ (za, z) ∈ r ⟶ (x, z) ∈ r* *)
  apply (simp add: crt_paso)
  done

― ‹ Demostración automática ›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
  by (induction rule: crt.induct)
     (auto simp add: r_contenida_clausura
                     crt_paso)

― ‹ Demostración declarativa ›
lemma crt_paso2 [rule_format]: 
  "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
proof (induction rule: crt.induct)
  fix x
  show "(x,z) ∈ r ⟶ (x,z) ∈ r*" by (simp add: r_contenida_clausura)
next
  fix x y u
  assume H1: "(x,y) ∈ r" and 
         H2: "(y,u) ∈ r*" and 
         H3: "(u,z) ∈ r ⟶ (y,z) ∈ r*"
  show "(u,z) ∈ r ⟶ (x,z) ∈ r*"
  proof
    assume "(u,z) ∈ r"
    with H3 have "(y,z) ∈ r*" by (rule mp)
    with H1 show "(x,z) ∈ r*" by (rule crt_paso)
  qed
qed

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"
  by (simp add: refl')

― ‹ Demostración aplicativa de r contenida en (star' r) ›
lemma "r x y ⟹ star' r x y"
  apply (rule_tac y=x in step')
     (* 1. r x y ⟹ star' r x x
        2. r x y ⟹ r x y *)
   apply (rule refl')
     (* r x y ⟹ r x y *)
  apply assumption
     (* *)
  done

― ‹ Demostración automática de r contenida en (star' r) ›
lemma "r x y ⟹ star' r x y"
  by (meson refl' step')

lemma rsubsetStar'_b: "r x y ⟹ star' r x y"
by (simp add:step'[OF refl'[of r x]])
    
    
― ‹ Demostración declarativa de r contenida en (star' r) ›
lemma rsubsetStar': "r x y ⟹ star' r x y"
proof -
  assume 1:"r x y"
  have 2: "star' r x x" by (simp add: refl')
  show "star' r x y" using 2 1 by (simp add: step')
qed

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"
  apply (induct rule: star'.induct)
    (* 1. ⋀xa. r x xa ⟹ star' r x xa
       2. ⋀xa y z. ⟦star' r xa y; r x xa ⟹ star' r x y; r y z; r x xa⟧
                   ⟹ star' r x z *)
  apply (simp add: rsubsetStar')
    (* ⋀xa y z. ⟦star' r xa y; r x xa ⟹ star' r x y; r y z; r x xa⟧
                ⟹ star' r x z *)
  apply (simp add: step')
    (* *)
  done

― ‹ Demostración automática ›
lemma star'_subset_star'_l1:
  "⟦star' r y z; r x y⟧ ⟹ star' r x z"
  by (induct rule: star'.induct)
     (auto simp add: rsubsetStar' step')

― ‹ Demostraciones de que  (star' r) es transitiva ›

― ‹ Demostración aplicativa ›
lemma "⟦star' r x y; star' r y z⟧ ⟹ star' r x z"   
  apply  (induction rule: star'.induct)
     (* 1. ⋀x. star' r x z ⟹ star' r x z
        2. ⋀x y za. ⟦star' r x y; star' r y z ⟹ star' r x z; r y za;
                     star' r za z⟧
                    ⟹ star' r x z *)
   apply simp
     (* ⋀x y za. ⟦star' r x y; star' r y z ⟹ star' r x z; r y za;
                     star' r za z⟧
                    ⟹ star' r x z *)
  apply (simp add: star'_subset_star'_l1)
     (* *)
  done

― ‹ Demostración automática ›
lemma star'Trans: 
  "⟦star' r x y; star' r y z⟧ ⟹ star' r x z"
  by (induction rule: star'.induct) 
      (auto simp add: star'_subset_star'_l1)
   
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)"
  apply (induct rule: star'.induct)
     (* 1. ⋀x. ∃n. iter r n x x
        2. ⋀x y z. ⟦star' r x y; ∃n. iter r n x y; r y z⟧
                   ⟹ ∃n. iter r n x z *)
   apply (rule_tac x=0 in exI)
     (* 1. ⋀x. iter r 0 x x
        2. ⋀x y z. ⟦star' r x y; ∃n. iter r n x y; r y z⟧
                   ⟹ ∃n. iter r n x z *)
   apply (rule iterRefl)
     (* ⋀x y z. ⟦star' r x y; ∃n. iter r n x y; r y z⟧
                ⟹ ∃n. iter r n x z *)
  apply (erule exE)
     (* ⋀x y z n. ⟦star' r x y; r y z; iter r n x y⟧
                  ⟹ ∃n. iter r n x z *)
  apply (rule_tac x="n+1" in exI)
     (* ⋀x y z n. ⟦star' r x y; r y z; iter r n x y⟧
                  ⟹ iter r (n + 1) x z *)
  apply (erule iterStep)
     (*  ⋀x y z n. ⟦star' r x y; r y z⟧ ⟹ r y z *)
  apply assumption
     (* *)
  done

― ‹ Demostración automática ›
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"    
  by (induct rule: star'.induct)
     (auto intro: iterRefl iterStep)

― ‹ Demostración declarativa ›
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"    
proof (induct rule: star'.induct)
  fix x 
  have "iter r 0 x x" by (rule iterRefl)
  then show "∃n. iter r n x x" by (rule exI)
next
  fix x y z
  assume 1: "star' r x y" and
         2: "∃n. iter r n x y" and
         3: "r y z"
  from 2 obtain m where  "iter r m x y" by (rule exE)      
  then have  "iter r (m+1) x z" using 3 by (rule iterStep)
  then show "∃n. iter r n x z" by (rule exI)
  qed
  
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"
  apply (induct rule: iter.induct)
     (* 1. ⋀x. star' r x x
        2. ⋀n x y z. ⟦iter r n x y; star' r x y; r y z⟧
                     ⟹ star' r x z *)
   apply (rule refl')
     (* ⋀n x y z. ⟦iter r n x y; star' r x y; r y z⟧
                  ⟹ star' r x z *)
  apply (erule step')
     (* ⋀n x y z. ⟦iter r n x y; r y z⟧ ⟹ r y z*)
  apply assumption
  done

― ‹ Demostración automática del lema ›
lemma "iter r n x y ⟹ star' r x y"
  by (induct rule: iter.induct)
     (auto simp add: refl' step')

― ‹ Demostración aplicativa ›
lemma "(∃n. iter r n x y) ⟹ star' r x y"
  apply (erule exE)
    (* ⋀n. iter r n x y ⟹ star' r x y *)
  apply (erule iter_star'_subset)
    (* *)
  done

― ‹ Demostración automática ›
lemma "(∃n. iter r n x y) ⟹ star' r x y"
  by (auto simp add: iter_star'_subset)

― ‹ Demostración declarativa ›
lemma assumes "(∃n. iter r n x y)"
      shows "star' r x y"
proof -
  have  "∃n. iter r n x y" using assms .
  then obtain k where "iter r k x y" by (rule exE)
  then show "star' r x y" by (rule iter_star'_subset)
qed

end