*To*: Manuel Eberl <eberlm at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Simplifying addition and subtraction of multisets*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 11 Apr 2016 15:28:35 +0200*In-reply-to*: <570B90BD.50907@in.tum.de>*References*: <57079B46.8060302@in.tum.de> <87shywthip.fsf@jnx230.uibk.ac.at> <570B90BD.50907@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Hi Manuel,

Hope this helps, Andreas On 11/04/16 13:55, Manuel Eberl wrote:

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#}" 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

**Follow-Ups**:**Re: [isabelle] Simplifying addition and subtraction of multisets***From:*Jeremy Dawson

**References**:**[isabelle] Simplifying addition and subtraction of multisets***From:*Manuel Eberl

**Re: [isabelle] Simplifying addition and subtraction of multisets***From:*Julian Nagele

**Re: [isabelle] Simplifying addition and subtraction of multisets***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Simplifying addition and subtraction of multisets
- Next by Date: [isabelle] Automation for sub-term-like well-orderings
- Previous by Thread: Re: [isabelle] Simplifying addition and subtraction of multisets
- Next by Thread: Re: [isabelle] Simplifying addition and subtraction of multisets
- Cl-isabelle-users April 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list