List and Bag

spec
     GenerateList [Elem with sort Elem] =
     free
          types
           List[Elem]         ::=  nil | sort NonEmptyList[Elem];
           NonEmptyList[Elem] ::=  __ :: __ (first : Elem; rest :
                                   List[Elem])
     op
          __ :: __: Elem × List[Elem] -> List[Elem] %%right assoc
end

spec
     List[Elem with sort Elem] =
     GenerateList[Elem] with
      sort List[Elem], NonEmptyList[Elem],
      ops nil, __ :: __, first, rest
     and Nat with
      sorts Nat, Pos,
      preds __ <= __,__ >= __,__<__,__>__,
      ops  0, suc, pre,
           +__, abs, __ + __, __ - __, __ * __,
           __ div __, __ mod __, min, max, __ ^ __,
           1,2,3,4,5,6,7,8,9, __ :: __
then
     pred
          isEmpty: List[Elem]
     ops
           last:      List[Elem] ->? Elem;
           length:    List[Elem] -> Nat;
           __ ++ __ : List[Elem] × List[Elem] -> List[Elem];
           reverse:   List[Elem] -> List[Elem];
           take,drop: Nat × List[Elem] ->? List[Elem]
     vars
          x: Elem; n: Nat; L,K: List[Elem]
     %%          isEmpty:
     .          isEmpty(L) <=> L=nil
     %%          last:
     .          def last(L) <=> not isEmpty(L)
     .          last (x :: nil) = x
     .          last (x :: L) = last(L) if not L=nil
     %%          length:
     .          length (nil) = 0
     .          length (x :: L) = suc(length(L))
     %%          concatenating lists:
     .          nil ++ L = L
     .          x::L ++ K = x :: (L ++ K)
     %%          reverse:
     .          reverse(nil)=nil
     .          reverse(x::L)= reverse(L) ++ (x::nil)
     %%          take(n,L) - construct a list of the first n items of a list L:
     .          def take(n,L) <=> length(L) >= n
     .          take ( 0, L) = nil
     .          take ( suc(n), x :: L)  = x :: take(n,L) if def take( n, L)
     %%          drop(n,L) - remove the first n items of a list L:
     .          def drop(n,L) <=> length(L) >= n
     .          drop ( 0, L) = L
     .          drop ( suc(n), x :: L ) = drop(n,L) if def drop(n, L)
end

view
     Monoid_in_List [Elem]: Monoid to List [Elem] =
     sort
          Elem |-> List[Elem],
     ops
           0 |-> Nil,
           __+__ |-> __ ++ __
end

spec
     GenerateBag [Elem with sort Elem] =
     Nat with
      sorts Nat, Pos,
      preds __ <= __,__ >= __,__<__,__>__,
      ops  0, suc, pre,
           +__, abs, __ + __, __ - __, __ * __,
           __ div __, __ mod __, min, max, __ ^ __,
           1,2,3,4,5,6,7,8,9, __ :: __
     and List[Elem] with
      sorts List[Elem], NonEmptyList[Elem],
      pred  empty,
      ops   nil, __ :: __, first, rest,
            last, length, __ ++ __, reverse, take, drop
then
     op
          numberOf: Elem × List[Elem] -> Nat
     vars
          x,y:Elem; L: List
     .          numberOf (x,nil) = 0
     .          numberOf (x, y::L) = numberOf (x, L) if not x=y
     .          numberOf (x, y::L) = suc(numberOf (x, L)) if x=y
then
     free
     {
          type
               Bag[Elem] ::= quotient(List[Elem])
          vars
               x:Elem; K,L: List[Elem]
          .                quotient(K)=quotient(L) <=>
                numberOf(x,K) = numberOf(x,L)
     }
     %%          intended system of representatives:
     %%          functions B: Elem -> Nat,
     %%          where B(x)>0 for finitely many x. Any such function B
     %%          represents a set of lists L
     %%          with numberOf(x,L)=B(x) for all x in Elem.end

spec
     Bag[Elem with sort Elem] =
     GenerateBag[Elem] with
      sorts Nat, Pos, List[Elem], NonEmptyList[Elem], Bag[Elem],
      preds __ <= __,__ >= __,__<__,__>__, empty,
      ops  0, suc, pre,
           +__, abs, __ + __, __ - __, __ * __,
           __ div __, __ mod __, min, max, __ ^ __,
           1,2,3,4,5,6,7,8,9, __ :: __,
           nil, __ :: __, first, rest,
           last, length, __ ++ __, reverse, take, drop,
           numberOf, quotient
then
     preds
           __ elemOf __:     Elem * Bag[Elem];
           __ isSubsetOf __: Bag[Elem] * Bag[Elem]
     ops
           empty:                           Bag[Elem];
           numberOf:                         Bag[Elem] -> Nat;
           put, remove:                     Elem × Bag[Elem] -> Bag[Elem];
           __ union __, __ intersection __: Bag[Elem] * Bag[Elem] ->
                                            Bag[Elem]
     axiom
          empty = quotient(nil)
     vars
          x: Elem; B,C,D: Bag[Elem]; L: List[Elem]
     %%          numberOf - cast for the operation on List:
     .          numberOf(x,quotient(L)) = numberOf(x,L)
     %%          x  elemOf B:
     .          x elemOf B <=> numberOf(x,B) > 0
     %%          put(x,B) - add an element x to a bag B:
     .           put(x,B) = C <=>

           (forall y: Elem .  ( not y = x => numberOf (y,B) =
                              numberOf(y,C)) /\
                              ( y = x => numberOf (y,B)+1 = numberOf(y,C))
                              )

     %%          remove(x,B) - remove an element x from a bag B:
     .          remove(x,B) = B if numberOf(x,B)=0
     .          remove(x,B) = C /\
           (forall y: Elem . ( not y = x => numberOf (y,B) = numberOf(y,C))
                             /\
                             ( y = x => numberOf (y,B)-1 = numberOf (y,C)))

          if numberOf(x,B)>0
     %%          B isSubsetOf C:
     .          B isSubsetOf C <=> ( forall x: Elem . numberOf(x,B) <=
          numberOf(x,C) )
     %%          B union C:
     .           B union C = D <=> ( forall x: Elem .           numberOf(x,D) = numberOf(x,B) + numberOf(x,C) )
     %%          S intersection T:
     .           B intersection C = D <=> ( forall x: Elem . numberOf(x,D) = min ( numberOf(x,B), numberOf(x,C) ) )

end

view
     PartialOrder_in_Bag [Elem]: PartialOrder to Bag[Elem] =
     sort
          Elem |-> Bag[Elem],
     pred
          __ <= __ |-> __ isSubsetOf __
end