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

That application is very interesting! And one can argue that a simproc is a very similar concept as a conversion, anyway.


On 23 Oct 2012, at 14:41, Brian Huffman <huffman at> wrote:

> On Tue, Oct 23, 2012 at 3:21 PM, Lawrence Paulson <lp15 at> wrote:
>> 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.
>> Larry
> I can't speak for Peter, but I am currently using conversions in a few places.
> My main application is for writing simprocs: See e.g.
> HOL/Tools/group_cancel.ML or nat_arith.ML. Rewriting these
> cancellation simprocs to use conversions made the code significantly
> shorter, simpler, more efficient, and more reliable. There used to be
> a few simprocs that would sometimes return an equation whose
> left-hand-side did not match the input term; using conversions ensures
> that this will not happen.
> I would definitely recommend conversions to anyone thinking about
> writing a simproc.
> I am also using conversions inside the transfer package, to do some
> preprocessing steps. For this purpose, conversions are more
> predictable and more customizable than using the simplifier.
> - Brian

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