Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
On Tue, 23 Oct 2012, Thomas Sewell wrote:
An additional beauty of the Isabelle library is how often you get to
build your own primitives because none of the existing ones do what you
I have this sitting around somewhere:
fun fix_conv conv ct = let
val thm = conv ct
val eq = Logic.mk_equals (term_of ct, term_of ct) |> head_of
in if (term_of (Thm.lhs_of thm) aconv term_of ct)
else thm RS trivial
(Thm.mk_binop (cterm_of (theory_of_cterm ct) eq) ct (Thm.rhs_of thm))
That fixes the problem with rewr_conv, so fix_conv Conv.rewr_conv does
what you would expect Conv.rewr_conv to do.
You should explain what "_ RS trivial" does. It is the conventional way
to let Larry's rule composition calculus do its normalization for you.
Thinking in terms of "broken" and "fixed" is unwise. Which is actually my
main complaint on this thread.
This archive was generated by a fusion of
Pipermail (Mailman edition) and