Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution

Multiset.thy defines the relation mset_le as you describe.

It also overloads <= with the much stronger multiset ordering, which is described in a classic paper:

Nachum Dershowitz, Zohar Manna: Proving Termination with Multiset Orderings. Commun. ACM 22(8): 465-476 (1979)


On 4 Jul 2007, at 08:01, Revantha Ramanayake wrote:

Is the subset relation defined in the obvious way for multisets? I.e. how do I write
N is a sub-multiset of M.

I know that I can define: N is a sub-multiset of M as (ALL b. count N b <= count M b) but then I will have to prove a host of properties for the sub- multiset relation.
I was wondering if the relation is already defined somewhere?

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