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

header {* T15 (c) Interpretaciones locales *}

theory T15c
imports T14
begin

text {* En en ejemplo anterior, para probar el segundo objetivo,
se usó de forma explícita que op ≤ era un orden parcial. También
se puede hacer mediante una interpretación local dentro de la 
prueba, usando el comando interpret.

Observar que depende de la prueba del primer objetivo (por lo 
que usamos them) y que los objetivos que se generan por este 
comando se prueban de forma automática (.)

Entonces, la prueba del segundo objetivo se realiza mediante 
la expansión de las definiciones y auto.
 *}

interpretation int: partial_order "op ≤ :: int ⇒ int ⇒ bool"
    where "int.less x y = (x < y)"
  proof -
    show "partial_order (op ≤ :: int ⇒ int ⇒ bool)"
      by unfold_locales auto
    then interpret int: partial_order "op ≤ :: [int, int] ⇒ bool" .
    show "int.less x y = (x < y)"
      unfolding int.less_def by auto
  qed


text {* Mediante la siguiente interpretación se especifica que
los números enteros, con la relación  ≤, y las funciones min, max,
tiene estructura de retículo.
*}

interpretation int: lattice "op ≤ :: int ⇒ int ⇒ bool"
    where int_min_eq: "int.meet x y = min x y"
      and int_max_eq: "int.join x y = max x y"
  proof -
    show "lattice (op ≤ :: int ⇒ int ⇒ bool)"
      apply unfold_locales
      apply (unfold int.is_inf_def int.is_sup_def)
      by arith+
    then interpret int: lattice "op ≤ :: int ⇒ int ⇒ bool" .
    show "int.meet x y = min x y"
      by (bestsimp simp: int.meet_def int.is_inf_def)
    show "int.join x y = max x y"
      by (bestsimp simp: int.join_def int.is_sup_def)
  qed

text {* Mediante la siguiente interpretación se especifica que
los números enteros, con la relación  ≤ es un orden total. *}

interpretation int: total_order "op ≤ :: int ⇒ int ⇒ bool"
    by unfold_locales arith


text {* Algunos de los teoremas actuales en la teoría son: *}

thm int.less_def int.less_le_trans
thm int.meet_left
thm int.join_distr

text {* Observaciones:
* La teoría de retículos distributivos (distrib_lattice) también 
se ha interpretado, debido  a que en la jerarquía actual los 
órdenes totales son retículos distributivos. En general, se 
realizan las interpretaciones recorriendo la jerarquía hacia arriba.

* Mediante print_interps st se obtiene la lista de instancias de st.
*}

print_interps partial_order

text {*
\begin{itemize}
\item
  Locale @{text distrib_lattice} was also interpreted.  Since the
  locale hierarchy reflects that total orders are distributive
  lattices, the interpretation of the latter was inserted
  automatically with the interpretation of the former.  In general,
  interpretation traverses the locale hierarchy upwards and interprets
  all encountered locales, regardless whether imported or proved via
  the \isakeyword{sublocale} command.  Existing interpretations are
  skipped avoiding duplicate work.
\item
  The predicate @{term "op <"} appears in theorem @{thm [source]
  int.less_total}
  although an equation for the replacement of @{text "op ⊏"} was only
  given in the interpretation of @{text partial_order}.  The
  interpretation equations are pushed downwards the hierarchy for
  related interpretations --- that is, for interpretations that share
  the instances of parameters they have in common.
\end{itemize}
  *}

text {* Composición de contextos locales.
  Una aplicación φ entre los órdenes parciales ⊑ y ≼ conserva el orden si
  "x ⊑ y" implica "φ x ≼ φ y".  
Para formalizar esta noción es necesario importar dos veces el contexto local
de orden parcial.
*}

locale order_preserving =
    le: partial_order le + le': partial_order le'
      for le (infixl "⊑" 50) and le' (infixl "≼" 50) +
      fixes φ
      assumes hom_le: "x ⊑ y ⟹ φ x ≼ φ y"

thm order_preserving.hom_le

abbreviation (in order_preserving)
    less' (infixl "≺" 50) where "less' ≡ partial_order.less le'"


text{* Homomorfismo entre retículos: φ es un homomorfismo entre 
retículos si conserva l supremo yel ínfimo.
 *}

locale lattice_hom =
    le: lattice + le': lattice le' for le' (infixl "≼" 50) +
    fixes φ
    assumes hom_meet: "φ (x ⊓ y) = le'.meet (φ x) (φ y)"
        and hom_join: "φ (x ⊔ y) = le'.join (φ x) (φ y)"

context lattice_hom
  begin
  abbreviation meet' (infixl "⊓''" 50) where "meet' ≡ le'.meet"
  abbreviation join' (infixl "⊔''" 50) where "join' ≡ le'.join"
  end

text {* Un homomorfismo es un endomorfismos si ambos órdenes coinciden.
*}

locale lattice_end = lattice_hom _ le

text {* La notación _ permite omitir un parámetro, que queda libre
y se puede instanciar.
*}

text {* Como caso particularse tiene que un homomorfimo de retículos
conserva el orden.
 *}

sublocale lattice_hom ⊆ order_preserving
  proof unfold_locales
    fix x y
    assume "x ⊑ y"
    then have "y = (x ⊔ y)" by (simp add: le.join_connection)
    then have "φ y = (φ x ⊔' φ y)" by (simp add: hom_join [symmetric])
    then show "φ x ≼ φ y" by (simp add: le'.join_connection)
  qed

end