Re: [isabelle] Simplifier question



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





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