Re: [isabelle] Multiset elements
Am 13.08.2014 um 20:35 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> 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)«
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