Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue

My guess (I don't have time to study the code) is that this will perform beta-eta normalisation.

As a historical remark, I'm quite attached to conversions, which were the topic of my very first journal article:

L. C. Paulson. 
A higher-order implementation of rewriting. Science of Computer Programming 3 (1983), 119–149.

They made a lot of sense in the context of LCF and HOL, where users routinely wrote code as part of the verification process. Although I included this code in Isabelle, it didn't have a central role and I thought it'd got deleted. Obviously it would be sensible to correct any deficiencies or omissions. But I'm still intrigued regarding what sort of application you could have for them.


On 23 Oct 2012, at 12:27, Makarius <makarius at> wrote:

> On Tue, 23 Oct 2012, Peter Lammich wrote:
>> So what normalizations does instantiate_normalize do (beta?, eta?,
>> beta-eta?, how deep?). Looking at the source code does not really help
>> here:
>> fun instantiate_normalize instpair th =
>> Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR
>> asm_rl);
> Larry should be able to tell you.
> It is again the same technique to let rule composition perform some normalization.  The above function goes back to Stefan Berghofer, IIRC. I merely changed its name Drule.instantiate ~> Drule.instantiate_normalize recently, to make it a bit more explicit what was meant here.
> 	Makarius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.