Re: [isabelle] rewr_conv

After a false start and some experiments I have now converged on (essentially)
Thomas' solution, but integrated into rewr_conv. It lets resolution do the work
and is thus immune against funny matchers. No point in doing anything cleverer.
No theory in the distribution or the AFP were affected and Peter's example works
fine now.


Am 24/10/2012 05:14, schrieb Thomas Sewell:
>>> 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.