[isabelle-dev] Problem with let-simproc

[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