Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Get core HOL to build with new definition of "by"

Progress with github issue #407

Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

Fix integer theories in light of pat_assum rename

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.

Add an embodiment of the Omega d.p. for use inside the simplifier. It
can perform quite badly on goals with too many disjunctive assumptions
(and ~(x = y) counts as a disjunction).

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.

Add more aggressive normalisation of multiplicative expressions to ARITH_ss.
Also provide old_arith_ss values for scripts that don't want this new
behaviour. Update proofs to go through again. Some should be a bit more
robust in the face of future changes to arith_ss. Others just punt and refer
to old_arith_ss.

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.

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

A fix for the bug in AC-rewriting. Thanks to Tobias Nipkow who showed
me the ordering function used by Isabelle. A few changes needed to be
made to the integer theory scripts to cope with the changed behaviour.

Sorry to have broken the build. By way of recompense, here's my
independent fix for the problem (checking it in over Joe's because it's
shorter).

Fixed the build.

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 now works on all of the test case, bar KXSDIV1, on which it
blows up. Some investigation suggests that this is "just" an efficiency
issue and not one of code correctness. With luck, I'll check in some
efficiency changes tomorrow, and then I'll be done.

Very close to a complete symbolic method.

New proof of the principle that lets me turn
0 <= nx + c
into
0 <= x + c/n
and a corresponding change in the implementation of gcd_check in OmegaMath.

Omega equality elimination done. Some new supporting theorems required.
Is a bit slow, so will need to profile quite a bit to see just what's
wrong.

Added file that will be basis for implementation of Omega Test for
Presburger arithmetic. (Also push a divisibility theorem into core
integerTheory, and slightly change it.)

Fairly extensive modifications to give integerTheory two division functions
(and each gets a corresponding mod function too). They are int_div (int_mod)
and int_quot (int_rem). All are abbreviated by the printer-parser:
int_mod : %
int_div : /
int_rem : rem
int_quot : quot
The behaviour is as for the SML constants of the Basis Library's Integer
structure. Most theorems about one function have analogous theorems in
the other camp. Cooper's algorithm modified to work with int_div and
int_mod. I haven't made it work over the other pair, though I probably
should at some stage.

More reorganisation, mainly to remove listTheory as an ancestory wherever
possible (it still persists as a necessary ancestor of CooperCore, but
isn't used un-necessarily elsewhere).
Also sped up phase5 of CooperCore some more.

New constant called bmarker used to mark certain boolean valued terms
as interesting; allowing for simple rewriting to move these terms
about within a conjunction. Possibly should be earlier in the
distribution, as this technique could speed up UNWIND_EXISTS_CONV, which
currently uses AC_CONV to do no more than pull one conjunct to the
head of a term.

Added another useful theorem to this theory. It's an easy derivation
from existing theorems, but it's useful to have things "just so" when
applying theorems in the middle of a big proof procedure.
(Theorem is n | n * x + c = n | c )

Now builds, with successful proof of Cooper's first lemma for performing
"delta-elimination". Have already proved second lemma, so should now
be able to implement optimisation.

Gotta go home; part-way through proof of delta-elimination lemma for
Cooper's algorithm.

Changing arithLib to numLib.

Not going to change this anymore. Instead I'm going to write about how
well it performs. Many improvements since last time, and a little
more code factorisation as well. Code should be easy to adjust to
use full gcd optimisations in future for pure goals.

In dividesScript:
* change DIVIDES_REF to be DIVIDES_REFL
* prove DIVIDES_TRANS
In gcdScript:
* eliminate a duplicate copy of GCD_0L
* prove an efficient rewrite for calculating gcds with computeLib
In intSyntax:
* add {mk_,dest_,is_}injected functions
In int_arithScript:
* prove a couple more useful theorems for dealing with gcds
In integerScript:
* prove that x int_divides 1 = (x = 1) \/ (x = ~1)

Further speed improvements. Average of about 17% quicker. This comes
mainly through not converting to NNF and the search for equalities to
eliminate is now also more sophisticated.

Cooper now can eliminate on the a's or the b's. Currently though it's
forced into just the a's to test that part of the code, and there may
be something very strange happening with the pt11 example.
int_arith has picked up some new theorems to support all this.

Added can_get_big theorem (a version of can_get_small really, as its short
little proof makes clear).

New theories of number theory (divides, prime, gcd) and a simple
optimisation in Cooper that divides leaves through by the gcds of
variable coefficients.

New theorems about gcd and eliminating coefficients for use in Cooper.

Reimplemented REDUCE_CONV in intSimps, by making it use computeLib
directly. This should speed it up. Many _REDUCE theorems needed for
this additionally proved in integerScript.sml. int_arithScript has
just had a couple of minor tidy-ups.

Made it all Kananaskis compatible.

Decision procedure now keeps equality terms rather than normalising
them away, and seems a deal quicker as a result, though its
performance on pt7 has worsened by at least a factor of two. This
will bear investigating.

Added better rewrites for ODD and EVEN over :num, and also the (now unused
HO_SUB_ELIM).

Functionality updates for Cooper.sml. Still inefficient though. Code
in comments is start of attempt to improve this.

Purely notational changes. I thought the name "COOPER_CONV" would be
catchy ...

Modifications now mean that decision procedure works over naturals as
well.

int_arith now exports a INT_ARITH_CONV and INT_ARITH_PROVE that
implement smart integer decision proving. In particular, it attempts
to prove things that aren't pure Presburger, by generalising out
bad terms.

Fixed a number of bugs and improved performance quite considerably.
Performance tweaks could continue indefinitely from this point, but
I think my time would be better spent on broadening the scope of the
code I have.

Files for Cooper's algorithm, an implementation of a decision procedure for
all of Presburger arithmetic, including arbitrary quantifier nesting and
alternation.
* int_arithScript.sml generates a theory with the pre-proved theorems
needed for the algorithm. None of them are really very interesting
in themselves, so don't really deserve to be in integerTheory itself.
* int_arith.sml actually implements the algorithm.
The procedure only works on formulae with no free variables and doesn't
handle non-Presburger sub-terms at all. Future work will fix these two
problems.