Re: [isabelle] Problem with simplifier trace



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





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