library Calculi/Algebra/RelationsAndOrders

version 0.1
%author: S. Woelfl
%date: 03-06-2005

%(
    This library defines some basic concepts from the
    theory of relation algebras
)%


%left_assoc __cup__,__cap__,__cmps__
%prec {__cup__} < {__cmps__}
%prec {__cmps__} < {__cmpl__}



from Basic/RelationsAndOrders version 0.7 get
        Relation,ReflexiveRelation,
        StrictOrder |-> StrictPartialOrder


spec SerialRelation =
     Relation
then
     forall x:Elem
     . exists y:Elem . x ~ y                        %(serial)%
end

view ReflexiveImpliesSerial :
     SerialRelation to ReflexiveRelation
end



spec ExtStrictPartialOrderByOrderRelations[StrictPartialOrder] = %def
     preds __>__,__<=__,__>=__,__cmp__: Elem * Elem

     forall x,y:Elem
     . x > y <=> y < x                                  %(def_suc)%
     . x <= y <=> x < y \/ x = y                        %(def_preE)%
     . x >= y <=> x > y \/ x = y                        %(def_sucE)%
     . x cmp  y <=> x < y \/ x = y \/ y < x             %(def_cmp)%

then %implies
     forall x,y:Elem
     . x <= y <=> y >= x                                %(equi_preE_sucE)%
     . x cmp y => y cmp x                               %(cmp_sym)%
end




logic HasCASL
from HasCASL/Set get Set |-> SetHasCASL


spec ExtStrictPartialOrderByConvexity[StrictPartialOrder] = %def
     SetHasCASL
then %def
     pred
         Convex : Set(Elem)
     op
         convexhull : Set(Elem) -> Set(Elem)

     forall x:Elem; X:Set(Elem)
     . Convex(X) <=>
                (forall x,y,z:Elem . x < y /\ y < z /\ x isIn X /\ z isIn X => y isIn X)
                                                                                %(def_convex)%
     . x isIn convexhull(X) <=> x isIn X \/
        (exists x',x'':Elem . x isIn X /\ x' isIn X /\ x' < x /\ x < x'')
                                                                                %(def_convexhull)%

then %implies
     forall X,Y:Set(Elem); XX:Set(Set(Elem))
     . Convex(emptySet)
     . Convex(X) /\ Convex(Y) => Convex(X intersection Y)
     . (forall X:Set(Elem) . X isIn XX => Convex(X)) /\
        (forall X,X':Set(Elem) . X isIn XX /\ X' isIn XX => X subset X' \/ X' subset X) =>
        Convex(bigunion XX)
     . Convex(convexhull(X))
end


spec ExtStrictPartialOrderBySetRelations[StrictPartialOrder] =
     ExtStrictPartialOrderByOrderRelations[StrictPartialOrder]
then %def
local SetHasCASL
within
     preds
        __<__,__>__,__<=__,__>=__: Set(Elem) * Set(Elem);
        __<__,__>__,__<=__,__>=__: Elem * Set(Elem);
        __<__,__>__,__<=__,__>=__: Set(Elem) * Elem

     forall x,y:Elem; X,Y:Set(Elem)
     . X < Y <=> (forall x,y:Elem . x isIn X /\ y isIn Y => x < y)
     . X <= Y <=> (forall x,y:Elem . x isIn X /\ y isIn Y => x <= y)
     . X > Y <=> Y < X
     . X >= Y <=> Y <=  X

     . X < y <=> X < {y}
     . X <= y <=> X <= {y}
     . X > y <=> X > {y}
     . X >= y <=> X >= {y}

     . x < Y <=> {x} < Y
     . x <= Y <=> {x} <= Y
     . x > Y <=> {x} > Y
     . x >= Y <=> {x} >= Y
end