# Theory Orders

section ‹Orders›
theory Orders imports Main begin
subsection ‹Ordered structures›
text ‹
We define several classes of ordered structures over some type \<^typ>‹'a› with relation ‹⊑ :: 'a ⇒ 'a ⇒ bool›. For a
\emph{quasi-order} that relation is required to be reflexive and
transitive, for a \emph{partial order} it also has to be
anti-symmetric, while for a \emph{linear order} all elements are
required to be related (in either direction).
›
class leq =
fixes leq :: "'a ⇒ 'a ⇒ bool" (infixl "⊑" 50)
class quasi_order = leq +
assumes leq_refl [intro?]: "x ⊑ x"
assumes leq_trans [trans]: "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z"
class partial_order = quasi_order +
assumes leq_antisym [trans]: "x ⊑ y ⟹ y ⊑ x ⟹ x = y"
class linear_order = partial_order +
assumes leq_linear: "x ⊑ y ∨ y ⊑ x"
lemma linear_order_cases:
"((x::'a::linear_order) ⊑ y ⟹ C) ⟹ (y ⊑ x ⟹ C) ⟹ C"
by (insert leq_linear) blast
subsection ‹Duality›
text ‹
The \emph{dual} of an ordered structure is an isomorphic copy of the
underlying type, with the ‹⊑› relation defined as the inverse
of the original one.
›