Move Q.ID_EX_TAC to Tactic.

ID_EX_TAC doesn't take any arguments, let alone a quotation, so
doesn't belong in Q.

Closes #359

Rename pat_assum to pat_x_assum; provide pat_assum

To be consistent with naming conventions elsewhere, change the name of
qpat_assum (and PAT_ASSUM, and Q.PAT_ASSUM) to include an extra _x_ (or
_X_), indicating that the matching assumption is pulled out of the
assumption list.

Use the old names to provide a version that doesn't pull the assumption
out of the list.

Again, seeking consistency with other similar tactics, make variable
names that appear in the pattern and the goal be forced to have the type
that they have in the goal.

Implement Q.RENAME_TAC / bossLib.rename

This tactic is more powerful than rename1 as it allows multiple patterns
to be matched at once, and without regard to the initial goal's free
variables (which might otherwise cause unpredictable clashes).

Rename: qcase_tac/rename1; Q.FIND_CASE_TAC/Q.RENAME1_TAC

This use of the "case" substring was just confusing given things like
Cases_on. The "1" is there because I want to now implement a more
general version that
- deals with the issue (identified in the .doc file), where existing
names in the goal can still get in the way; and
- allows multiple subterms to be matched and renamed as a unit

Though seemingly independent, the second feature is really needed if the
first is to be done: implementing the first will require all the free
variables in a goal to be renamed away (to genvars, I expect), and then
it's impossible to ground particular matches against known free
variables.

Define special backtracking cases of pat_assum

In particular, the "pattern" is a single term or quotation that has to
either be the head constant of the assumption or the head of the lhs of
the assumption. Unlike pat_assum as it stands currently, the behaviour
backtracks (à la first_assum) if the theorem-tactic doesn't succeed with
the first assumption found.

Versions come in "copy assumption" and "cut assumption" versions, just
like first_assum and first_x_assum.

implement abbrevation tactics for subterms.

Change API of Q's MATCH...RENAME_TACs.

Now rather than a string list hanging off the end specifying which
variable bindings aren't supposed to induce a renaming, just put
underscores into the pattern in those positions.

Documentation and release notes updated.

Document new FIND_CASE_TAC.

Implement Q.MATCH_ASMSUB_RENAME_TAC.

Progress with #81.

A renaming/matching tactic that matches against subterms in the goal.

Progress with Github issue #81 (which also calls for the same against
assumptions and an abbreviation version too).

Add Q.GENL.

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.

Two new tactics in Q for renaming parts of a goal by pattern matching.

MATCH_RENAME_TAC works on the goal statement; MATCH_ASSUM_RENAME_TAC on the
assumption list. Both tactics attempt to match a pattern against the goal (or
an assumption). Matching parts of the goal are then replaced by the
corresponding pattern variables.

Useful for renaming ugly generated variable names with minimal effort. The
pattern does double duty in the assumption case: it both picks out the matching
assumption and also specifies what the new variable names should be.

Recently I was writing structures like

Q.EXISTS_TAC `e1` THEN
Q.EXISTS_TAC `e2` THEN
...
Q.EXISTS_TAC `en` THEN

in my proof scripts a lot. This is lengthy and tidious. So I added

Q.LIST_EXISTS_TAC [`e1`, `e2`, ..., `en`]

as a shortcut.

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.

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.

Have to add the new functions to the signature. Take the opportunity to
define type abbreviations and align all those pesky colons.

Implemented Anthony's PAT_ABBREV_TAC. He should write some documentation
for it :-)

SPEC_THEN etc managed to disappear from the signature file.

New versions of old stuff.

Theorem argument to the new SPEC_THEN functions must be last for
better composition with other tacticals. Want to be able to write
things like
FIRST_X_ASSUM (Q.SPEC_THEN `x` (Q.X_CHOOSE_THEN `y` SUBST_ALL_TAC))

Added SPEC_THEN (and obvious friends) to make it easier to specialise
theorems in the middle of proofs and use the current parsing context.

Added REFINE_EXISTS_TAC, which allows you to turn an existential goal
into a new existential goal, where the variable has been replaced by
a more concrete term.
E.g.,
?n. 0 < n
================ REFINE_EXISTS_TAC `SUC m`
?m. 0 < SUC m

Modified Q.prove to be in line with prove, i.e., taking a tuple of
arguments.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision