[isabelle-dev] Probable bug in let_simp simproc
Makarius
makarius at sketis.net
Thu Aug 11 14:08:50 CEST 2011
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
More information about the isabelle-dev
mailing list