Implement and document new irule_at tactic

Move some of the machinery behind BasicProvers.VAR_EQ_TAC to Tactic

Extend drule family with rev_ and _at options

rev_ causes search for assumptions to start at opposite end of
list (i.e., uses last{_x,}_assum), and _at allows specification of
which hypothesis in the implicational theorem to match against.

Promote mp_then and resolve_then to be exported by Tactic

Keep their implementations in separate files for the sake of
self-containedness.

Implement & document controlled resolution tactics (drule & friends)

Implement impl_{keep_,}tac with new provehyp_then primitive

The underlying primitive allows obvious generalisations of the impl
tactics, such as pulling from assumptions and passing the resulting
theorems to different continuation thm-tactics.

Add lowercase alias of “DISCH_TAC”.

Various doc fixes

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

Define part_match_exists_tac

This tactic allows users to specify bindings for existential variables
in goals by providing a term to match against some part of the body
under the existentials.

Define tactics to apply implication-L rule backwards

Rule is sequent calculus's:

Γ ⊢ P Γ, Q ⊢ R
----------------------
Γ, P ==> Q ⊢ R

Implementation assumes that goal is of the form

(P ==> Q) ==> R

(rather than with P ==> Q in the assumptions).

The impl_keep_tac version also adds P as an assumption to the second
sub-goal.

(From CakeML.)

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

Expose and document IRULE_CANON.

This function is similar to MP_CANON (which is undocumented), and
normalises theorems to make them usable as introduction rules (as is
done by the irule tactic). Also tweak irule's documentation to better
reflect this implementation.

Finally, give irule an alias in Tactic as IRULE_TAC.

new tactic RULE_L_ASSUM_TAC

like RULE_ASSUM_TAC but f produces list of theorems

renamed prim_irule_tac to prim_irule

Tactic.irule, also prim_irule_tac and Drule.SPEC_UNDISCH_EXL

extra semicolons removed from (some) .sig files

Added HINT_EXISTS_TAC.

Implement & use a generic tactic to apply "deep" introduction rules.

A "deep" intro rule is one that looks like

sideconds ==> P (someterm)

The P is a variable and so the P (someterm) pattern can be seen as a
way to match any term that has someterm within it as a sub-term.
Example rules of this form are boolTheory.SELECT_ELIM_THM,
whileTheory.LEAST_ELIM and optionTheory.some_intro. (It's a shame the
names for the older theorems feature "ELIM" as substrings; these are
clearly introduction rules.) We can't use normal first-order
matching, nor higher-order patterns to match such patterns. Instead,
the code performs a search through the term, looking for first-order
matches of someterm.

In both LEAST_ELIM_TAC and SELECT_ELIM_TAC, the search was done by
find_terms; the new implementations of these functions work through
the term in a different, but now well-specified order: top-down,
left-to-right. If there are multiple matches in a term, and it makes
a difference what one you get, you should use DEEP_INTROk_TAC, which
takes a tactic 'continuation'. If this tactic fails with a HOL_ERR
when applied to the resulting goal-state, then DEEP_INTROk_TAC tries
again on a different sub-term, if there is one.

I will write proper documentation for this all shortly.

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