*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Simplifying addition and subtraction of multisets*From*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Date*: Fri, 15 Apr 2016 20:05:50 +1000*Authentication-results*: lists.cam.ac.uk; dkim=none (message not signed) header.d=none; lists.cam.ac.uk; dmarc=none action=none header.from=anu.edu.au;*In-reply-to*: <570BA683.507@inf.ethz.ch>*References*: <57079B46.8060302@in.tum.de> <87shywthip.fsf@jnx230.uibk.ac.at> <570B90BD.50907@in.tum.de> <570BA683.507@inf.ethz.ch>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:23*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.3.0

obeying A + B - B = A but not (necessarily) A - B + B = A It's all in http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/pmgms/ specifically in pmg_cancel_sums.ML

Jeremy On 11/04/16 23:28, Andreas Lochbihler wrote:

Hi Manuel, I also think that you need a simproc, because the nesting can be arbitrarily deep. Since multisets are similar to natural numbers in terms of their algebraic properties, I'd suggest that you look at the simprocs for natural numbers. I guess that you can generalise cancel_diff_conv in src/HOL/Tools/Nat_Arith.ML appropriately to multisets. 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

**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

**Re: [isabelle] Simplifying addition and subtraction of multisets***From:*Andreas Lochbihler

- Previous by Date: [isabelle] International SAT/SMT/AR Summer School
- Next by Date: [isabelle] inductive + for
- Previous by Thread: Re: [isabelle] Simplifying addition and subtraction of multisets
- Next by Thread: [isabelle] Problem with function definitions
- 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