Re: [isabelle] Problem with simplifier trace


On Wed, Mar 25, 2009 at 13:23, Tobias Nipkow <nipkow at> wrote:
> I cannot reproduce this behaviour. I get the following:
> [...]

My concrete case is more complicate than the example so that isn't too

> I suspect your subset of the trace does not show the correctly matching
> Trying and Succeeded.

I can't deny that but before my subset/-sequence I had an failed
attempt at a similiar rule like R1 (where the assumption wasn't
reducible to False) and I didn't leave anything out. Perhaps there is
some output from Isabelle missing here?

I solved the problem as I noticed that I really want a more general form of R1:
(C1 ?s ?v) : X ==> f ?s ?w == f (C1 ?s ?v) ?w

(So the parameter of the function doesn't have to be the same as the
parameter of the constructor.)

Now it's nice that it works but I have no idea why. And while it isn't
really urgent an explanation of that trace would be appreciated as it
could give some insight into the simplifier and what can lead to loops

> Tobias
> [...]

Christoph Feller

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