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