# Re: [isabelle] Multiset elements

```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
>>
>>
>

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

```

Attachment: signature.asc
Description: OpenPGP digital signature

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