*To*: Christoph Feller <c_feller at informatik.uni-kl.de>*Subject*: Re: [isabelle] Problem with simplifier trace*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 25 Mar 2009 13:23:20 +0100*Cc*: isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <a1e5e35a0903240623u73402fc1u49fa04ba7c90410@mail.gmail.com>*References*: <a1e5e35a0903240623u73402fc1u49fa04ba7c90410@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.19 (Macintosh/20081209)

I cannot reproduce this behaviour. I get the following: [0]Adding rewrite rule "Scratch.R1": C1 ?s1 ?v1 : X ==> f ?s1 ?v1 == f (C1 ?s1 ?v1) ?v1 [0]Adding rewrite rule "Scratch.R2": C1 ?s1 ?v1 : X == False [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: P (f (C2 s) v) [1]Applying instance of rewrite rule "Scratch.R1": C1 ?s1 ?v1 : X ==> f ?s1 ?v1 == f (C1 ?s1 ?v1) ?v1 [1]Trying to rewrite: C1 (C2 s) v : X ==> f (C2 s) v == f (C1 (C2 s) v) v [2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: C1 (C2 s) v : X [2]Applying instance of rewrite rule "Scratch.R2": C1 ?s1 ?v1 : X == False [2]Rewriting: C1 (C2 s) v : X == False [1]FAILED C1 (C2 s) v : X ==> f (C2 s) v == f (C1 (C2 s) v) v I suspect your subset of the trace does not show the correctly matching Trying and Succeeded. Tobias Christoph Feller schrieb: > Hallo! > > I have a loop in my simplifier rules and I try to get to the cause of > it. I set Isabelle to give me a simplifier trace and set the > simplifier depth to 5. Then I get a trace that leaves me confused > because I don't get what's going on. I give a reduced version of my > trace to keep it simple. C1 and C2 are constructors, f is a function. > > [1] Applying instance of rewrite rule R1 > (C1 ?s ?v) : X ==> f ?s ?v == f (C1 ?s ?v) ?v > > [1] Trying to rewrite > (C1 (C2 s) v) : X ==> f (C2 s) v == f (C1 (C2 s) v) v > > [2] SIMPLIFIER INVOKED ON THE FOLLOWING TERM > (C1 (C2 s) v) : X > > [2] Applying instance of rewrite rule R2 > (C1 ?s ?v) : X == False > > [2] Rewriting > (C1 (C2 s) v) : X == False > > [1] Succeeded > f (C2 s) v == f (C1 (C2 s) v) v > > > What I don't get is: Why does the rule R1 succeed even if it's premise > was simplified to False. Or is there something else going on? Did I > read it wrong? > > Thanks in advance, > Christoph Feller

**Follow-Ups**:**Re: [isabelle] Problem with simplifier trace***From:*Christoph Feller

**References**:**[isabelle] Problem with simplifier trace***From:*Christoph Feller

- Previous by Date: [isabelle] Type Coercions?
- Next by Date: Re: [isabelle] The Symbolic Newton Method
- Previous by Thread: [isabelle] Problem with simplifier trace
- Next by Thread: Re: [isabelle] Problem with simplifier trace
- Cl-isabelle-users March 2009 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