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



I just tried my suggestion and it seems to break HOL. I'll investigate more.

Tobias

Am 23/10/2012 13:17, schrieb Makarius:
> On Tue, 23 Oct 2012, Tobias Nipkow wrote:
> 
>> "A conversion is any function that maps a term t to a theorem |-t==u."
>> LCP, 1983
>>
>> up to beta-equivalence. Since conversions are low-level proof methods which
>> are sensitive to the precise term structure, this is a wart that causes
>> non-modularity. This non-modularity only shows up (to refine Brian's analysis)
>> if the lhs of the rewrite rule has a free variable F in an applied position: F
>> t. This does not happen very often, but if it does, rewr_conv should still
>> behave nicely. It should do a non-normalizing instantiation followed by a
>> beta-normalization.
> 
> Alternatively one could do the normalization before on the input term.
> Empirically, higher-order matching can produce surprises if applied to terms
> with beta redexes, it normally is never used like that in the existing tools. 
> So it is better not to give non-normal stuff to the match operation.
> 
> Again, I don't expect too many fundamental problems in this rather small
> incident, but one has to approach it with the proper mindset about how the
> Isabelle code base (and its history) works.
> 
> (Next time I will tell a story how an efficient and fully verified merge-sort
> function included in the core sources caused several days of worries.)
> 
> 
>     Makarius





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