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.