# [isabelle] Simplifying addition and subtraction of multisets

Hallo,

`I have terms like "{#a,b,c,d#} - {#b#}", which desugars to "(single a +
``single b + single c + single d) - single b". This is obviously equal to
``"{#a,c,d#}".
`

`However, the simplifier fails to prove this and I was not able to find a
``setup of existing simplification rules to solve it.
`
I ended up proving the following rule, which works in my particular case:
lemma multiset_Diff_single_normalize:
fixes a c assumes "a â c"
shows "({#a#} + B) - {#c#} = {#a#} + (B - {#c#})"

`This, combined with add_ac, does the trick. (but only because I can, in
``this particular instance, decide whether two elements are equal, i.e. I
``know that b != c and b != d, even though the simplification of
``"{#a,b,c,d#} - {#b#}" would be sound even if that were not the case)
`
Is there some existing simproc that can be set up to do this automatically?
Cheers,
Manuel

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