Handle more constants in list_compset

With some regression tests.

Closes #548

Make sure recent new constants (from CakeML) are in compsets

In particular, oHD and oEL (aka LLOOKUP need to appear).

Remove -- as an alias for Term parser.

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

Remove some duplicates of the theorem TRUTH.

These are:
• INFINITE_DEF and IN_LIST_TO_SET (replaced with overloadings)
• IN_APP_applied and IN_ABS_applied (inadvertently generated)

Also, made changes to try to avoid new definitions in listTheory accidentally having a "_DEF" suffix instead of "_def". Old naming inconsistencies still remain in listTheory (e.g. EXISTS_DEF, FIND_def and FLAT).

These changes will break a few proofs but patches should be trivial (i.e. removing references to these TRUTH theorems and/ or renaming "_DEF" to "_def").

Attempt to tidy-up some proof scripts. Much of this has come from CakeML.

Removed Unicode and tried to eliminate lines longer than 80 characters.

Also added a few new constants to listTheory: INDEX_FIND, FIND and INDEX_OF.

Added "nub" to listSyntax.

add new dropWhile constant to listTheory, and various lemmas

add LIST_TO_SET_THM to the list compset

Rearrange "open" order in listSimps.

Revert to using LENGTH instead of LEN

Based on some performance experiments done by Anthony.
This partially reverts aeb5670.

add tail-recursive SUM for EVAL, and use the tail-rec LENGTH

this modifies list_compset, and what is added to the_compset by
listTheory. LEN appeared to have been defined but not used.

Minor tweaks to list compset.

Support list_compset evaluation of TAKE, DROP, PAD_LEFT, PAD_RIGHT and isPREFIX. Also make evaluation of REVERSE more efficient.

Minor tweaks to evaluation.

Name a simpset fragment.

Modications to simpsets and compsets for lists with respect to the evaluation of EL.
This requiered some minor additions to listTheory. I used the change to add some more simple rewrites and definition that I use in my separationLogic example.

As discussed on the HOL-developers mailing list (18 March 2010, 3:33 pm, "Simpsets and compsets for lists / evaluation of EL"), I had
trouble with the standard compsets and EL. If applied to a term "EL n l" where "n" was not a ground term these compsets diverged.
That is changed now. For ground terms the evaluation should behave the same, for non-ground ones it will now terminate.

The simpsets terminated, but evaluated EL as long as possible. For example
``EL 5 (x1::x2::xs)`` got converted to "|- EL 5 (x1::x2::xs) = HD (TL (TL (TL xs)))".
That has been changed and now the result is "|- EL 5 (x1::x2::xs) = EL 3 xs".

The main additional definition I added is "LIST_COUNT" to rich_listTheory.
``LIST_COUNT n`` evaluates to the list [0;1;...;(n-1)].

Clean-up of LIST_EQ_SIMP_CONV and related functions.

- make it aware of REVERSE
- added documentation
- remove orginal name of simpset "list_eq_simp_ss" and just use the new one "LIST_EQ_ss"
- bring listLib.sig up-to-date

Fix a problem in a proof that occurs because of the stronger simplification.

Fix for LIST_EQ_SIMP_CONV bug (from Thomas Tuerk).

Move Thomas' list_eq_simp_ss to listSimps and make it automatic.

This requires the movement of SNOC and some theorems from rich_list to list.
Making the simpset fragment automatic may break proofs by solving more than
expected.

Extension of the interface of listLib.sml by adding the functions provided by

listSimps
rich_listSimps
ListConv1

For a clean cut, the implementation of "list_compset" has been moved to listSimps. It is however still available in the interface of listLib, so no code needs to be changed.

Complete implementation of generic theory data feature, and use it to
implement the exportable rewrites used in srw_ss(). The code still
needs some more polishing. Hopefully that will come as I convert
other "stored data features" to use the same underlying code.

Exported some SRW rewrites, using the theorems that go into
listSimps.LIST_ss. In fact, made listSimps.LIST_ss just refer back
to listTheory.list_rwts.

Changed names of simpset fragments to be more consistent. Also
reinstated ELL in what is now RICH_LIST_ss, which was removed for no
good reason, and put FRONT_CONS and LAST_CONS into LIST_ss. (These
used to be in RICH_LIST_ss as LAST_CONS and BUTLAST_CONS.)

Added a trivial theorem about MEM and APPEND.

Changes to add REVERSE to the automatic tools.

New work aimed at making a single global EVAL function, with
an underlying compset.

Made directory Kananaskis compatible; added listSyntax library.

Removed dependency on the global grammar.

Added APPEND_11 to list_ss.

A couple more theorems for listTheory (EVERY_APPEND and EXISTS_APPEND).
Also put these into the standard simpset. Put entries for ZIP and UNZIP
into rich_list to preserve some modicum of backwards compatibility. Of
course, these will be theorems now rather than definitions, but who's
going to notice?

Moved ZIP and UNZIP into listTheory. Proved a bunch of theorems about
them and also EVERY and EXISTS.

Added definition of MEM to simpset.

Oops. MEM, not MEM_DEF.

backtracked the unnecessary restatement of the definitions of MEM, etc.

Removed the ugly boolean of add_thms and from_list.
Use lazyfy_thm or strictify_thm instead.
Modified examples accordingly.

Refinement of computeLib support.

New additions to listSimps, to track all the relevant definitions
made in listScript.

added list_rws to work with computeLib

Initial revision