fix proofs by reducing stateful simpset

Strengthen length_zero_extend and length_sign_extend

Get src/n-bit to build given tight-equality

Generalise bit-string theorem.

Fix more proofs for #346

Tweak automatic rewrites for TAKE and DROP

The previous rewrites introduce COND (if), which is often undesirable.
The new rewrites are more constrained but desirable in more contexts.

See https://sourceforge.net/p/hol/mailman/message/35184168/

Further simplify n2v.

Simplify definition of n2v.

Also remove semicolons.

Add a new conversion and simpset fragment for bit-strings.

Opening lcsymtacs is no longer necessary.

All l/case short simp tacs use LET_ss + ARITH_ss

This means that fs and rfs pick up LET_ss and ARITH_ss, making them
indistinguishable from the 'l' versions.

Ensure the bit-string rotate operations is well-defined on empty lists.

Remove unnecessary application of fixwidth.

Fix for the definition of bit-string rotate.

Bit-string were being padded when rotating by zero.

Also improve wordsLib.WORD_GROUND_CONV.

Support building custom compsets that cover bitstringTheory and integer_wordTheory.

Add a bit-string rotate operation.

Fix a couple of proofs broken at a9c9add.

Move bitTheory into src/num/extra_theories and move evaluations theorems in wordsLib further up the build sequence.

Includes some tidying-up work.

This closes issue #120. Evaluation for "toNum" and "toString" can now be enabled by loading up stringLib (or, more precisely, ASCIInumbersLib), without the need to load up wordsLib.

This check-in can be viewed as finishing off the (many) loose ends left over from work on issue #70.

Overhaul to rich_listTheory (it had become a bit of a disaster area).

Some points:

1. rich_listTheory now uses the same constant names that are used in listTheory, e.g. TAKE instead of FIRSTN.

2. listTheory theorems are no longer replicated (saved again) in rich_listTheory. This avoids DB.match returning multiple instances of the same theorem. It also avoids saving around 100 theorems twice — in some cases after re-proving them.

3. Compatibility is now maintained though a bunch of SML "val" assignments added using adjoin_to_theory, e.g.

val ZIP_FIRSTN_LEQ = ZIP_TAKE_LEQ
val ALL_DISTINCT_SNOC = listTheory.ALL_DISTINCT_SNOC

4. Some incompatibilities are introduced:

* FRONT___LENGTH is deleted, since it is the same as rich_listTheory.LENGTH_FRONT.
* COUNT_LIST___ADD -> COUNT_LIST_ADD
* COUNT_LIST___COUNT -> COUNT_LIST_COUNT
* The compute theorems for COUNT_LIST and SPLITP have been renamed.
* Some other theorems are no longer saved, e.g. rich_listTheory.list_INDUCT

5. Some theorems in listTheory have gained quantifiers.

Move n2l and l2n constants (and similar) into new numposrep theory.

A number of fixes follow on from this.

Also mention the new theories (numposrep and ASCIInumbers) in the release notes.

This is progress with #70.

Move ASCII numbers stuff from bitTheory to ASCIInumbersTheory in src/string.

Rather bloody surgery at this point. There may well be rough patches
remaining. A number of knock-on effects in src/n-bit, as well as the
movement of a nice rewrite about LOG into logrootTheory.

This is progress with #70

change interface to add_persistent_funs (#73) and fix more calls

The new interface takes a list of strings naming theorems.
(The old interface took a list of (string * thm) pairs.)
The new way better ensures consistency of theory development and theory
load behaviour: you can no longer pass a name with a theorem that isn't
actually saved under it.

Theorems are looked up with DB.theorem, or failing that, DB.definition
or DB.axiom.

Alas, I found more examples using add_persistent_funs to add theorems in
ancestor theories. Rather than modify the ancestor theories, I have
opted to make the offending theories save the theorems they want to add
to computeLib themselves so they have a name in the current theory to
pass to add_persistent_funs.

If this behavior was appropriate for patricia too (da47401) change it.
Alternatively, if the ancestor theories should have exported those
things for computeLib anyway, search this commit for new instances of
"save_thm" to see what needs fixing.

Two more theorems in bitstringTheory.

Generalize field_concat_left theorem.

A couple more bitstring theorems.

Add a theory of bit-strings, which defines word operations over ``:bool list``. The maps "v2w" and "w2v" provide a connection to fixed-width bit vectors.