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.