Concepts from Order Theory

spec
     SigOrder =
     sort
          Elem
     pred
           __ <= __,
           __ >= __,
           __ < __,
           __ > __: Elem * Elem;
     var
          x,y:Elem
     .          x >= y <=> y <= x
     .          x < y <=> (x <= y /\ not (x=y))
     .          x > y <=> y < x
end

spec
     PartialOrder =
     sort
          Elem
     pred
          __ <= __: Elem * Elem
     vars
          x,y,z:Elem
     %%          reflexivity:
     .          x <= x
     %%          antisymmetry:
     .          x = y if x <= y /\ y <= x
     %%          transitivity:
     .          x <= z if x <= y /\ y <= z
end

spec
     TotalOrder =
     PartialOrder with sort Elem, pred __ <= __
then
     vars
          x,y:Elem
     .          x <= y \/ y <= x
end

spec
     DefineBooleanAlgebra =
     sort
          Elem
     ops
           0:Elem;
           1:Elem;
           __ cap __: Elem * Elem -> Elem,
                      assoc, comm, unit 1;
           __ cup __: Elem * Elem -> Elem,
                      assoc, comm, unit 0;
     %%prec          __ cup __ < __ cap __
     vars
          x,y,z:Elem
     %%          "adjointness":
     .          x cap ( x cup y) = x
     .          x cup ( x cap y) = x
     %%          Zero and One:
     .          x cap 0 = 0
     .          x cup 1 = 1
     %%          distributive laws:
     .          x cap ( y cup z) = (x cap y) cup ( x cap z)
     .          x cup ( y cap z) = (x cup y) cap ( x cup z)
     %%          existence of an inverse element:
     .          exists x': Elem . x cup x' = 1 /\ x cap x' = 0
end

spec
     BooleanAlgebra
     [DefineBooleanAlgebra with sort Elem, ops 0, 1,__ cap __, __ cup __] =
%%def
     SigOrder with preds __ <= __,__ >= __,__<__,__>__
     vars
          x,y:Elem
     %%          induced partial order:
     .          x <= y <=> x cap y = x
end

view
     PartialOrder_in_BooleanAlgebra
     [DefineBooleanAlgebra]:
PartialOrder
     to BooleanAlgebra [DefineBooleanAlgebra] =
      sort Elem |-> Elem,
      pred __ <= __ |-> __ <= __
end