Sol 13
De Lógica matemática y fundamentos (2018-19)
Revisión del 18:02 26 jun 2019 de Mjoseh (discusión | contribuciones)
chapter {* R13: Definiciones inductivas: clausuras *}
theory R13_sol
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*"
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*.
*}
(* La demostración aplicativa es *)
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) (* blast*)
next
fix x
show "(x,x) ∈ r*" by simp
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 aplicativa *)
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*" ..
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 vondició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" ..
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" ..
then have "iter r (m+1) x z" using 3 by (rule iterStep)
then show "∃n. iter r n x z" ..
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" ..
then show "star' r x y" by (rule iter_star'_subset)
qed
end