[PostScript]
Bag (E, C): trait
% Common bag operators
includes
BagBasics,
DerivedOrders (C, \subseteq for <=, \supseteq for >=,
\subset for <, \supset for >)
introduces
delete: E, C -> C
{__}: E -> C
__\in __, __\notin __: E, C -> Bool
size: C -> Int
__\U __, __-__: C, C -> C
asserts
forall e, e1, e2: E, b, b1, b2: C
count(e1, delete(e2, b)) ==
if e1 = e2 then max(0, count(e1, b) - 1)
else count(e1, b);
{ e } == insert(e, {});
e \in b == count(e, b) > 0;
e \notin b == count(e, b) = 0;
size({}) == 0;
size(insert(e, b)) == size(b) + 1;
count(e, b1 \U b2) ==
count(e, b1) + count(e, b2);
count(e, b1 - b2) ==
max(0, count(e, b1) - count(e, b2));
b1 \subseteq b2 == b1 - b2 = {};
implies
AbelianMonoid (\U for \circ, {} for unit, C for T),
JoinOp (\U, {} for empty),
MemberOp ({} for empty),
PartialOrder (C, \subseteq for <=, \supseteq for >=,
\subset for <, \supset for >)
forall e, e1, e2: E, b, b1, b2: C
insert(e, b) \neq {};
count(e, b) >= 0;
count(e, b) <= size(b);
b1 \subseteq b2 => count(e, b1) <= count(e, b2)
converts count, \in, \notin, {__}, \U, -:C,C->C,
delete, size, \subseteq, \supseteq, \subset, \supset

[Table of Contents] [Index]