Thanks for all your help but I did it the following way eventually:
First I restricted my bags to contain only elements with non-zero multiplicity
module bags
open util/natural
open util/relation
sig Element{}
sig Bag{
elements: Element -> one Natural
}{
all e: Element.elements | e != Zero
}
And coded union/difference/intersection like this:
fun BagUnion[b1, b2 : Element -> one Natural]: Element -> one Natural{
let e = (dom[b1] + dom[b2]) | e -> add[e.b1, e.b2]
}
fun BagDifference[b1, b2 : Element -> one Natural]: Element -> one Natural{
let e = dom[b1] | e -> max[Zero + sub[e.b1, e.b2]]
}
fun BagIntersection[b1, b2 : Element -> one Natural]: Element -> one Natural{
let e = (dom[b1] & dom[b2]) | e -> min[e.b1 + e.b2]
}