Email Gateway (Aug 22 2022 at 13:06): Email Gateway (Aug 22 2022 at 13:06):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:06):From: Julian Nagele <julian.nagele@uibk.ac.at>
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:
Email Gateway (Aug 22 2022 at 13:08):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:08):From: Mathias Fleury <mathias.fleury12@gmail.com>
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
Email Gateway (Aug 22 2022 at 13:08):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 13:10):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Yes, I've done simprocs to do this. They're based largely on those for
natural numbers, but for a type class that has +, =
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
It all works with Isabelle 2005, which is where I gave up changing
everything I'd ever done to keep up with the changes in Isabelle
Jeremy
Last updated: Apr 26 2024 at 04:17 UTC