[isabelle-dev] Probable bug in let_simp simproc

[Makarius]

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