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

Hello Manuel,
simplifying with subset_mset.diff_add_assoc works for me:
lemma "{#a, b, c, d#} - {#b#} = {#a, c, d#}"
by (simp add: subset_mset.diff_add_assoc)
or, more generally
lemma
fixes A B C :: "'a multiset"
shows "(A + C + B) - C = A + B"
by (simp add: subset_mset.diff_add_assoc ac_simps)
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.*