Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
On Tue, Oct 23, 2012 at 3:21 PM, Lawrence Paulson <lp15 at cam.ac.uk> 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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and