Re: [isabelle] Multiset elements

> There are variations. Hence this requires a clear design of which notions get
> reduced to which, and a library that follows the design.

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

With the proposal

  x :# M == not (count M x = 0)

you would end up with the problem of double negation (try »not (x :# m)«

There is also a strong algebraic argument: membership abstracts over
structure (order) and repetition.  This is what »set« does for lists,
and »set_of« for multisets (where structure anyway is irrelevant).
»count« does not abstract over anything.

> Or at least an
> empirical proof that some newly proposed design improves matters.

The simp rules surely need some refinement and augmentation, like
  "count M x = 0 <--> not (x :# M)"
  "x :# (M inter N) <--> x :# M && y :# N"
if not present yet.

But this is the usual iteration cycle of analysis and empirical checking.

Hope this makes things more explicit,

PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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