Email Gateway (Aug 18 2022 at 10:47): Email Gateway (Aug 18 2022 at 10:47):From: Peter Lammich <peter.lammich@uni-muenster.de>
I wonder how to influence the precedence of simplifier rules, I have the
following problem using the Multiset library:
theory Scratch
imports Main Multiset
begin
lemma mset_singleton_eq[simp]: "a :# {#b#} = (a=b)" by auto
lemma "s:#{#f#} ==> (s=f)"
apply simp
-->This leaves me with the subgoal
0 < (if f = s then 1 else 0) ==> s = f
Of course, I could have used (simp split: split_if_asm) to resolve this,
but my point is: Why did the simplifier not use mset_singleton_eq, that
was just declared as [simp].
Examining the simplifier trace gives me, that (Multiset.count_single) is
used instead (as "x:#A" is a syntactic sugar for "0<count A x") .
Can I get the simplifier to use my lemma instead, without erasing
count_single from the default simpset ?
Bests and thanks in advance for any hints,
Peter
Email Gateway (Aug 18 2022 at 10:47):From: Tobias Nipkow <nipkow@in.tum.de>
The two lemmas
count {#b#} a = ...
0 < count {#b#} a =
form a critical pair, which is always asking for trouble. Since the
simplifier works bottom-up, the second lemma will never be applicable if
the first one is present. Sorry.
The canonical thing would be to add the critical pair as another lemma:
0 < (if a = b then 1 else 0) = (a = b).
Tobias
Peter Lammich schrieb:
Email Gateway (Aug 18 2022 at 10:53):From: Peter Lammich <peter.lammich@uni-muenster.de>
I have the following lemma about foldl:
"foldl op @ ?i ?ww = ?i @ foldl op @ [] ?ww" (or with any other
suitable operator like \<union>)
Using this as a simplification lemma loops (I think because repeatedly
rewriting the RHS with "?i=[]").
But reformulating the lemma as "?i~=[] ==> foldl op @ ?i ?ww = ?i @
foldl op @ [] ?ww" does not help, because I
want it for all expressions ?i (except literal "[]").
Is there any way to set the simplifier up to make the intended
simplification, i.e. simplify with the above lemma only if ?i is not a
literal "[]" ?
Many thanks in advance, yours
Peter
p.s. My current workaround is to instantiate ?i using [of exp], but I'd
like to have it automatically.
Email Gateway (Aug 18 2022 at 10:53):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think this can be done except by a simplification procedure (in
ML) which looks at the actual term representation.
Tobias
Peter Lammich wrote:
Last updated: Nov 21 2024 at 12:39 UTC