I'd forgotten I'd ever reported this to you.

My problems with let_simproc run a little deeper anyway, and I've moved to a different approach in the meanwhile. Sorry if I've left you labouring on my behalf.


On 07/02/13 02:38, Johannes Hölzl wrote:
Am Mittwoch, den 06.02.2013, 12:25 +0100 schrieb Makarius:
On Tue, 5 Feb 2013, Johannes Hölzl wrote:

there is a bugproblem with the let-simproc, resulting in a non
terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of

  theory Scratch imports Complex_Main begin

  lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X"
    using [[simp_trace]]
    apply simp

The attached hg-bundle changes this behaviour to a terminating simproc.
(The bundle can be applied to a repo containing #58e2d0cd81ae by
"hg pull let_simp_betaeta.bundle")

It currently runs in the testboard:

@Makarius: Is it possible to include this patch in Isabelle2013, when
the testboard run is green?
Testboard does not test very much, compared to what has been tested
manually and semi-automatically in the past 2 weeks for the release.  AFP
would also have to be covered.

Anyway, this behaviour of let_simproc seems to have been there from its
beginning, or at least back until Isabelle2011 (what is what I have
tried). Nobody has noticed a problem in several years, so this change is
for the next release, unless there are really strong reasons to revisit it

Thomas reported the problem to me. For me it is okay to fix it after

@Thomas: Is it important for you to fix it in Isabelle2013? I hope the
workaround with adding Let_def to the simplifier should work fine. Then
I will add it just to the development version of Isabelle.

  - Johannes

isabelle-dev mailing list

isabelle-dev mailing list

Reply via email to