# 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
```
```
```
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.

```

• References:

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