*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Simplifying addition and subtraction of multisets*From*: Mathias Fleury <mathias.fleury12 at gmail.com>*Date*: Mon, 11 Apr 2016 14:06:55 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*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>

Hello Manuel, I do not know whether this works in all your cases, but using multiset_eq_iff might be useful: lemma "(A + B + C + D ) - (C :: 'a multiset) = A + B + D" by (auto simp: multiset_eq_iff) Mathias > On 11 Apr 2016, at 13:55, Manuel Eberl <eberlm at in.tum.de> 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 >> > >

**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: Re: [isabelle] Simplifying addition and subtraction of multisets
- 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