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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
