Fix bug in handling of bounded simp (e.g., with Once)

The bug was introduced by d71df467 and was apparent in a CakeML proof:
the commit made it impossible to use the simplifier to rewrite with
the Abbrev definition backwards (i.e., GSYM markerTheory.Abbrev_def)
because the variable on the LHS of that theorem has type bool. This is
a loopy rewrite, but should be permitted if the rewrite is bounded.

Equally, rewriting with the definition of I backwards would exhibit
the same problem, as long as one first instantiated the alpha in that
theorem to bool.

Stop simplifier from generating rewrites on boolean variables

Occasionally, an assumption will be generated that the simplifier
reads as a conditional rewrite, but which has the shape

!... x..... preconds x y z ==> x

where x is a variable of type bool. These generate pointless
conditional rewrites for all possible terms of type bool. Now we stop
these from getting in.

Closes #556

Fix simp failing to handle rewrites P ==> (b = e) (for b = T or F)

Issue was that code existed for this case but incorrectly manipulated
the input theorem rather than the "undisch" theorem which had moved P
into the theorem assumptions.

Include test.

provide first version of BackchainingLib

This lib is used to combine matching preconditions against assumptions
in the goalstack with conditional rewriting. This enables efficient
backwards-chaining with theorems like

``!x y. R x y ==> !x' y'. complicated condition ==> R x' y'``

Make selftest output line up with parallel Holmake's

Also make tests use testutils.OK to report OK

Fix (somewhat obscure) looping bug in simplifier.

If the terms T = F and F = T both arrive in your assumption list, then
you will go into an infinite loop. Neither should fire as a rewrite at
all. Indeed, anything of the form T = x, or F = x, is better off
flipped, unless it's the bad case above. In the bad case, treat the
rewrite as we treat a bare F.

Extend simplifier's treatment of abbrevs to handle abstractions better

selftest for SATISFY_ss added

Simp{L,R} were only working if the argument was a relation.

This meant one could rewrite exclusively on the left/right of /\, =, ==>
etc, but not +. Problem was an unnecessarily specific theorem.

Bug reported by Ramana Kumar.

Add new test of simplifier's congruence technology.

Bug: bounds on rewrites should be shared between all derived rewrites.

In a situation like

th = |- (p = x) /\ (q = y)

as the input rewrite, you might want separate bounds (i.e., both
conjuncts of Once th get to apply once each), but with

|- (s1 = s2) <=> (!x. x IN s1 <=> x IN s2)

you surely do not want the two derived theorems

|- (s1 = s2) <=> (!x. x IN s1 <=> x IN s2)
|- (s2 = s1) <=> (!x. x IN s1 <=> x IN s2)

to both get a chance to apply. Arguably, in the latter case, the
simplifier should be smart enough to see that the two terms are
instances of each other and not generate two theorems, but the test is
not as simple as just "are both sides variables", because one or both
of the variables may be bound in a goal's assumptions, and then both
rewrites are useful.

New "portable" subdirs per ML implementations in src/portableML.

Hope to do away with Poly/ML specific code in tools-poly eventually,
moving it into src/portableML/poly. tools/build-sequence now records
that the implementation-specific directories have to be included.

src/simp/src/selftest.sml now correctly tests the bug claimed in r6991.
(Yikes^2!)

Selftest contained an error in its check for correct behaviour. (Yikes)

Bounded rewrites where the LHS is a single variable (which you might
want if doing something fiddly with |- m = m + 0, say) get their
bounding reference variable decremented prematurely. This bug
manifests with this pattern (and not with more typical ones) because
the pattern matches everything and gets pulled out of the
internal term-net. Other patterns don't get tried on so many terms.

The problem is not the "pulling out of the net", but the decrementing
the reference inappropriately early.

Add a test-case for a problem found by Ramana Kumar: the Once
annotation doesn't prevent some rewrites from being rejected as
looping, meaning that they don't get applied at all.

Modify the standard conditional rewrite behaviour so that if a rewrite
theorem has been bounded (with Once, or Ntimes), then it is allowed to
be applied in circumstances where the simplifier's looping detection
would otherwise reject it. This allows (Once EQ_SYM_EQ) to do
something, as the new self-test demonstrates.

Additional functionality for abbreviations.

1. The labels library has been merged into
markerLib and the src/labels directory eliminated.
2. Have added markerSyntax structure.
3. Operations on abbrevs used to all be in
structure Q, even those that didn't deal
with quotations (like UNABBREV_ALL_TAC). Now
markerLib provides all abbrev. operations and
these take terms. Operations that benefit from
quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc.
are still to be found in Q.
4. Abbrevs are kept reduced by the simplifiers and
there is a REABBREV_TAC which can be separately called.
This sorts abbrevs topologically, so that they get
restored in a sensible order.
5. For situations where one wants to get rid of all
abbrevs, apply a tactic, and then restore the abbrevs,
there is WITHOUT_ABBREVS: tactic->tactic.
6. Have added a simple topological sort to Lib.
7. Updated proofs in the src directories, and also
in examples/lambda.

Repaired example in selftest to parse under HOL-Omega.

A little code reorganisation and a fix for a bug in the implementation
of ASM_SIMP_TAC and FULL_SIMP_TAC: abbreviation references in the
argument list weren't being dealt with early enough. In the case of
ASM_SIMP_TAC this caused the effect of an abbreviation being eliminated
in the assumptions but not in the goal.

Add a test to check on bounded simplification.

Test that AC really can cope with the associativity and commutativity
theorems the other way round.

Alright, I admit, this is just being precious.

Handle Interrupt slightly more gracefully.

Self-test demonstrating the current bug in the AC rewriter.