Theory Order_Lattice_Props.Sup_Lattice
section ‹Sup-Lattices and Other Simplifications›
theory Sup_Lattice
imports Main
begin
unbundle lattice_syntax
text ‹Some definitions for orderings and lattices in Isabelle could be simpler. The strict order in
in ord could be defined instead of being axiomatised. The function mono could have been defined on ord
and not on order---even on a general (di)graph it serves as a morphism. In complete lattices, the
supremum---and dually the infimum---suffices to define the other operations (in the Isabelle/HOL-definition
infimum, binary supremum and infimum, bottom and top element are axiomatised). This not only increases
the number of proof obligations in subclass or sublocale statements, instantiations or interpretations,
it also complicates situations where suprema are presented faithfully, e.g. mapped onto suprema in
some subalgebra, whereas infima in the subalgebra are different from those in the super-structure.›
text ‹It would be even nicer to use a class less-eq which dispenses with the strict order symbol
in ord. Then one would not have to redefine this symbol in all instantiations or interpretations.
At least, it does not carry any proof obligations.›
context ord
begin
text ‹ub-set yields the set of all upper bounds of a set; lb-set the set of all lower bounds.›
definition ub_set :: "'a set ⇒ 'a set" where
"ub_set X = {y. ∀x ∈ X. x ≤ y}"
definition lb_set :: "'a set ⇒ 'a set" where
"lb_set X = {y. ∀x ∈ X. y ≤ x}"
end
definition ord_pres :: "('a::ord ⇒ 'b::ord) ⇒ bool" where
"ord_pres f = (∀x y. x ≤ y ⟶ f x ≤ f y)"
lemma ord_pres_mono:
fixes f :: "'a::order ⇒ 'b::order"
shows "mono f = ord_pres f"
by (simp add: mono_def ord_pres_def)
class preorder_lean = ord +
assumes preorder_refl: "x ≤ x"
and preorder_trans: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
begin
definition le :: "'a ⇒ 'a ⇒ bool" where
"le x y = (x ≤ y ∧ ¬ (x ≥ y))"
end