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-
I was wondering if the relation is already defined somewhere?
This archive was generated by a fusion of
Pipermail (Mailman edition) and