*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Simplifier question*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 30 Aug 2007 13:45:01 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <46D68FFE.6070408@uni-muenster.de>*References*: <46D68FFE.6070408@uni-muenster.de>*User-agent*: Thunderbird 2.0.0.0 (Macintosh/20070326)

The two lemmas count {#b#} a = ... 0 < count {#b#} a =

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

**References**:**[isabelle] Simplifier question***From:*Peter Lammich

- Previous by Date: [isabelle] PhD position available : Building reliable programs in computational geometry and certifying them with Coq
- Next by Date: [isabelle] Isabelle Installation
- Previous by Thread: [isabelle] Simplifier question
- Next by Thread: [isabelle] PhD position available : Building reliable programs in computational geometry and certifying them with Coq
- Cl-isabelle-users August 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list