Re: [isabelle] Multiset elements

Hi Florian,

Am 13.08.2014 um 20:35 schrieb Florian Haftmann <florian.haftmann at>:

> The design principle is simply to follow the established convention on
> lists.  Here we do not have any abbreviation for membership but simply write
>  x : set xs
> Transferring this to multisets, we end up with
>  x : set_of M
> for which you can argue that almost-well-established mathematical
> notation exists also, hence the abbreviation
>  x :# M == x : set_of M

Good point. The design for "List", other parts of the library, and the BNF (co)datatypes, is in favor of "_ : set_of _" rather than "predicators" (?). It seems to have worked well and should probably be imitated. Apart from the fact that multisets are not a free datatype, they are otherwise very much like lists and should feel that way too (while keeping the set-like syntactic sugar).

> With the proposal
>  x :# M == not (count M x = 0)
> you would end up with the problem of double negation (try »not (x :# m)«
> mentally).

My original proposal didn't have the double negation issue, but it had another blemish, as noted by Tobias. ;)

> Hope this makes things more explicit,

Yes. In the coming weeks or months, Dmitriy and I should be making some contributions to the "Multiset" theory. This would be a good opportunity to clean it up, to the extend to which it can be done without breaking existing applications beyond repair.

Two more things:

1. You circulated privately some renaming proposals, with "_mset" as a fairly systematic suffix (no more "m" or "M" prefixes). This is also something we would look into.

2. There are currently two (provably identical) map functions -- the traditional "image_mset" and the Popescuesque "mmap". This needs to be consolidated.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.