[isabelle-dev] Problem with let-simproc

[Johannes Hölzl]

Hi Thomas _Sewell_,

no no don't worry, the report was from Thomas _Tuerk_! And the change
was not too hard to produce.

What were your problems with the let-simproc? Did it to much or not
enough unfolding?

 - Johannes

Am Donnerstag, den 07.02.2013, 11:34 +1100 schrieb Thomas Sewell:
> 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.
> 
> Yours,
>      Thomas.
> 
> 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
> >>> 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
> >
> >
> >
> >
> >
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>