Implement machinery to check that tactic results change acceptably

Used to implement checks that h.o. redexes don't remain, or have
decreased in count.

This is progress towards implementation of github issue #680.

Various doc fixes

Implement line-number reporting for failing THEN1/>-

This relies on a somewhat disgusting quotation filter hack which
replaces occurrences of >-/THEN1 in line with the following pattern:

tac1 >- tac2 - - - > tac1 >>- linenumber ?? tac2

This relies on >>- and ?? being left-associative, which is how they
are defined. The definition of ?? is

fun f ?? x = f x

The linenumber is inserted by the quotation filter, which tracks this
naturally.

Provide access to more switches when parsing in context

In particular, allow setting of Feedback traces which will be used
when parsing of quotations occurs.

This allows Q.PAT_ASSUM to be made quiet about inventing type
variables. This is deemed desirable in github issue #425. (I'm not
100% sure now of this, but hey.)

Closes #425

Provide "typed" parsing-in-context entry-points

This allows

QTY_TAC ty tac q

to parse q in the context of the goal and also require the resulting
term to have the provided type. The resulting term is then passed to
tac, as per Q_TAC>

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.

Fix build errors prompted by goal_assum

Put goal_assum into Tactical's signature

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.

More moving lcsymtacs implementations elsewhere

Eventually lcsymtacs will just be a bunch of 'open' declarations, and
then people won't bother to include it at all.

Move some tactics from lcsymtacs to Tactic{,al}

As per Github issue #274

Move lcsymtacs functions to natural homes

For example, we do not need to have >> in lcsymtacs; it might as be in
Tactical. The ultimate aim is to do away with lcsymtacs entirely.

This is work towards github issue #274

Delete trailing whitespace

new irule, order of new subgoals is consistent,

regardless of how the substitution may change the internal
order of hypothesis in the argument theorem

also new tactical ADD_SGS_TAC - like VALIDATE
but new terms to be proved need to be specified

extra semicolons removed from (some) .sig files

new list-tactic USE_SG_THEN

makes one subgoal available in the proof of another

relaxing type constraint for THEN and THENL

to permit
val THEN : list_tactic * tactic -> list_tactic
val THENL : list_tactic * tactic list -> list_tactic
as well as the usual types

GEN_VALIDATE(_LT) - flag for adding new subgoals in any event

GEN_VALIDATE false is like VALIDATE, but adds subgoals for the assumptions
of the theorem produced by the justification, regardless of whether they
are among the assumptions of the goal. Advantage of this is that
GEN_VALIDATE false (ACCEPT_TAC th) produces predictable subgoals,
which may help in coding compound tactics

VALIDATE and VALIDATE_LT

If tac (ltac) is invalid due to proving theorems with extra assumptions,
VALIDATE tac and VALIDATE_LT ltac make the tactic valid by returning extra
subgoals to prove the extra assumptions

expand_list to interactively work on a list of subgoals

also Tactical.VALID_LT, to check that a list-tactical is valid
(expand_list checks validity, expand_listf doesn't)

also abbreviations elt, eall, eta, enth to apply (list-)tactic to subgoal(s)

Delete trailing whitespace in src/

This needs doing periodically, and is best done to a whole bunch of files
at once.

replacing code for THEN and THENL using ALLGOALS and TACS_TO_LT

also defines NULL_OK_LT to implement change to THENL
(see https://github.com/HOL-Theorem-Prover/HOL/issues/214 )

list_tactic concept

introduce list_tactic - works on a list of goals, not a single goal
THEN_LT (tac1, ltac2 : list_tactic),
A tactical that applies ltac2 to the list of subgoals resulting from tac1
TACS_TO_LT (tac2l: tactic list) : list_tactic
ALLGOALS - A list_tactic which applies a given tactic to all goals
ALL_LT - always succeeds
NTH_GOAL - applies tactic to nth goal of list
REVERSE_LT - A list_tactic that reverses a list of subgoals
SPLIT_LT - apply two list-tactics, one to first n subgoals,
the other to the rest
ROTATE_LT - rotate the list of subgoals by n positions

Add LAST_ASSUM and LAST_X_ASSUM tactics

like first_assum and first_x_assum, but work from the other end of the
assumption list

Change src/bool to src/1 as a prelude to experimentation!