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 would expect.

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)
   then thm
   else thm RS trivial
(Thm.mk_binop (cterm_of (theory_of_cterm ct) eq) ct (Thm.rhs_of thm)) end

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.


	Makarius






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