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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
