*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Multiset elements*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 13 Aug 2014 20:35:21 +0200*In-reply-to*: <53EB72BC.9050904@in.tum.de>*Organization*: TU Munich*References*: <A67B9E22-FC50-46BE-BCE6-5A029AB42108@in.tum.de> <53EA56F4.8030504@in.tum.de> <53EB5282.3020202@informatik.tu-muenchen.de> <53EB72BC.9050904@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.0

> 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)« mentally). 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, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Multiset elements***From:*Jasmin Christian Blanchette

**References**:**[isabelle] Multiset elements***From:*Jasmin Christian Blanchette

**Re: [isabelle] Multiset elements***From:*Tobias Nipkow

**Re: [isabelle] Multiset elements***From:*Florian Haftmann

**Re: [isabelle] Multiset elements***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] RC-3 puts method error after subgoals and warnings in output
- Next by Date: Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
- Previous by Thread: Re: [isabelle] Multiset elements
- Next by Thread: Re: [isabelle] Multiset elements
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list