[isabelle-dev] Probable bug in let_simp simproc

[Thomas Sewell]

Thanks Makarius, this entry explains a lot.

The NEWS entry in the changeset I found (1b257449f804) simply says:

* Simplifier: simproc for let expressions now unfolds if bound variable
occurs at most one time in let expression body.  INCOMPATIBILITY.

Thought that was all I was going to find. It seems I'm still learning how to read the sources the proper way.

This longer entry more or less answers the question. The strategy is to expand let x = v in f x if it allows simplifications of f v which were not possible with f/v seperated. A consequence of this is possible term explosion. I'll keep deleting the simproc from my simpset and try to implement a mechanism for allowing these simplifications that's specific to my problem.

Yours,
    Thomas.

________________________________________
From: Makarius [makarius at sketis.net]
Sent: Thursday, August 11, 2011 10:08 PM
To: Thomas Sewell
Cc: isabelle-dev at mailbroy.informatik.tu-muenchen.de; norbert.schirmer at dfki.de
Subject: Re: [isabelle-dev] Probable bug in let_simp simproc

On Thu, 11 Aug 2011, Thomas Sewell wrote:

> I spent a bit of yesterday trying to discover why the standard simpset was
> taking forever to simplify a large term I happen to have.
>
> The term is folded down in such a manner that unfolding Let_def will cause it
> to grow extremely large, which turns out to be what is happening. Deleting
> the let_simp simproc from the simpset solves the problem.
>
> The let_simp simproc is written in two halves. The first bit I can easily
> understand, and if I produce a simproc with just that code it does what is
> expected.
>
> The second half is commented "Norbert Schirmer's case", and is
> incomprehensible to me at the moment. Does anyone know, broadly, what it is
> meant to do? If I knew that I might be able to figure out what the problem
> was.

Here are some further clues from ancient history:
http://isabelle.in.tum.de/repos/isabelle/rev/761a4f8e6ad6

In particular the NEWS entry:

* Simplifier: new simproc for "let x = a in f x".  If a is a free or
bound variable or a constant then the let is unfolded.  Otherwise
first a is simplified to b, and then f b is simplified to g. If
possible we abstract b from g arriving at "let x = b in h x",
otherwise we unfold the let and arrive at g.  The simproc can be
enabled/disabled by the reference use_let_simproc.  Potential
INCOMPATIBILITY since simplification is more powerful by default.


        Makarius

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.