proposal to regularize Multiset

[jonhnet]

The current pervasvie Multiset is a bit clunky and inconsistent with other libraries:

• it is restricted to finite support, so that it can admit recursive datatypes
• its ::new constructor takes a Map, not a closure-ready Function

I propose the following changes:

• rename Multiset to FiniteMultiset. Add a doc comment to the type explaining when one would be interested in using this restricted type: when you need to put a recursive datatype inside. I'm proposing FiniteMultiset gets the funny name because it's the exception to the convention elsewhere in the standard lib.

• rename the current ::new to ::from_map, for consistency with other pervasive type APIs

• have ::new constructor to accept a Function, if feasible to express & satisfy the finiteness constraint. Otherwise, just omit ::new and let callers use ::from_map.

• Introduce a Multiset that rejects recursive datatypes, allows infinite support, and whose ::new accepts a closure Function.

• Multiset is just a wrapper for Map<V, nat>; implemented in multiset_lib.rs (no axioms).

• Note that the inifinite-support Multiset would still only have finite multiplicities, because nat for multiplicities is usable.

• Make an effort to harmonize the interfaces to Multiset and FiniteMultiset, and harmonize them with Map/Set

[jonhnet]

Further proposal for Set:

• • operator means union, but - operator doesn't mean difference. Do we need spec_subtract?
• • operator should mean intersect.
• Set has subset_of, but Map has le. Maybe we should support <= via spec_le?