Mjoseh: Protegió «R15» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-05-28T06:58:39Z

Protegió «R15» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R15: Definiciones inductivas: clausuras › theory R15 imports Main begin section ‹ La clausura reflexiva transitiva › text…»

2020-05-28T06:58:20Z

Página creada con «<source lang = "isabelle"> chapter ‹ R15: Definiciones inductivas: clausuras › theory R15 imports Main begin section ‹ La clausura reflexiva transitiva › text…»

Página nueva

<source lang = "isabelle">
chapter ‹ R15: Definiciones inductivas: clausuras ›

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

― ‹La demostración automática es›
lemma "⟦(x,y) ∈ r*; (y,z) ∈ r*⟧ ⟹ (x,z) ∈ r*"
oops

― ‹La demostración declarativa es ›
lemma assumes "(x,y) ∈ r*" and
"(y,z) ∈ r*"
shows "(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

― ‹ Demostración declarativa ›
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*.›

― ‹Demostración aplicativa ›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
oops

― ‹Demostración automática›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
oops

― ‹Demostración declarativa ›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
oops

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

― ‹Demostración aplicativa ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
oops

― ‹Demostración automática ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
oops

― ‹Demostración declarativa ›
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 automática ›
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

</source>

← Revisión anterior	Revisión del 06:58 28 may 2020
(Sin diferencias)

R15 - Historial de revisiones

Mjoseh: Protegió «R15» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R15: Definiciones inductivas: clausuras › theory R15 imports Main begin section ‹ La clausura reflexiva transitiva › text…»