[isabelle] Simplifier question



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.