library Basic/RelationsAndOrders
version 0.7
%% authors: M.Roggenbach, T.Mossakowski, L.Schröder
%% date: 23.3.01

%prec { __ cup __ } < { __ cap __}

from Basic/Numbers version 0.7 get Nat, Int, Rat

spec Relation =
     sort
          Elem
     pred
          __ ~ __: Elem * Elem
end

spec ReflexiveRelation =
     Relation
then
     forall
          x:Elem
     .
          x ~ x             %(refl)%
end

spec SymmetricRelation =
     Relation
then
     forall
          x,y:Elem
     .
          x ~ y if y ~ x             %(sym)%
end

spec TransitiveRelation =
     Relation
then
     forall
          x,y,z:Elem
     .
          x ~ z if x ~ y /\ y ~ z             %(trans)%
end

spec SimilarityRelation =
     ReflexiveRelation and SymmetricRelation
end

spec PartialEquivalenceRelation =
     SymmetricRelation and TransitiveRelation
end

spec
     EquivalenceRelation =
     ReflexiveRelation and PartialEquivalenceRelation
end

spec
     SigOrder[sort Elem] =

     preds
           __ <= __, __ < __,
           __ >= __, __ > __: Elem * Elem;
     forall
          x,y:Elem
     .
          x >= y <=> y <= x             %(SigOrder_geq_def)%
     .
          x < y <=> (x <= y /\ not (x=y))             %(SigOrder_less_def)%
     .
          x > y <=> y < x             %(SigOrder_greater_def)%
end

spec
     PreOrder =
     {ReflexiveRelation and TransitiveRelation}
     with pred __ ~ __ |-> __ <= __
end

spec
     PartialOrder =
     PreOrder
then
     forall
          x,y:Elem
     .
          x = y if x <= y /\ y <= x             %(POrder_antisym)%
end

spec TotalOrder =
  PartialOrder
then
  forall x,y:Elem
  . x <= y \/ y <= x             %(TOrder_comparability)%
end


view TotalOrder_in_Nat: TotalOrder to Nat =
     sort Elem |-> Nat
end

view TotalOrder_in_Int: TotalOrder to Int =
     sort Elem |-> Int
end

view TotalOrder_in_Rat : TotalOrder to Rat =
     sort Elem |-> Rat
end


spec
     BooleanAlgebra =
     sort
          Elem
     ops
           0,1:       Elem;
           __ cap __: Elem * Elem -> Elem, assoc, comm, unit 1;
           __ cup __: Elem * Elem -> Elem, assoc, comm, unit 0;
     forall
          x,y,z:Elem
     .
          x cap ( x cup y) = x             %(absorption_def1)%
     .
          x cup ( x cap y) = x             %(absorption_def2)%
     .
          x cap 0 = 0             %(zeroAndCap)%
     .
          x cup 1 = 1             %(oneAndCup)%
     .
          x cap ( y cup z) = (x cap y) cup ( x cap z)             %(BA_distr_def1)%
     .
          x cup ( y cap z) = (x cup y) cap ( x cup z)             %(BA_distr_def2)%
     .
          exists x': Elem . x cup x' = 1 /\ x cap x' = 0             %(BA_inverse_def)%
then
     %implies
     op
          __ cup __, __ cap __ : Elem * Elem -> Elem , idem
     forall
          x: Elem
     .
          exists! x': Elem . x cup x' = 1 /\ x cap
          x' = 0             %(BA_uniqueComplement)%
end


spec
     ExtPartialOrder  [PartialOrder]
=
     %def
     SigOrder [sort Elem]
and
{
          ops
                inf,sup : Elem * Elem ->? Elem
          forall
               x,y,z: Elem
          .
               inf(x,y) = z <=>
                z <= x /\ z <= y /\ (forall t: Elem . t <= x /\ t <= y => t
                <= z)             %(inf_def)%
          .
               sup(x,y) = z <=>
                x <= z /\ y <= z /\ (forall t: Elem . x <= t /\ y <= t => z
                <= t)             %(sup_def)%
     then
          %implies
          ops
               inf,sup : Elem * Elem ->? Elem, comm
}
end


spec
     ExtTotalOrder  [TotalOrder]
=
     %def
     ExtPartialOrder [PartialOrder]
and
{
          ops
               min, max: Elem * Elem -> Elem
          forall
               x,y: Elem
          .
               min(x,y) = x when x <= y else y             %(min_def)%
          .
               max(x,y) = y when x <= y else x             %(max_def)%
     then
          %implies
          ops
                min, max: Elem * Elem -> Elem,
                          comm, assoc
}
then
     %implies
     forall
          x,y: Elem
     .
          min(x,y)=inf(x,y)             %(min_inf_relation)%
     .
          max(x,y)=sup(x,y)             %(max_sup_relation)%
end



spec
     ExtBooleanAlgebra  [BooleanAlgebra]
=
     %def
     {
          SigOrder [sort Elem]
          then forall x,y:Elem
          . x <= y <=> x cap y = x             %(BA_po_def)%
     }
     and
     {
          op compl: Elem -> Elem
          forall x,y:Elem
          . compl(x)=y <=> x cup y = 1 /\ x cap y = 0             %(BA_compl_def)%
     }
then
     %implies
     forall
          x,y: Elem
     .
          compl(x cap y) = compl(x) cup compl(y)             %(de_Morgan1)%
     .
          compl(x cup y) = compl(x) cap compl(y)             %(de_Morgan2)%
     .
          compl(compl(x)) = x             %(BA_involution_compl)%
end

view
     PartialOrder_in_ExtBooleanAlgebra  [BooleanAlgebra]:
     PartialOrder to ExtBooleanAlgebra[BooleanAlgebra] 
end


spec RichPartialOrder = ExtPartialOrder  [PartialOrder]
spec RichTotalOrder = ExtTotalOrder  [TotalOrder]
spec RichBooleanAlgebra = ExtBooleanAlgebra  [BooleanAlgebra]