Struct MultisetCopy item path

Returns the count, or multiplicity of a single value within the multiset.

The total size of the multiset, i.e., the sum of all multiplicities over all values.

An empty multiset.

Creates a multiset whose elements are given by the domain of the map m and whose multiplicities are given by the corresponding values of m[element]. The map m must be finite, or else this multiset is arbitrary.

A singleton multiset, i.e., a multiset with a single element of multiplicity 1.

Takes the union of two multisets. For a given element, its multiplicity in the resulting multiset is the sum of its multiplicities in the operands.

Takes the difference of two multisets. The multiplicities of m2 are subtracted from those of self; if any element occurs more in m2 then the resulting multiplicity bottoms out at 0. (See axiom_multiset_sub for the precise definition.)

Note in particular that self == self.sub(m).add(m) only holds if m is included in self.

{ self.add(Self::singleton(v)) }

Inserts one instance the value v into the multiset.

This always increases the total size of the multiset by 1.

{ self.sub(Self::singleton(v)) }

Removes one instance of the value v from the multiset.

If v was absent from the multiset, then the multiset is unchanged.

{
    let map = Map::new(
        |key: V| (self.contains(key) || key == v),
        |key: V| if key == v { mult } else { self.count(key) },
    );
    Self::from_map(map)
}

Updates the multiplicity of the value v in the multiset to mult.

{ forall |v: V| self.count(v) <= m2.count(v) }

Returns true is the left argument is contained in the right argument, that is, if for each value v, the number of occurences in the left is at most the number of occurences in the right.

{ choose |v: V| self.count(v) > 0 }

Chooses an arbitrary value of the multiset.

This is often useful for proofs by induction.

(Note that, although the result is arbitrary, it is still a deterministic function like any other spec function.)

{ self.count(v) > 0 }

Predicate indicating if the multiset contains the given value.

{ self.contains(v) }

Predicate indicating if the set contains the given element: supports self has a syntax.

{
    let m = Map::<
        V,
        nat,
    >::new(
        |v: V| self.contains(v),
        |v: V| min(self.count(v) as int, other.count(v) as int) as nat,
    );
    Self::from_map(m)
}

Returns a multiset containing the lower count of a given element between the two sets. In other words, returns a multiset with only the elements that “overlap”.

{
    let m = Map::<
        V,
        nat,
    >::new(|v: V| self.contains(v), |v: V| clip(self.count(v) - other.count(v)));
    Self::from_map(m)
}

Returns a multiset containing the difference between the count of a given element of the two sets.

{ forall |x: V| self.count(x) == 0 || other.count(x) == 0 }

Returns true if there exist no elements that have a count greater than 0 in both multisets. In other words, returns true if the two multisets have no elements in common.

{ Set::new(|v: V| self.count(v) > 0) }

Returns the set of all elements that have a count greater than 0

{ self.len() == 0 }

Is true if called by an “empty” multiset, i.e., a set containing no elements and has length 0

{
    &&& self.len() > 0
    &&& (forall |x: A| self.contains(x) ==> self.count(x) == 1)
    &&& (forall |x: A, y: A| self.contains(x) && self.contains(y) ==> x == y)

}

A singleton multiset has at least one element with multiplicity 1 and any two elements are equal.

self.is_singleton(),

self.contains(x),

self =~= Multiset::singleton(x),

A singleton multiset that contains an alement is equivalent to the singleton multiset with that element.

self.is_singleton(),

self.len() == 1,

A singleton multiset has length 1.

s.is_singleton() <==> (s.len() == 1),

A multiset has exactly one element, if and only if, it has at least one element with multiplicity 1 and any two elements are equal.

Returns the argument unchanged.

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.