Start of work to replace MEM with λx l. x ∈ set l.  See #52.
Get listTheory to build in features/mem-abbrev branch.  See #52.
Build all of src/list/src and up to integer_word.  See #52.

listSyntax loses mem_tm, but retains a mk_mem and a dest_mem that do
the obvious thing.
Attempt to fix cooper_conv bug.

COOPER_CONV ``~(&a + &b < 0)`` still fails.
Fix bug in Cooper's algorithm; build-sequence at selftest=0 builds.

Progress with #52.
Add IN_INSERT and NOT_IN_EMPTY to list_ss.

This allows simplification of MEM terms to work in all circumstances.  For example, if the term is

  MEM x (FRONT [y])

the simplification works like

     x IN set (FRONT [y])
     ^^^^^^^^^^^^^^^^^^^^

 --> x IN set (FRONT [y])
          ^^^^^^^^^^^^^^^

 --> x IN set (FRONT [y])
               ^^^^^^^^^

 --> x IN set []
              ^^

 --> x IN set []
          ^^^^^^

 --> x IN EMPTY

and the simplifier's theorem for MEM x [] (= x IN set []) never gets to fire.

This is progress with #52.
Get quotient examples (finite sets) to work in mem-abbrev world.

Progress with #52.
Add IN_UNION to list_ss; handles set(l1 ++ l2) being rewritten.

This is progress with #52.
Get decidable separation logic example to build.

Now that IN_LIST_TO_SET is gone, some scripts have to change. Another
alternative would be to bind that name to a trivial theorem that can't
hurt the progress of simplification (TRUTH would do).

This is progress with #52.
Make listTheory.IN_LIST_TO_SET a trivial rwt for backwards compatibility.

Its old statement was

  x IN set l <=> MEM x l

but that is now an instance of reflexivity given MEM's overloading.
A couple of minor fixes to make sep. logic example's treeScript build.

Problem was that rewriting with IN_DEF (itself a generally risky thing
to do) now affects terms of the form `MEM x t`, turning them into `set
t x`, which is likely to end particularly badly.
Minor changes towards getting theorem-prover example to build.

Problem is use of IN_DEF as a rewrite when there are also MEM h t
terms around. This is pretty bad form in my opinion, so I don't feel
too bad about having to adjust proofs.
Get cheney_allocTheory to build in mem-abbrev world.

Progress with #52.
Get all of machine-code/garbage-collectors to build.

Progress with #52. General principle is to avoid use of IN_DEF, and to
instead prove rewrites of the form

  |- x ∈ myconstant arg1 .. argn ⇔ somerhs

rewriting set l x back to MEM x l as necessary.
Ignore .s files in theorem-prover's bin directory.
Merge branch 'features/mem-abbrev'.  Closes #52.

This makes MEM e list an abbreviation for e ∈ set list.

The overall damage is summarised here, and I think it's pretty
acceptable.

 .../src/decidable_separationLogicScript.sml        |   36 ++++---
 .../garbage-collectors/cheney_allocScript.sml      |   23 ++++-
 .../garbage-collectors/lisp_gcScript.sml           |   10 +-
 examples/separationLogic/src/treeScript.sml        |   13 ++-
 .../garbage-collector/lisp_consScript.sml          |   14 +--
 .../lisp-runtime/implementation/lisp_invScript.sml |   27 +++---
 src/boss/bossLib.sml                               |    3 +-
 src/integer/CooperCore.sml                         |   17 ++--
 src/list/src/listScript.sml                        |  101 +++++++-------------
 src/list/src/listSyntax.sig                        |    1 -
 src/list/src/listSyntax.sml                        |   11 ++-
 src/list/src/rich_listScript.sml                   |    8 +-
 src/quotient/examples/ext_finite_setScript.sml     |   13 ++-
 src/quotient/examples/finite_setScript.sml         |   36 ++-----
 14 files changed, 151 insertions(+), 162 deletions(-)

The changes to the examples mostly came about because people were
rewriting with IN_DEF, as per the discussion on some of the commits on
the feature branch (f42df6bf5ef85f4abb73 .. 8747783169b6c0c).

The change to Cooper was required because it pulled apart MEM terms in
a RAND_CONV/RATOR_CONV kind of way, and the underlying term
structure *has* changed, of course.

In the quotient examples, the MEM constant no longer exists, so can't
be lifted.