library Calculi/Algebra/BooleanAlgebra

version 0.2
%author: S. Woelfl
%date: 16-06-2005

%(
    This library defines some basic concepts from the  theory of
        Boolean algebras. Some specs are just here to remove some
        "junk" from other libraries
)%


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



from Basic/RelationsAndOrders version 0.7 get
        BooleanAlgebra |-> WeakBooleanAlgebra ,
        ExtBooleanAlgebra ,
        RichBooleanAlgebra
from Basic/RelationsAndOrders version 0.7 get
        StrictOrder |-> StrictPartialOrder


spec BooleanAlgebra =
     WeakBooleanAlgebra
then
     . not 0 = 1
end


spec ExtBooleanAlgebraByCompl[BooleanAlgebra] = %def
     { ExtBooleanAlgebra[BooleanAlgebra]
        hide preds __<=__, __<__, __>=__, __>__}
then %implies
     forall x,y: Elem
     . compl(0) = 1
     . compl(1) = 0
end


spec BooleanAlgebraWithCompl = ExtBooleanAlgebraByCompl[BooleanAlgebra]


spec ExtBooleanAlgebraByOrderRelations[BooleanAlgebra] = %def
     { ExtBooleanAlgebra[BooleanAlgebra]
        hide op compl__ }
then %def
     pred Atom: Elem

     forall x,y:Elem
     . Atom(x) <=> not x = 0 /\ (forall y:Elem . y < x => y = 0) %(def_Atom)%
end


spec BooleanAlgebraWithOrderRelations =
        ExtBooleanAlgebraByOrderRelations[BooleanAlgebra]
end


view BooleanAlgebraWithOrderRelations_as_StrictPartialOrder :
     StrictPartialOrder to BooleanAlgebraWithOrderRelations
end



spec AtomicBooleanAlgebra =
     { BooleanAlgebraWithOrderRelations hide pred Atom }
then
     sort AtomElem = {x: Elem . not x = 0 /\ (forall y:Elem . y < x => y = 0)}
     forall x:Elem
     . not x = 0 => (exists y:AtomElem . y <= x)
end