Fix printing of boolean negation after numeric types are loaded

If you have a term ~p /\ q, it should print as ¬p ∧ q (assuming
Unicode is enabled).

This wasn't true previously because of the dance around use of ~ as
numeric negation. The desired behaviour:

Parsing:

~ is preferentially parsed as boolean negation
¬ is only parsed as boolean/word negation
- (unary) is only parsed as numeric negation

Printing (with Unicode):
~ is never printed
¬ is printed for boolean/word negation
- (unary) is printed for numeric negation

Printing (without Unicode)
~ is printed for boolean/word negation
- (unary) is printed for numeric negation

Inspired to fix by reporting of issue #871

Fix a bug in normalisation of ℝ-multiplication

Use of MATCH_MP caused avoidance of variables occurring in assumptions
and introduction of unwanted priming. Assumptions can get pulled in
to goals through the use of arithmetic decision procedures that suck
in everything they think might be relevant.

Closes #844

Ensure ℕ and ℝ dp's have different names when embedded in simplifier

Now they are NUM_ARITH_DP and REAL_ARITH_DP, which are the names to
use when "Excl"-uding them from simplifier invocations. The
NUM_ARITH_DP also does normalisation over additive ℕ-terms.

Fix a MULRELNORM instance: 2 * x = inv 2 * y should canonicalise

Fix a REALMULCANON bug to do with inv applied to real literals

Further fixes (with tests) to ℝ-multiplication-normalisation

More ℝ-normalisation, removing inverted factors where possible

Previously, the code would collect up

...x... <= ... x...

for various possible exponents of x, but the normalisation would only
trigger if the x was present on both sides. Now, if the exponent is
negative, a lone x will shift to the other side of the relation
regardless.

This applies also to fractions, so that

x <= 3/4 * y

will turn into

4 * x <= 3 * y

Fixes in src/probability and more explicit regression tests.

Make ℝ-relation-normalisation first canonicalise arguments to rel'n

Fix canonicalisation of terms with leading fraction coefficients

Further extend normalisation of multiplications on ℝ

In particular, fractions are handled better so that something like

4 * x * inv 2

will turn into

2 * x

Also normalise so that something that would otherwise appear as

-1 * (f1 * f2 * ...)

will become

-(f1 * f2 * ...)

Further improve ℝ normalisation

More test-cases, more automatic rewrites, better code.

Normalise ℝ multiplications on either side of relation symbols

This can factor out things like

8 * x <= 12 * y ~~~> 2 * x <= 3 * y

as well as

x pow 10 * z < y * x⁻¹ pow 6 ~~~> x pow 16 * z < y

though the latter relies on being able to discharge the side condition
that x <> 0.

Put into srw_ss() and problems arising fixed

Tweaks to multiplicative normalisation over ℝ

Includes some new automatic rewrites

Add RMULCANON to automatic simplification

Builds up to selftest level 1.

Extend/improve REALMULCANON normalisation

Add canonicalisation convs for real addition and multiplication

These should be included in default simplification for the real
numbers.

Fix pretty-printing of real and relation inverses

Now both get to keep their pretty superscript forms (-1 for the reals,
and T for the relations) even when both theories are loaded. The cost
is that neither will be printed as "inv" when unapplied to arguments,
instead appearing as "realinv" and "relinv" respectively.

Closes #481

Tidy up some selftests, making output prettier

Mention bug fixed in 730f9a26a in release notes.

Also add regression test for this bug in src/real.

Fix calculation bug (see test).

Adjust a whole bunch of selftests to use Unicode at zero. In some
cases this is just for the sake of prettiness (making columns line
up), but in others, where the test is of the pretty-printer, I didn't
want to alter the tests.

Fix a silly hole in the automatic simplification of real number arithmetic.

Fix a number of calculation bugs, mostly calculations involving zero.
The new tests all used to fail.

Real number reduction wasn't working on terms of the form
0 = x / y
or
x / y = 0
Fixed, and test added to selftest regression.

The problem was that we weren't reducing double negations. Now fixed.

Remove an unnecessary loading message, and add regression tests for
calculation over the real numbers. Discover a bug in the handling
of abs thereby. Fix to follow.