Make global simpset state easier to recreate with "logged_update"

This entry-point records that a change to the global simpset has
happened within a piece of code (rather than a script). The change is
made (as before), but the change is also recorded so that it can be
recreated/applied to different base simpsets.

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

align numeric syntax: 'great' becomes 'greater' The earlier names are inconsistent with numSyntax and less descriptive.

The changes are:
intSyntax.great_tm -> intSyntax.greater_tm
intSyntax.dest_great -> intSyntax.dest_greater
intSyntax.mk_great -> intSyntax.mk_greater

int_arithTheory.add_to_great -> int_arithTheory.add_to_greater

realSyntax.great_tm -> realSyntax.greater_tm
realSyntax.dest_great -> realSyntax.dest_greater
realSyntax.mk_great -> realSyntax.mk_greater

github issue #629

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

More work on getting better simplification/normalisation over reals

Change "thm-names" (used in various places) to be Thy-Name record

This saves on pulling things apart and looking for dots and the like.
It changes the simpLib API (most significantly for the SSFRAG function
which builds simpset fragments).

Add canonicalisation convs for real addition and multiplication

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

Give theorems names in simpsets

This is to allow them to be removed easily. System builds on -t1, but
there are still two things to be done

1. the names associated with export_rewrites calls aren't passed on to
the simpsets yet
2. there is not yet an API for removing them

Also, perhaps just as an interim measure, I removed the unused
entrypoint for removing rewrites by pattern matching against their
LHSes (simpLib.remove_theorems).

Remove eqtype declaration for term type

Provide support for evaluating float to int and real to int operations.

For example, the following weren't working before (with intLib and realLib loaded):

EVAL ``NUM_FLOOR (-0.5)``; (* |- flr (-0.5) = 0 *)
EVAL ``NUM_CEILING 0.5``; (* |- clg 0.5 = 1 *)
EVAL ``INT_FLOOR 0.5``; (* |- flr 0.5 = 0 *)
EVAL ``INT_CEILING 0.5``; (* |- clg 0.5 = 1 *)

Improvements to evaluation coverage for realTheory.

Previously, the follow terms were failing to evaluate:

``sum (1, 4) real_of_num``
``1 > 1 / 2``
``1 >= 1 / 2``
``flr (232 / 3)``

The operation "sum" is now introduced using Define.

Evaluation was not occurring for terms such as ``1 / 2 * 0r`` and ``0r * 1 / 2``.

Fix calculation bug (see test).

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

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.

Changed a couple of misleading/annoying names. The type ssdata is now
called ssfrag (to bring it into line with documentation that talks about
simpset fragments), and the constructor SIMPSET is now called SSFRAG.
It never created a simpset, so the latter was a stupid name.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

Follow-on to the change to the pre-processor. There's a significant
problem, in that the heretofore standard way of protecting a
piece of code from alterations to the grammar(s) used to parse
terms in that piece of code ... no longer works after the change.

The previous recommendation was to re-bind Type and Term with

val (Type,Term) = Parse.parse_from_grammars <grms>

which allowed subsequent

Term ` .... `

to parse with the specified grammar. However, also

`` ... ``

would subsequently use the specified grammar as well. But I
changed the pre-processor, and this broke the usage of

`` ... ``

with the specified grammar.

The fix is to do as in src/real/RealArith.sml: get the
ambient grammar, set the desired grammar, execute the
body of code, then reset to the ambient grammar. Works
provided the code doesn't alter the grammar.

This probably needs to be documented in a more visible place,
once Michael comments.

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.

My last check-in broke the building of the n-bit word theories (should
always try the -selftest option to build to catch this) because the
implementation of relevance analysis didn't believe that SUC a <= 2 ** WL
was relevant to proving 0 < 2 ** WL. The solution is to realise that
even ground terms may end up being treated as variables by decision
procedures. So, there is now an additional parameter to RCACHE : a function
that takes a term and returns a list of terms that should be treated
as free variables in the relevance analysis.

A better cache function, RCACHE that does relevance analysis to speed
up the rejection of formulas that are sure to fail.

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

Add handling of absolute value terms to the "reduce" simpset.

REAL_REDUCE_ss wasn't reducing (ground) terms of the form
max 0 <somenumber>
or terms with min, either.

REAL_REDUCE_ss was reducing more than just ground formulae.
Also, be slightly more careful about rewrite generation to avoid
duplicates.

Added DIVMOD to arithmeticScript, which helps complete the suite
of generated code. Unfortunately, arithmetic then depends on pairs,
which I had been trying to avoid, for purely aesthetic reasons.

Also fixed up more of the ML code generation business.

Changed NUMERAL_BIT1 and NUMERAL_BIT2 to BIT1 and BIT2, respectively.
Sorry, they were just too long. Also, ALT_ZERO is now named ZERO.

Make the real arithmetic decision procedure available as a (cached)
procedure inside the simplifier. Just include REAL_ARITH_ss to see
ARITH_ss-like simplifications made to terms involving linear real
arithmetic.

Handle exponentiation in the "real reduction" functionality. Done through
one big rewrite theorem (pow_rat) proved in realScript.sml.

When a library file uses the parser, must must must must must include a line
specifying which grammars to parse with.

Provide elimination of common factors, and also properly extend real_ss
so that it does real number reductions, and doesn't just leave calculations
halfway through, waiting for natural number reductions to fire.
Unfortunately, this does break one of Joe's probability proofs, which
relied on seeing SUC 0, rather than 1. Fixed this too.

Make specialisations more specific (pick &(NUMERAL n) and ~&(NUMERAL n)
instead of just &n and ~&n), and also include the x/x = 1 rewrite for
non-zero x.

First cut at calculation with the reals. Doesn't include a treatment of
exponentiation, nor does it eliminate divisors in fractions. Updates
stateful rewriter and global compset, so that EVAL will do calculations
with fractions.
Am about to go home with build just in the middle of probability. If
I've broken anything, apologies! Fix the bug by commenting out
++ REAL_REDUCE_ss
in the definition of real_ss in realSimps.sml

Little more progress with this stuff.

Moving towards calculation with the reals.

A really useful theorem about supremums: for any 0 < e, you can
always gets within e of the supremum.

More real simplifications, and more theorems about pos, max and min.

As predicted, I need a few more simplifying rewrites.

Finally got around to fleshing out the real simpset (the other changes are
the ramifications of this!)

Major changes:

1. Got rid of AC rewrites for + and *. If you want them (perhaps for
compatibility with the old real_ss), use real_ac_ss.

2. Added a huge bunch of useful rewrites to real_ss, though I'm sure
I'll need to add a huge bunch more before I'm finished with it.

Changing arithLib to numLib. And RealSS to realSimps.