Stop REAL_RAT_REDUCE_CONV diverging on rational literals

[lukaszcz]

The bug

REAL_RAT_DIV_CONV rewrites x / y to x * inv y and back, so on a
literal already in lowest terms it returns |- &1 / &3 = &1 / &3 —
success, no change. computeLib re-evaluates whatever a registered
conversion hands back, so CBV_CONV went round that term forever:
REAL_RAT_REDUCE_CONV did not terminate on any term containing a
non-integral rational literal.

The fix

real_rat_compset already guarded one entry — REAL_RAT_NEG_CONV —
with CHANGED_CONV. Several of the others are no-ops on an
already-reduced argument in the same way, so the guard belongs on every
entry rather than on whichever operator's no-op was noticed first. The
compset now adds all of them through a single add_reduce_conv that
applies it.

A registered conversion can report no progress in two ways: return a
reflexive theorem, or raise UNCHANGED (as ALL_CONV, hence
TRY_CONV, does). Both are fatal — the first loops, the second escapes
CBV_CONV entirely, because reduce_cst catches only HOL_ERR when
deciding to move on to the next rule. Conv.CHANGED_CONV covers both,
so it needs no QCHANGED_CONV around it; QCHANGED_CONV in its place
would be a regression, since it catches only the raise and lets the
diverging mode through. A comment at the site records this so the
question is not reopened.

Tests

src/real/selftest.sml gains a test that the conversion terminates on
&1 / &3 * x, plus a companion pinning that &1 / &3 + &1 / &6 still
reduces to &1 / &2 — so the termination guard cannot be satisfied by
simply disabling reduction.

Scope

This is the instance half of #2034. The underlying computeLib
mechanism — reduce_cst counting a reflexive result as progress — and
the add_conv documentation that never stated the contract are
deliberately left alone here.

[mn200]

Both new selftests should use convtest; only one does at the moment.

[lukaszcz]

Both new selftests should use convtest; only one does at the moment.

Fixed

[mn200]

Thanks!