[isabelle] Multiset elements



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"

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.