Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
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))
You should explain what "_ RS trivial" does. It is the conventional way
to let Larry's rule composition calculus do its normalization for you.
Admittedly this is not beautiful code. I just happened to have it.
What "thm RS trivial P" does is constructs the trivial theorem "P ==> P"
and then discharges its assumption using thm.
The point here is to specify the conclusion we want (Thm.mk_binop ...)
with the original cterm on the left hand side, construct a theorem with
that conclusion, and then "prove" it by resolution with a theorem we
have (which is alpha-beta-eta- equivalent). Yes, that is a big hammer to
apply, but it won't be applied all that often. The major cost here is
checking whether it is needed all the time.
Thinking in terms of "broken" and "fixed" is unwise. Which is actually my
main complaint on this thread.
Some things are neither broken nor fixed, they are just surprising, but
surprising for good reason. This is broken. As others have pointed out,
there is a clear contract for convs to follow so that then_conv can
chain them using Thm.transitive. This contract is not followed by rewr_conv.
This is one solution. An alternative would be to broaden the contract by
having then_conv catch the exception from Thm.transitive and switch to a
more general mechanism (possibly by doing the above). This might create
problems for some other consumers of convs, which I have not taken time
This archive was generated by a fusion of
Pipermail (Mailman edition) and