[isabelle] Problem with simplifier trace



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.