Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
On Tue, 23 Oct 2012, Tobias Nipkow wrote:
"A conversion is any function that maps a term t to a theorem |-t==u."
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and