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

Yours,
    Thomas.






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