[isabelle-dev] Problem with let-simproc

[Johannes Hölzl]

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
> > isabelle-release):
> >
> >  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:
> >  http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c
> >
> > @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 
> now.
> 
> 
>  	Makarius

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

@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