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




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