Re: [isabelle] Multiset elements



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.