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



Am 23/10/2012 13:30, schrieb Makarius:
> On Tue, 23 Oct 2012, Tobias Nipkow wrote:
> 
>> I just tried my suggestion and it seems to break HOL. I'll investigate more.
> 
> I would have given it a > 50% chance of not breaking immediately, since
> rewrite_conv is relatively new back in Isabelle/HOL.

The problem comes from my matching code that eta-expands even if it does not
need to. Substituting such a matcher back into the pattern creates new
beta-redexes that were not there beforehand. This is more subtle than expected.

In contrast, it seems that Thomas' solution (fix_conv) does the job, but it is a
bit on the brutal side. I'll see if I can come up with something less brutal.

Tobias





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