Improve treatment of multiplication by constant in blastLib.

For example, testing with

BBLAST_PROVE ``x <+ 10w: word32 ==> x * n2w (2 ** 8 - 2 ** 4) <+ 2500w``

showed an improvement of 10.8s (before) to 0.53s (after).

Various tweaks to bit-vector development.

NOTE: It is possible that some bit-vector proofs may break, due to subtle changes in bit-vector simplification.

The selftest script now tests calls to WORD_GROUND_CONV. (This conversion's flag is also set to false for use outside of wordsLib.)

Some unused tools have been removed from blastLib.

Add blastLib.BBLAST_PROVE_TAC.

Added new operations for shifting by a bit-vector value, namely:

LSL: <<~
LSR: >>>~
ASR: >>~
ROR: #>>~
ROL: #<<~

These are supported by the procedures in blastLib. For example, one can prove

w <+ 10w /\ s <+ 3w ==> w <<~ (s + 1w) <+ 73w : word16

The time-complexity is a pretty shocking but "simple" 32-bit problems seem to
be okay. NB. ROR and ROL only bit-blast with word sizes that are a power of
two.

Added a new conversion WORD_MOD_BITS_CONV for mapping applications of
``word_mod w (n2w n)`` into ``(h -- 0) w`` where n is a power of two.

Also added support for bit-blasting arbitrary multiplication, but the word-size
limit is set to 8 bits by default. Things seem to be just about feasible with
that limit (and become horrendously slow after that).

To improve performance, the conversion BBLAST_CONV does not have exactly the
same coverage as before. For backward compatibility, a conversion
EBLAST_CONV (which calls SAT at every bit position) is now available.

Added Tactical.PRED_ASSUM. It's similar to PAT_ASSUM but uses a predicate to
pick the assumption.

Added blastLib.FULL_BBLAST_TAC, which attempts to use "blastable" assumptions.

Make blastLib.BBLAST_PROVE smarter with respect to counterexamples (existential
goals). For example,

> blastLib.BBLAST_PROVE ``?x y. x + y = 12w : word8``;
val it = |- ?x y. x + y = 12w: thm

is now possible, and we also have:

> blastLib.BBLAST_PROVE ``x < y = x <=+ y : word8``;
Found counterexample:

y -> 255w

and

x -> 0w

Exception- SAT_cex |- (0w < 255w <=> 0w <=+ 255w) <=> F raised

The printing of counterexamples is controlled by the trace
"print blast counterexamples".

Add BBLAST_PROVE.

Added a bit-blasting conversion: BBLAST_CONV. This goes beyond the
capabilities of WORD_BIT_EQ_CONV by expanding out additions / subtractions.
This allows the new conversion to automatically handle small but tricky bit
vector goals. For example:

``(x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w)``

and

``!a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w``

(These aren't provable with wordsLib.WORD_DECIDE.)

Obviously bit-blasting is a brute force approach, so the new conversion should
be used with care. It will only work well for smallish word sizes and when
there is only and handful of additions around. It is also "eager" -- additions
are expanded out even when not strictly necessary. For example, in

``(a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32``

the sum ``a + b`` is expanded. Users may be able to achieve speed-ups by first
introducing abbreviations and then proving general forms, e.g.

``x <+ c /\ c <+ d ==> x <+ d:word32``

The conversion handles most operators, however, the following are not covered /
interpreted:

-- Type variables for word lengths, i.e. terms of type ``:'a word``.

-- General multiplication, i.e. ``w1 * w2``. Multiplication by a literal is
okay, although this may introduce many additions.

-- Bit field selections with non-literal bounds, e.g. ``(exp1 -- exp2) w``.

-- Shifting by non-literal amounts, e.g. ``w << exp``.

-- ``n2w exp`` and ``w2n w``. Also w2s, s2w, w2l and l2w.

-- word_div, word_sdiv, word_mod and word_log2.