Enhanced fcpTheory (FCP_FST, FCP_SND, FCP_CONCAT_THM, ...); moved duplicated HAS_SIZE to upstream

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

Fixes of bag, container, finite_map and in n-bit/

Set grammar ancestries in fcp and word theories

These are test cases for the new machinery

Clean up some code.

Make sure FCP_UPDATE doesn't get added to the_compset.

Clean up of fcpTheory. Also added a few new constants.

The new constants are: FCP_CONCAT, FCP_ZIP and FCP_FOLD.

The definition of V2L has changed — avoiding the unnecessary use of Hilbert choice. Also removed the sub1 type constructor. These were introduced in 102792de.

Fix hand-rolled case-constant in finite Cartesian product theory.

This is progress with github issue #97.

Pushing things so I can work on case constant flipping.

Remove theorems that are already available in listTheory.

Change fcp$HAS_SIZE to have fixity NONASSOC-450.

The 450 fixity level is standard for binary relations. The previous
level of 8 used for HAS_SIZE is so weak that it even works badly with
the propositional connectives, forcing things like

... /\ (s HAS_SIZE n) /\ ...

Further extend the bounds generation under WORD_DECIDE. For example, can now
prove:

wordsLib.WORD_DECIDE
``((4w * (3 >< 1) b + 10w) << 2) // 3w <+ 57w :word16``

Also added WORD_EXTRACT_ss to WORD_CONV. Unfortunately this can break proofs.

Remove unnecessary antecedent to a theorem.

Add evaluation support for FCP index and update. This has required fixing
a problem with the evaluation of EL, namely EVAL ``EL i x`` didn't terminate.

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!

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

Free the name "index".

Two extra theorems produced for the benefit of
examples/acl2/ml/translateTheory

Temporary change to get the theory to build. Probably
mn200 will want to change names to "array" versions,
but I'll leave that to him.

Demonstrate that arrays are an algebraic datatype, though this isn't
as much use as we might like because our datatype package doesn't
handle functions.

Revised expressions of the form <term>:<type> ' <term> to be (<term><type>) ' <term>
to avoid confusion with the type variable ' .

Changed the standard symbol for fcp$index, from %% to '. The old symbol
can still be used, so existing code shouldn't break.

Turns off bracket syntax for array types when using EmitML.

fcpScript: Included some list <-> fcp theories and an 'a sub1 type which reduces the cardinality by one

FSUBST is now called FCP_UPDATE.

Moved the function substitution operation (:-) to standard part of
the distribution.

substTheory.SUBST_EVAL:
|- !f a b c. (a :- b) f c = (if a = c then b else f c)

A couple of theorems have been renamed in the process:

SUBST_EQ2 -> SUBST_IMP_ID
SUBST_EQ3 -> SUBST_ID

Likewise renamed these theorems for FCP substitution (:+).

Added a substitute operation :+ for FCPs.

Also made EmitML work with numeric types e.g. ``:2`` gets the ML
type "unit bit0".

A cleaner solution for emitting ML code for Finite Cartesian Products.

The ``:'a itself`` type is given a type constructor "ITSELF n" in ML,
where "n" is the dimindex size of ``:'a``.

Second go at changing the scheme for index types. The new scheme uses:
``:one``, ``:'a bit0``, and ``:'a bit1``. For example, ``:i18`` is
``:one bit0 bit0 bit1 bit0``. The EmitML code is more like the original
version i.e. the performance loss is avoided.

Have changed the way that index types are created. The new scheme
uses a canonical form, with ``:bool # 'a`` used to double the index
size and ``:'a option`` used to increment it. The index type is
generated by a new function fcpLib.index_type; for example:

- fcpLib.index_type 5;
> val it = ``:(bool # bool) option`` : hol_type

The function fcpLib.mk_index_type performs roughly as it did before,
however, a type abbreviation is now used for the index type. These
abbreviations are printed for indexes > 8. For example:

- fcpLib.mk_index_type 5;
> val it =
(|- FINITE UNIV, |- CARD UNIV = 5, |- dimindex (:(bool # bool) option) = 5)
: thm * thm * thm
- ``:i5``;
> val it = ``:(bool # bool) option`` : hol_type

- fcpLib.mk_index_type 30;
> val it = (|- FINITE UNIV, |- CARD UNIV = 30, |- dimindex (:i30) = 30) :
thm * thm * thm

It is not expected that these changes will break anything...

Added a theorem about concatenating sub-words.

Some rationalisation with the use of computeLib.auto_import_definitions.

Also, TOP and MSB are computed, saved and added to the compsets for
the standard word sizes.

Using Define for dimindex mucks up evaluation.

Added TOP_def to the SIZES_ss fragment and the evaluation compsets.

Alter the n-bit word theories to use the :'a itself type, and also add
new constants (TOP(:'a) and MSB(:'a)) to stand for the numeric value of
2 ** width, and 2 ** (width - 1). Using these makes the expression
of several results a lot nicer. As the updated proofs in integer_wordScript
demonstrate, you don't always have to expand these definitions either,
which is nice.
I'm not 100% sure that these are the best names for these constants.

Syntax support for words.

The standard word sizes are now provided in machine_wordsTheory - previously
they could be loaded with machine_wordsLib, but then the type theorems
weren't saved in a proper theory.

A new theory of words - based on an idea from John Harrison.
This is now a unified theory of words - so there's no more need
for the Functor or mkword.exe.

The old library (n_bit) will eventually be dropped, so current
users are advised to adopt the new library as soon as possible.
NB. bitTheory is nearly identical to the old bitsTheory.

The new representing type is finite Cartesian products e.g.
:bool ** 'a is the type for words whose length is the size
of the indexing type 'a.

The function fcpLib.mk_index_type can be used to create the
required index type.

Most theorems from the old theory should be present (if I've
missed any out then let me know). NB. A few theorems have
changed name and some have been dropped (e.g. there is no longer
a word_suc function).

Some symbols have changed. This avoids complaints from the
parser and should hopefully aid readability.

old new
two's comp. : ~ $-
bitwise not : NOT ~
bitwise or : | !!
bitwise and : & &&
bitwise xor : # ??
unsigned < : <. <+
unsigned <= : <=. <=+
unsigned > : >. >+
unsigned >= : >=. >=+

The bits and slice functions no longer map to :num - they now
map from :bool ** 'a to :bool ** 'a.

bits : WORD_BITS h l w (h -- l) w
slice : WORD_SLICE h l w (h <> l) w

The function w2w converts between words of different sizes
(unsigned) and sw2sw is a signed (2's complement)
word-word conversion.

The library machine_wordsLib provides the types word4, word8
word16, word32 and word64. Ground term evaluation with
EVAL should work here. Some operations (+, *) can be evaluated
with alpha types e.g.

EVAL ``6w + 4w``;
<<HOL message: inventing new type variable names: 'a>>
> val it = |- 6w + 4w = 10w : thm

Subtraction only works when the word size is known e.g.

EVAL ``6w:word8 - 4w``;
> val it = |- 6w - 4w = 258w : thm

An attempt to do evaluation with alpha types around will likely
result in gibberish.