Fix bug in integer d.p.s' handling of ODD/EVEN.

Include test-case.

Rewriting of ODD now uses

|- ODD n <=> ?m. n = 2 * m + 1

rather than

|- ODD n <=> ~(2 int_divides n)

because in the latter, the elimination of natural number subtraction
can't get to grips with the "isolated" argument n.

Closes #437

Make the integer decision procedures handle maximum and minimum.

This works for :num and :int. In both cases, the treatment is to
expand with the definition of the relevant constant.

Bug-fix in integer self-tests.

Bug was caused by change to Timer structure.

Add a couple of test-cases. Mike2 used to cause the bug that I just
fixed in Cooper's algorithm.

Bug-fixes and test-cases from problems in src/rational.

Add some pre-processing code so that the decision procedures can
handle the Num constant, which coerces from integers to natural
numbers. Changes to intSyntax include adding {mk,dest,is}_Num and
also dest_absval.

I think this is a bug-fix. Now the SEND MORE MONEY test case takes
four hours to raise an exception instead of just a minute. I've taken
it out of the test cases list. I can't easily come up with a test
case that proves this is a bug, but it seems plausible that it is.
(Now I'm going to have to implement that "combine with DPLL d.p.")

Send more money problem should require leading digits not to be zero.
(Still breaks Cooper's.)

Add a test case for Cooper's algorithm corresponding to the

S E N D
+ M O R E
----------
M O N E Y

puzzle. This causes it to break. Don't bother testing it with Omega
as all the inequality constraints would force DNF normalisation to
generate 2^28 clauses. (Hope to fix Cooper in the near future.)

Implement improved handling of integer div and mod, along lines already
done for natural number operations. This allows Omega to prove John Matthew's
example, recently posted to the Isabelle mailing list, in half a second.
(Cooper seems to fail miserably.) Added this example (in four variants)
to the test case suite.

Ahem, shouldn't try to write these things out from memory.

Another test case for Omega's new handling of MOD and DIV. From my work
on netsem, a fact to do with sign-bits being zero (imagine 100000 being
2^31).

Implement some improvements to the pre-processing of natural number goals
such that OMEGA can now prove goals of the form
(x MOD c + y MOD c) MOD c = (x + y) MOD c
in reasonable time. Cooper can't, unfortunately, so the test case for the
above (with c = 1001) is added to a new class of examples that are only
tried for Omega.

Multiplication normalisation bug fixes, along with a couple of extra bugs
picked up along the way recorded in the test cases.

Introduce Alexey Gottsman's test case to the integer and natural number
arithmetic decision procedures regression test suites. Now, selftests
fail. Fixes forthcoming.

A fix for my "natural number goal" bug. (And a new test case for no
particularly good reason.)

The integer decision procedures don't handle natural number assumptions
properly: the new goal added to the list here raises an exception.

Fix for bug 964085 (to do with DIV/MOD expressions nested inside
themselves). Also made the procedure cope with the presence of
?! quantifiers with scope over DIV/MOD expressions. Added test cases
to demonstrate. Unfortunately, the example I chose in the bug report
above produces a goal that takes too long to solve (the bug was in the
production of the goal), so my exemplar of the bug in the regression
test suite is instead
(x MOD 2) MOD 2 = x MOD 2
which is rather less interesting.

A fix for the bug reported in hol-info by Arthur van Leeuwen. Also
extended the testing programs to be able to check goals (like the one
he provided as an example).
The problem is that his goal had an assumption where the
non-presburger sub-term was in the scope of a universal quantifier.
(If it was a existential then it could be pulled out, turned into a
universal, stripped, allowing access to the non-presburger sub-term
so that it could be generalised away.) The conversion still doesn't
cope with this situation, but the tactics now won't attempt to include
assumptions that look like that.

Added some test cases due originally to JRH (via Konrad) and discovered
a bug in Cooper's handling of conditional expressions. Fixed the
problem by making some code from IntDP_Munge visible.

Fixed a bug found by Mike. Problem stemmed from the routine that
normalised multiplicative terms, which was supposed to do things
like p * k * 2 --> 2 * (k * p).
The code did this fine on natural number formulas, but was doing the
wrong thing on integer formulas because a DEPTH_CONV of it would wrap
non-multiplications in a multiplication by one. This multiplication by one
was relied on elsewhere though, so the sum-normalisation routine needed
tweaking as a result. In testing/ there are two new test cases, the
natural number version worked before, but the integer one did not.

Fixed a bug in the normalisation routine; it wasn't handling the
possibility that it might return ?x. F. New addition to test_cases is
the example that tweaked this bug; thanks to Joe and Konrad for
coming up with it.

Omega now passes all of its tests, and I claim it's probably now a reasonable
approximation of a complete procedure for doing Preburger arithmetic.
Aggressive preprocessing attempts to minimise DNF blowup, but the fact
that EXISTS_OR_CONV can still consume over 10% of the procedure's running
time basically sucks.

OMEGA_CONV is now "almost complete". There are just bugs to be ironed out.
Changes are too many to document extensively. Some though:
* OmegaMath has got a lot bigger, with OmegaEq being merged into it and
also gaining some divisibility normalisation code.
* couple of new test cases
* decided against prenexing mixed quantifier problems.

Konrad found a bug: elimination of subtraction has to happen after DIV
and MOD are eliminated so that terms of the form (x - y) DIV c are
handled properly. Added a couple of test cases to demonstrate the bug
in the old version.

Reorganised test programs so that regression suite is shared between
omega and cooper tests. Also added useful Perl program for doing
comparisons between test runs.