*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Multiset elements*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 13 Aug 2014 16:14:20 +0200*In-reply-to*: <53EB5282.3020202@informatik.tu-muenchen.de>*References*: <A67B9E22-FC50-46BE-BCE6-5A029AB42108@in.tum.de> <53EA56F4.8030504@in.tum.de> <53EB5282.3020202@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

There are variations. Hence this requires a clear design of which notions get reduced to which, and a library that follows the design. Or at least an empirical proof that some newly proposed design improves matters. Tobias On 13/08/2014 13:56, Florian Haftmann wrote: > A more radical answer would be > > abbreviation Melem :: "'a => 'a multiset => bool" > ("(_/ :# _)" [50, 51] 50) > where > "a :# M == a : set_of M" > > i.e. reduce membership on multisets to membership on sets. > > It is similar to membership on lists, and requires only a notion about > the functorial structure of multisets. > > This also suggests a lemma [simp]: > > "count M a = 0 <--> a \<notin> set_of M" > > which seems to be absent from Multiset.thy > > Florian > > > Am 12.08.2014 um 20:03 schrieb Tobias Nipkow: >> >> On 12/08/2014 19:38, Jasmin Christian Blanchette wrote: >>> Hi all, >>> >>> When playing with multisets, I stumbled upon the following annoying behavior. Formulas of the form "~ x :# M" are rewritten to "count M a = 0" due to the simp rule "not_gr0". This is easy to see once we look at how ":#" is introduced: >>> >>> abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where >>> "a :# M == 0 < count M a" >>> >>> The issue wouldn't arise if the definition were >>> >>> abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where >>> "a :# M == count M a = 0" >> >> I hope you meant ~= ? >> >> I believe I defined it that way because a long time ago linear arithmetic >> preferred "> 0" over "~= 0". This is no longer the case and I don't think we >> have a strong preference either way wrt proofs. Thus a change is likely to cause >> few ill effects, although of course that needs to be checked. >> >> Tobias >> >>> instead. Apart from compatibility, is there a reason not to do so? >>> >>> Thanks. >>> >>> Jasmin >>> >>> >> >

**Follow-Ups**:**Re: [isabelle] Multiset elements***From:*Florian Haftmann

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

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

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

- Previous by Date: Re: [isabelle] op =simp=> in congruence rules
- 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