# Re: [isabelle] Simplifying addition and subtraction of multisets

```Well, that works for some cases, but not for all, e.g:

lemma "(A + B + C + D ) - (C :: 'a multiset) = A + B + D"

```
I don't think this is going to work without a simproc. The arithmetic procedures do things like that; maybe they can be adapted for this, or perhaps it's just a matter of the right setup?
```
I don't know who is the expert on these procedures.

Manuel

On 08/04/16 14:24, Julian Nagele wrote:
```
```Hello Manuel,

simplifying with subset_mset.diff_add_assoc works for me:

lemma "{#a, b, c, d#} - {#b#} = {#a, c, d#}"

or, more generally

lemma
fixes A B C :: "'a multiset"
shows "(A + C + B) - C = A + B"

Hope that helps,
Julian

Manuel Eberl writes:

```
```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.