[isabelle-dev] Problem with let-simproc

[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