Re: [isabelle] Simplifying addition and subtraction of multisets



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.