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.

Change irule to not include a rpt conj_tac effect

Closes #465

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”.

Remove eqtype declaration for term type

Change behavior of MATCH_MP_TAC to fail only when being applied to an actual goal-state, instead of failing when given the first parameter

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

Fix build errors prompted by goal_assum

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.)

Make COND_CASES_TAC handle repeated use of guard properly

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.

Remove some code now unused (as of 934bff32ef1)

Tweak order of subgoal-conjuncts produced by irule

Gets uses in sortingTheory to work again

Fix bug in irule found by Jeremy.

Wasn't collapsing groups of assumptions together in terms of their
shared free variables correctly.

Fix irule to handle input thms with hyps better

As per selftests. Other possible differences will be in ordering of new
subgoal, and distribution of existentials over those subgoals.

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

trivial simplification - uses match_term, not match_terml

new tactic RULE_L_ASSUM_TAC

like RULE_ASSUM_TAC but f produces list of theorems

change irule to do GEN_ALL to argument theorem first

links from help pages for MATCH_{ACCEPT,MP}_tac to [prim_]irule

Delete trailing whitespace in src/

renamed prim_irule_tac to prim_irule

Tactic.irule, also prim_irule_tac and Drule.SPEC_UNDISCH_EXL

infix THEN_LT - hopefully in the right place now

see comments on https://github.com/HOL-Theorem-Prover/HOL/pull/221

infix declaration for THEN_LT in Tactic.sml

not sure why this is needed - builds here without it, but not on GitHub;
and clearly not needed for THEN in Tactic.sml

re-implement CONJ_ASM1_TAC, CONJ_ASM2_TAC using USE_SG_THEN

now one-line implementation of these tactics

HO_MATCH_MP_TAC: new documentation and fix of failure report

Added HINT_EXISTS_TAC.

Tidy-up formatting of some src/1 code.

Tidy up some code under src/1. See commit ad9b041.

Move bvk_find_term (used in DEEP_INTROk_TAC) to HolKernel.

Document it and the other find_term functions from HolKernel.

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!