Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

header {* T14: Razonamiento modular (II) *}

theory T14
imports Main
begin

section {* Contextos simples *}

text {*
  La forma más simple de un contexto local es una declaración de 
  parámetros, junto con las propiedades que verifican.

  Por ejemplo, una relación le es un orden parcial si es reflexiva, 
  antisimétrica y  transitiva. (Usamos el símbolo  ⊑ para representar 
  la relación binaria le). *}

locale partial_order =
    fixes le :: "'a ⇒ 'a ⇒ bool" (infixl "⊑" 50)
    assumes refl [intro, simp]: "x ⊑ x"
      and anti_sym [intro]: "⟦ x ⊑ y; y ⊑ x ⟧ ⟹ x = y"
      and trans [trans]: "⟦ x ⊑ y; y ⊑ z ⟧ ⟹ x ⊑ z"

text (in partial_order) {* 
  En Isabelle las variables libres etán cuantificadas universalmente; es 
  decir,
     "⟦ x ⊑ y; y ⊑ z ⟧ ⟹ x ⊑ z" 
  significa
     "⋀x y z. ⟦ x ⊑ y; y ⊑ z ⟧ ⟹ x ⊑ z".

  Para conocer los detalles disponemos de los comandos:
  * print_locales: proporciona una lista con los contextos locales 
    de la teoría,
  * print_locale o print_locale!, que porporcionan una lista con los
    elementos del contexto local. *}
  
print_locale! partial_order

text{* El contexto local ha introducido el predicado (local) 
  ❙partial_order en la teoría. Su definición se puede ver mediante
    thm partial_order_def, 
  así como sus propiedades.
*}

thm partial_order_def
thm partial_order.trans

text {* Ampliación de contextos locales: definiciones dentro
  de un contexto. *}

text{* Definición de orden estricto *}

definition (in partial_order)
    less :: "'a ⇒ 'a ⇒ bool" (infixl "⊏" 50)
    where "(x ⊏ y) = (x ⊑ y ∧ x ≠ y)"

text {* La definción de less es accesible en el contexto local.
  Para inspeccionarla, se usa
     thm partial_order.less_def, 
  que muestra lo siguiente:
     partial_order ?le ⟹ 
        partial_order.less ?le ?x ?y = (?le ?x ?y ∧ ?x ≠ ?y) *}

thm partial_order.less_def

text {* En un contexto local, las propiedades de la especificación 
  se pueden usar como teoremas. Por ejemplo, en la prueba de la
  transitividad de  ⊏, a partir de la transitividad de ⊑. *}

lemma (in partial_order) less_le_trans [trans]:
  "⟦ x ⊏ y; y ⊏ z ⟧ ⟹ x ⊏ z"    
  unfolding less_def by  (blast intro: trans)

text {* Cuando trabajamos con entornos locales es frecuente 
 una sucesión de definiciones y teoremas con la misma etiqueta. 
 Se puede simplificar la notación estableciendo un principio y
 un final dentro del cual se tiene la especificación del contexto. *}

context partial_order
  begin

text {* Definiciones de las relaciones is_inf e is_sup, en el contexto 
  de orden parcial: *}

definition
  is_inf where "is_inf x y i =
    (i ⊑ x ∧ i ⊑ y ∧ (∀z. z ⊑ x ∧ z ⊑ y ⟶ z ⊑ i))"

definition
  is_sup where "is_sup x y s =
    (x ⊑ s ∧ y ⊑ s ∧ (∀z. x ⊑ z ∧ y ⊑ z ⟶ s ⊑ z))"

text {* Propiedades: *}

text{* Regla de introducción del ínfimo: *}
lemma is_infI [intro]: "i ⊑ x ⟹ 
                        i ⊑ y ⟹
                        (⋀z. ⟦z ⊑ x; z ⊑ y⟧ ⟹ z ⊑ i) ⟹ 
                        is_inf x y i"
by (unfold is_inf_def) blast

text{* Regla de eliminación del ínfimo: *}
lemma is_inf_lower [elim]:
  "is_inf x y i ⟹ (i ⊑ x ⟹ i ⊑ y ⟹ C) ⟹ C"
by (unfold is_inf_def) blast

text{* El ínfimo es la mayor de las cotas inferiores: *}
lemma is_inf_greatest [elim]:
  "is_inf x y i ⟹ z ⊑ x ⟹ z ⊑ y ⟹ z ⊑ i"
by (unfold is_inf_def) blast

text{* Unicidad del ínfimo: *}

theorem is_inf_uniq: 
  "⟦is_inf x y i; is_inf x y i'⟧ ⟹ i = i'"
by (metis anti_sym is_inf_def)

theorem is_inf_uniq_d: 
  "⟦is_inf x y i; is_inf x y i'⟧ ⟹ i = i'"
proof -
  assume inf: "is_inf x y i"
  assume inf': "is_inf x y i'"
  show ?thesis
  proof (rule anti_sym)
    from inf' show "i ⊑ i'"
    proof (rule is_inf_greatest)
      from inf show "i ⊑ x" ..
      from inf show "i ⊑ y" ..
    qed
    from inf show "i' ⊑ i"
    proof (rule is_inf_greatest)
      from inf' show "i' ⊑ x" ..
      from inf' show "i' ⊑ y" ..
    qed
  qed
qed

text{* Si  "x ⊑ y, x es el ínfimo de x, y. *}
theorem is_inf_related [elim]: 
  "x ⊑ y ⟹ is_inf x y x"
by (metis is_infI local.refl)
 
theorem is_inf_related_d: 
  "x ⊑ y ⟹ is_inf x y x" 
proof -
  assume "x ⊑ y"
  show ?thesis
  proof
    show "x ⊑ x" ..
    show "x ⊑ y" by fact
    fix z assume "z ⊑ x" and "z ⊑ y" show "z ⊑ x" by fact
  qed
qed

text {* Análogamente para el supremo.*}

lemma is_supI [intro]: "x ⊑ s ⟹ 
                        y ⊑ s ⟹
                        (⋀z. x ⊑ z ⟹ y ⊑ z ⟹ s ⊑ z) ⟹ 
                        is_sup x y s"
by (unfold is_sup_def) blast

lemma is_sup_least [elim]:
  "is_sup x y s ⟹ x ⊑ z ⟹ y ⊑ z ⟹ s ⊑ z"
by (unfold is_sup_def) blast

lemma is_sup_upper [elim]:
  "is_sup x y s ⟹ (x ⊑ s ⟹ y ⊑ s ⟹ C) ⟹ C"
by (unfold is_sup_def) blast

theorem is_sup_uniq: 
  "⟦is_sup x y s; is_sup x y s'⟧ ⟹ s = s'"
by (metis anti_sym is_sup_def)

theorem is_sup_uniq_d: "⟦is_sup x y s; is_sup x y s'⟧ ⟹ s = s'"
proof (rule anti_sym)
  assume sup: "is_sup x y s"
  assume sup': "is_sup x y s'"
  from sup  show "s ⊑ s'"
  proof (rule is_sup_least)
    from sup' show "x ⊑ s'" ..
    from sup' show "y ⊑ s'" ..
  qed
  from sup' show "s' ⊑ s"
  proof (rule is_sup_least)
    from sup show "x ⊑ s" ..
    from sup show "y ⊑ s" ..
  qed
qed

theorem is_sup_related [elim]: 
  "x ⊑ y ⟹ is_sup x y y"
by (metis is_supI local.refl)

theorem is_sup_related_d [elim]: "x ⊑ y ⟹ is_sup x y y"
proof -
  assume "x ⊑ y"
  show ?thesis
  proof
    show "x ⊑ y" by fact
    show "y ⊑ y" ..
    fix z assume "x ⊑ z" and "y ⊑ z"
    show "y ⊑ z" by fact
  qed
qed

text {* Finalización del contexto con end *}
  end

text {* Importación de contextos locales:
  En general, las estructuras algebraicas se construyen de forma 
  incremental, añadiendo operaciones y propiedades a estructuras
  ya existentes. Por ejemplo, la estructura de orden parcial se 
  puede extender a órdenes totales y a retículos. Y, a su vez,
  los retículos se pueden extender a retículos distributivos. 

  En lo que sigue, vemos ejemplos de cómo se importa y se 
  extiende un contexto local en Isabelle. *}

text {* Un retículo es uo orden parcial con ínfimo y supremo. *}
locale lattice = partial_order +
  assumes ex_inf: "∃inf. is_inf x y inf"
      and ex_sup: "∃sup. is_sup x y sup"
begin

text {* Observar que los predicados is_inf e is_sup están 
  definidos para un orden parcial. Ahora definimos las 
  funciones ínfimo (meet) y supremo (join) en un retículo.  *}

definition
    meet (infixl "⊓" 70) where "x ⊓ y = (THE inf. is_inf x y inf)"
definition
    join (infixl "⊔" 65) where "x ⊔ y = (THE sup. is_sup x y sup)"

thm the_def
thm the_equality
thm theI

text {* Propiedades: *}

text {* Regla de eliminación: si i es el ínfimo de x,y,  entonces es  
  x ⊓ y.  *}

lemma meet_equality [elim]: "is_inf x y i ⟹ x ⊓ y = i"
proof (unfold meet_def)
  assume "is_inf x y i"
  then show "(THE i. is_inf x y i) = i"
    by (rule the_equality) 
       (rule is_inf_uniq [OF _ `is_inf x y i`])
qed

text {* Regla de introducción: si i verifica las condiciones del ínfimo 
  de x,y, entonces es  x ⊓ y. *}
lemma meetI [intro]:
  "i ⊑ x ⟹ 
   i ⊑ y ⟹ 
   (⋀z. z ⊑ x ⟹ z ⊑ y ⟹ z ⊑ i)  ⟹  
   x ⊓ y = i"
by (auto simp add: meet_equality is_infI)

text {* Otras formas de escribir la prueba:

apply (rule meet_equality)
apply (rule is_infI)
apply blast+
 
by (rule meet_equality, rule is_infI) blast+ *}

text {* Regla de introducción: x ⊓ y es el ínfimo de x, y. *}
lemma is_inf_meet [intro]: "is_inf x y (x ⊓ y)"
proof (unfold meet_def)
  from ex_inf obtain i where "is_inf x y i" ..
  then show "is_inf x y (THE i. is_inf x y i)"
    by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`])
qed

text {* Propiedades x ⊓ y ⊑ x, x ⊓ y ⊑ y *}

lemma meet_left [intro]: "x ⊓ y ⊑ x"
apply (rule is_inf_lower)
apply (rule is_inf_meet)
apply auto
done

(* by (rule is_inf_lower) (rule is_inf_meet) *)

lemma meet_right [intro]:
  "x ⊓ y ⊑ y"
by (rule is_inf_lower) (rule is_inf_meet)

text {* Si z es una cota inferior de x e y, entonces  z es menor o igual 
  que el ínfimo de x e y. *}
lemma meet_le [intro]:
  "⟦ z ⊑ x; z ⊑ y ⟧ ⟹ z ⊑ x ⊓ y"
by (rule is_inf_greatest) (rule is_inf_meet)

text{* Análogamente para el supremo *}

lemma join_equality [elim]: "is_sup x y s ⟹ x ⊔ y = s"
proof (unfold join_def)
  assume "is_sup x y s"
  then show "(THE s. is_sup x y s) = s"
    by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`])
qed

lemma joinI [intro]: 
  "x ⊑ s ⟹ 
   y ⊑ s ⟹
   (⋀z. x ⊑ z ⟹ y ⊑ z ⟹ s ⊑ z) ⟹ 
   x ⊔ y = s"
by (rule join_equality, rule is_supI) blast+

lemma is_sup_join [intro]: "is_sup x y (x ⊔ y)"
proof (unfold join_def)
  from ex_sup obtain s where "is_sup x y s" ..
  then show "is_sup x y (THE s. is_sup x y s)"
    by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`])
qed

lemma join_left [intro]: "x ⊑ x ⊔ y"
by (rule is_sup_upper) (rule is_sup_join)

lemma join_right [intro]: "y ⊑ x ⊔ y"
by (rule is_sup_upper) (rule is_sup_join)

lemma join_le [intro]:
  "⟦ x ⊑ z; y ⊑ z ⟧ ⟹ x ⊔ y ⊑ z"
by (rule is_sup_least) (rule is_sup_join)

text {* Asociatividad del ínfimo *}

theorem meet_assoc: "(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)"
proof (rule meetI)
   show "x ⊓ (y ⊓ z) ⊑ x ⊓ y"
   proof
     show "x ⊓ (y ⊓ z) ⊑ x" ..
     show "x ⊓ (y ⊓ z) ⊑ y"
     proof -
       have "x ⊓ (y ⊓ z) ⊑ y ⊓ z" ..
       also have "… ⊑ y" ..
       finally show ?thesis .
     qed
   qed
   show "x ⊓ (y ⊓ z) ⊑ z"
   proof -
     have "x ⊓ (y ⊓ z) ⊑ y ⊓ z" ..
     also have "… ⊑ z" ..
     finally show ?thesis .
   qed
   fix w assume "w ⊑ x ⊓ y" and "w ⊑ z"
   show "w ⊑ x ⊓ (y ⊓ z)"
   proof
     show "w ⊑ x"
     proof -
       have "w ⊑ x ⊓ y" by fact
       also have "… ⊑ x" ..
       finally show ?thesis .
     qed
     show "w ⊑ y ⊓ z"
     proof
       show "w ⊑ y"
       proof -
         have "w ⊑ x ⊓ y" by fact
         also have "… ⊑ y" ..
         finally show ?thesis .
       qed
       show "w ⊑ z" by fact
     qed
   qed
qed

text {* Commutatividad del ínfimo *}

theorem meet_commute_auto: "x ⊓ y = y ⊓ x"
by auto

theorem meet_commute: "x ⊓ y = y ⊓ x"
proof (rule meetI)
  show "y ⊓ x ⊑ x" ..
  show "y ⊓ x ⊑ y" ..
  fix z assume "z ⊑ y" and "z ⊑ x"
  then show "z ⊑ y ⊓ x" ..
qed

text{* Ley de absorción *}

theorem meet_join_absorb_auto: "x ⊓ (x ⊔ y) = x"
by blast

theorem meet_join_absorb: "x ⊓ (x ⊔ y) = x"
proof (rule meetI)
  show "x ⊑ x" ..
  show "x ⊑ x ⊔ y" ..
  fix z assume "z ⊑ x" and "z ⊑ x ⊔ y"
  show "z ⊑ x" by fact
qed

text {* Análogamente para el supremo *}

theorem join_assoc: "(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)"
proof (rule joinI)
  show "x ⊔ y ⊑ x ⊔ (y ⊔ z)"
  proof
    show "x ⊑ x ⊔ (y ⊔ z)" ..
    show "y ⊑ x ⊔ (y ⊔ z)"
    proof -
      have "y ⊑ y ⊔ z" ..
      also have "... ⊑ x ⊔ (y ⊔ z)" ..
      finally show ?thesis .
    qed
  qed
  show "z ⊑ x ⊔ (y ⊔ z)"
  proof -
    have "z ⊑ y ⊔ z"  ..
    also have "... ⊑ x ⊔ (y ⊔ z)" ..
    finally show ?thesis .
  qed
  fix w assume "x ⊔ y ⊑ w" and "z ⊑ w"
  show "x ⊔ (y ⊔ z) ⊑ w"
  proof
    show "x ⊑ w"
    proof -
      have "x ⊑ x ⊔ y" ..
      also have "… ⊑ w" by fact
      finally show ?thesis .
    qed
    show "y ⊔ z ⊑ w"
    proof
      show "y ⊑ w"
      proof -
        have "y ⊑ x ⊔ y" ..
        also have "... ⊑ w" by fact
        finally show ?thesis .
      qed
      show "z ⊑ w" by fact
    qed
  qed
qed

theorem join_commute_auto: "x ⊔ y = y ⊔ x"
by blast

theorem join_commute: "x ⊔ y = y ⊔ x"
proof (rule joinI)
  show "x ⊑ y ⊔ x" ..
  show "y ⊑ y ⊔ x" ..
  fix z assume "y ⊑ z" and "x ⊑ z"
  then show "y ⊔ x ⊑ z" ..
qed

theorem join_meet_absorb_auto: "x ⊔ (x ⊓ y) = x"
by blast

theorem join_meet_absorb: "x ⊔ (x ⊓ y) = x"
proof (rule joinI)
  show "x ⊑ x" ..
  show "x ⊓ y ⊑ x" ..
  fix z assume "x ⊑ z" and "x ⊓ y ⊑ z"
  show "x ⊑ z" by fact
qed

text {* Idempotencia del ínfimo *}

theorem meet_idem_auto: "x ⊓ x = x"
by auto

theorem meet_idem: "x ⊓ x = x"
proof -
  have "x ⊓ (x ⊔ (x ⊓ x)) = x" by (rule meet_join_absorb)
  also have "x ⊔ (x ⊓ x) = x" by (rule join_meet_absorb)
  finally show ?thesis .
qed

text {* Si x es menor o igual que y, el ínfimo de x, y es x *}

theorem meet_related_auto [elim]: "x ⊑ y ⟹ x ⊓ y = x"
by blast

theorem meet_related [elim]: "x ⊑ y ⟹ x ⊓ y = x"
proof (rule meetI)
  assume "x ⊑ y"
  show "x ⊑ x" ..
  show "x ⊑ y" by fact
  fix z assume "z ⊑ x" and "z ⊑ y"
  show "z ⊑ x" by fact
qed

theorem meet_related2 [elim]: "y ⊑ x ⟹ x ⊓ y = y"
apply (drule meet_related)
apply (simp add:meet_commute)
done

(* by (drule meet_related) (simp add: meet_commute) *)

text {* Si x es menor o igual que y, el supremo de x, y es y *}

theorem join_related_auto [elim]: "x ⊑ y ⟹ x ⊔ y = y"
by blast

theorem join_related [elim]: "x ⊑ y ⟹ x ⊔ y = y"
proof (rule joinI)
  assume "x ⊑ y"
  show "y ⊑ y" ..
  show "x ⊑ y" by fact
  fix z assume "x ⊑ z" and "y ⊑ z"
  show "y ⊑ z" by fact
qed

theorem join_related2 [elim]: "y ⊑ x ⟹ x ⊔ y = x"
    by (drule join_related) (simp add: join_commute)

text {* x es menor o igual que y syss el ínfimo de x, y es x *}

theorem meet_connection: "(x ⊑ y) = (x ⊓ y = x)"
proof
  assume "x ⊑ y"
  then have "is_inf x y x" ..
  then show "x ⊓ y = x" ..
next
  have "x ⊓ y ⊑ y" ..
  also assume "x ⊓ y = x"
  finally show "x ⊑ y" .
qed

theorem meet_connection2: 
  "(x ⊑ y) = (y ⊓ x = x)"
using meet_commute meet_connection by simp

text {* x es menor o igual que y syys el supremo de x, y es y *}

theorem join_connection: "(x ⊑ y) = (x ⊔ y = y)"
proof
  assume "x ⊑ y"
  then have "is_sup x y y" ..
  then show "x ⊔ y = y" ..
next
  have "x ⊑ x ⊔ y" ..
  also assume "x ⊔ y = y"
  finally show "x ⊑ y" .
qed

theorem join_connection2: 
  "(x ⊑ y) = (x ⊔ y = y)"
using join_commute join_connection by simp

text {* Agrupamos lemas bajo un nombre común:
  L1: commutatividad del ínfimo y el supremo
  L2: asociatividad del ínfimo y el supremo
  L3: leyes de absorción *}

lemmas  L1 = join_commute meet_commute
lemmas  L2 = join_assoc meet_assoc
lemmas  L3 = join_meet_absorb meet_join_absorb

  end

text {* Un orden total es un orden parcial  ⊑, siendo la relación ⊑ 
  total. *}

locale total_order = partial_order +
    assumes total: "x ⊑ y ∨ y ⊑ x"

lemma (in total_order) less_total: 
  "x ⊏ y ∨ x = y ∨ y ⊏ x"
using total by (unfold less_def) blast

text {* Un retículo distributivo es un retículo que verifica la 
  propiedad "x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z".
*}
locale distrib_lattice = lattice +
  assumes meet_distr: "x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z"

text{* En un retículo distributivo, también se verifica la  propiedad 
  distributiva dual: "x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)" *}

lemma (in distrib_lattice) join_distr:
  "x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"  (* prueba en Jacobson I, pg. 462 *)
proof -
  have "x ⊔ (y ⊓ z) = (x ⊔ (x ⊓ z)) ⊔ (y ⊓ z)" by (simp add: L3)
  also have "... = x ⊔ ((x ⊓ z) ⊔ (y ⊓ z))" by (simp add: L2)
  also have "... = x ⊔ ((x ⊔ y) ⊓ z)" by (simp add: L1 meet_distr)
  also have "... = ((x ⊔ y) ⊓ x) ⊔ ((x ⊔ y) ⊓ z)" by (simp add: L1 L3)
  also have "... = (x ⊔ y) ⊓ (x ⊔ z)" by (simp add: meet_distr)
  finally show ?thesis .
qed

text {* Las pruebas sugeridas por Sledgehammer *}

lemma (in distrib_lattice) join_distr_auto:
 "x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"
by (metis join_assoc meet_commute_auto meet_distr meet_join_absorb_auto)

lemma (in distrib_lattice) join_distr_estructurada:
  "x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"
proof -
  have "⋀u v. u ⊔ u ⊓ v = u" by blast
  hence "x ⊔ z ⊓ (x ⊔ y) = x ⊔ y ⊓ z" 
    by (metis join_assoc meet_commute_auto meet_distr)
  thus "x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)" 
    using meet_commute_auto meet_distr meet_join_absorb_auto by fastforce
qed 

text {* La jerarquía establecida por los contextos locales definidos es 
  la siguiente:

                          partial_order
                           /         \
                          /           \
                       lattice    total_order
                          |
                          |
                   distrib_lattice

  Los contextos locales nos permiten probar teoremas que son ciertos
  bajo las hipótesis asumidas en el contexto. Estos teoremas se podrán
  utilizar en otros contextos, en los que se verifiquen las hipótesis 
  anteriores (mediante interpretaciones).

  Una forma simple de interpretación la proporciona el comando sublocal,
  que permite modificar la jerarquía entre los contextos locales 
  definidos.

  Por ejemplo, la jerarquía anterior no refleja que los órdenes totales
  son retículos y, por tanto, las definiciones y teoremas de retículos
  no se tienen para los órdenes locales.

  Mediante 
     sublocale l1 ⊆ l2
  se expresa que que la teoría l2 se puede interpretar en la teoría l1.
  Es decir, que todas las propiedades de l2 son válidas en l1.

  Por ejemplo, haciendo
     sublocale total_order ⊆ lattice
  se genera un objetivo para garantizar que un orden total verifica
  los axiomas de retículo. Este objetivo tiene que probarlo el usuario.
  Luego, las definiciones y teoremas de retículos serán válidos en los 
  órdenes totales. 

  Y tendremos la siguiente jeraquía:

                         partial_order
                               |
                               |
                            lattice    
                           /      \
                          /         \
                distrib_lattice     total_order
  
*}

sublocale total_order ⊆ lattice
proof unfold_locales
  fix x y
  from total have "is_inf x y (if x ⊑ y then x else y)"
    by (auto simp: is_inf_def)
  then show "∃inf. is_inf x y inf" ..
next 
  fix x y
  from total have "is_sup x y (if x ⊑ y then y else x)"
    by (auto simp: is_sup_def)
  then show "∃sup. is_sup x y sup" .. 
qed 

text {* Análogamente, se puede establecer los retículos distributivos 
  son órdenes totales. 

  De esta forma la jerarquía quedaría como sigue:

                        partial_order
                               |
                               |
                            lattice    
                               |
                               |
                        distrib_lattice     
                               |
                               |
                          total_order
 *}

sublocale total_order ⊆ distrib_lattice
proof unfold_locales
 fix x y z
 show "x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z" (is "?l = ?r")
 proof -  (* según Jacobson I, pg. 462 *)
   { assume c: "y ⊑ x" "z ⊑ x"
     from c have "?l = y ⊔ z"
       by (metis c join_connection2 join_related2 meet_related2 total)
     also from c have "... = ?r" by (metis meet_related2)
     finally have "?l = ?r" . }
   moreover
   { assume c: "x ⊑ y ∨ x ⊑ z"
     from c have "?l = x"
       by (metis join_connection2 join_related2 meet_connection total trans)
     also from c have "... = ?r"
       by (metis join_commute join_related2 meet_connection meet_related2 total)
     finally have "?l = ?r" . }
   moreover note total
   ultimately show ?thesis by blast
 qed
qed

text {* La interpretación a través de contextos locales es dinámica. 
  Cuando establecemos 
     sublocale l1  ⊆ l2
  no sólo se añaden las conclusiones de l1 a l2. También se almacena 
  la dependencia y las futuras propiedades que se prueben en l2 se
  propagan de forma automática a l1. Además, la relación establecida
  por sublocale es transitiva. *}

end