Add a new function for handling labels in markerLib

Alter VAR_EQ_TAC to call TIDY_ABBREVS after invocation

TIDY_ABBREVS "purges" abbreviations that have become malformed, where

- "malformed" means no longer of form Abbrev (var = exp), with exp not
itself a variable
- "purge" means Abbrev(e1 = e2) becomes e2 = e1, and Abbrev(other_exp)
becomes other_exp.

The action of TIDY_ABBREVS is included in the ABBREV_ss simpset
fragment, which is in turn included in the stateful simpset.

The calling of TIDY_ABBREVS is the only change in the behaviour of
VAR_EQ_TAC, and this can be turned off with the
BasicProvers.var_eq_old trace.

Tweak 'using' to now handle unnamed monomorphic theorem arguments

Allow Induct_on & Cases_on to use different theorems with 'using'

The using function is infix on tactics; other tactics can grab 'using'
theorems if they want to try, using the markerLib.maybe_using
entrypoint.

Reinstate a way to refer to labelled assumptions

This got lost in c76376ed3f7d (2008!).

It clearly isn't being used, but I may want it in the near future.
Change the name from LB to L. With markerLib open, one can write
things like

simp[L"mylabel",...]

to get access to the assumption labelled "mylabel".

Also, using a congruence, stop the stateful simpset from rewriting
under labels.

Implement Req0/ReqD forms to require simp rules to have been applied

Closes #680

Add Excl theorem form to exclude things from simplification

For example

simp[Excl "BETA_CONV"]

will stop the BETA_CONV conversion from firing.

This doesn't interact correctly with remove_ssfrags properly yet
because that function rebuilds a simpset from its constituent
fragments, and so will put back stuff that Excl has removed. The
remove_ssfrags implementation will change to simply remove those
things in the simpset that have come from given fragments (meaning
that simpsets will no longer need to store their originating fragments
at all).

Remove eqtype declaration for term type

Make PAT_ABBREV_TAC aware of hidden/revealed status of "constants"

In particular, use gen_variant Parse.is_constname rather than variant.
The latter avoids generating names that clash with constants in the
logical signature. The former only avoids those names that
the *parser* thinks of as constants. This is better for user-facing
code such as PAT_ABBREV_TAC.

Closes #431

MATCH_ABBREV tactics now ignore _ in patterns

Tactics affected are
- MATCH_ABBREV_TAC
- HO_MATCH_ABBREV_TAC
- MATCH_ASSUM_ABBREV_TAC

Documented and self-tested

Q.PAT_ABBREV_TAC fails rather than bind a bound variable

Documentation updated. Previous behaviour would be to attempt to bind a
bound variable in an abbreviation and end up creating a vacuous
abbreviation.

Closes #262

Let PAT_ABBREV_TAC use patterns that are more polymorphic than the goal

Closes #252

Fix bugs in Q's match_{rename,abbrev} tactics; refine spec.

In particular, make sure that instantiations arising from the matches
are applied in an order that is sure to make the substitutions apply
as much as possible. There are two obvious ways in which things can
go wrong (resulting in a goal-term that doesn't in fact look like the
supplied pattern).

1. If the match results in an instantiation that has a variable
binding a term that appears within another. E.g., (example from
Ramana):

Q.MATCH_RENAME_TAC `f v = z` (?- `f (h s) = s`)

The match will return (v |-> h s, z |-> s), but if this is applied
with the z going first, the goal won't contain `h s` when the
substitution for v is attempted. So that's bad, and affects both
renaming and abbreviating tactics.

The fix is to sort the instantiation list so that larger terms are
substituted out first.

2. Distinct variables in the pattern may end up binding the same
term. This is something users are less likely to bring about, but
it still seems worth trying to nail down what the behaviour should
be. E.g.,

Q.MATCH_RENAME_TAC `a + b = 10` (?- 5 + 5 = 10)

This will want to bind a and b to 5. When abbreviating, you might
like to see abbreviations `a = 5` and `b = 5` in the assumptions,
and when renaming or abbreviating, you might like to have the goal
become `a + b = 10`. Achieving both these might be possible, but
seems hard. Instead, the operational approach of performing
substitutions in a sequence is stuck to, but the substitution is
sorted so that the variable with the earlier name goes first. This
means you'll get ?- a + a = 10 as the goal, and when abbreviating,
you'll get `a = b` and `b = 5` as abbreviations in the
assumptions.

The fixes in examples/ are generally because proofs have relied on
abbreviations *not* occurring, despite the presence of variables in
the pattern. The situation is analogous to the situation in 1. above,
where the user has exploited the fact that a binding hasn't been
introduced for v.

Document Q.PAT_ABBREV_TAC. Also flip the default setting of "PAT_ABBREV_TAC: match var/const".

Warning: this change will break proofs that are sensitive to (rely on) the current behaviour of PAT_ABBREV_TAC.

See commits c5c281b, e824426, and a373506; and issue #79.

Add a configuration trace flag "PAT_ABBREV_TAC: match var/const", which should close Issue #79.

This flag is false by default. When set (by set_trace or trace) it enables PAT_ABBREV_TAC to match on variables and constants (which is not always desirable). Setting the flag can break existing proofs, e.g. the ARM6 correctness proof fails when more matches are permitted.

Implement a simple tactic to undo Abbrev in assumptions.

Suggested by Magnus, this tactic turns all assumptions of the form
Abbrev (t1 = t2)
into
t2 = t1

Added MATCH_ASSUM_ABBREV_TAC to Q and markerLib.

This completes the set of pattern-matching tactics spanning the two dimensions of abbreviate/rename and conclusion/assumptions.

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!

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.

Changed behaviour of simplifier to
propagate the abbreviation coming from
a let binding in the goal being moved to
the assumptions. This helps keep the goal
in "fully abbreviated form". Also added

Q.REABBREV_TAC

which re-abbreviates the goal and

Q.WITHOUT_ABBREVS tac

which temporarily removes all abbreviations,
runs tac, then reabbreviates.

Probably, Q is not the right place for these
functions, but the rest of the abbreviation
stuff is there.

Also added some internal documentation on what
Q.ABBRS_THEN does, and the like.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

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.

New treatment of abbreviations. Documentation still to be updated.
Backwards compatibility illustrated in examples/lambda/standardisationScript
and examples/arm6. New techniques and entry-points illustrated in
core distribution and some of the lambda example scripts.

Minor changes to support simpLib upgrade.

Support for rewriting annotations.

Got rid of QConv, and made all conversions do the "raise exception to
indicate reflexivity" thing. (Also fixed bug in new implementation
of ABS_CONV that attempted renaming on failure of conv, and not just
failure of ABS.)

Next step will be to rework the simplifier's implementation so that
it also uses Conv.UNCHANGED, rather than in its own internal version
of the same. This will let the simplifier play efficiently with
others.

May also assess making ABS_CONV not do renaming, and give the rewriter
its own special traverser. This might make some things more efficient.

Minor conflict resolved.

Fixed with structure ... end bracketting to protect it from the evils of
the W2K file-system.

Moved marker stuff to its own directory, and also used same_const
function in new markerLib.
In a far off, distant land, where we implement named assumptions using
Konrad's NAMED constant (see src/basicProof/Notes), this stuff will
need to put back into bool so that the basic tactics can be made to work
with named assumptions.