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 {* 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
