----------------------------------------------------------------------
SUBST1_TAC                                                    (Tactic)
----------------------------------------------------------------------
SUBST1_TAC : thm_tactic

SYNOPSIS
Makes a simple term substitution in a goal using a single equational theorem.

KEYWORDS
tactic.

DESCRIBE
Given a theorem {A'|-u=v} and a goal {(A,t)}, the tactic
{SUBST1_TAC (A'|-u=v)} rewrites the term {t} into {t[v/u]}, by substituting
{v} for each free occurrence of {u} in {t}:

      A ?- t
   =============  SUBST1_TAC (A'|-u=v)
    A ?- t[v/u]

The assumptions of the theorem used to substitute with are not added
to the assumptions of the goal but are recorded in the proof.  If {A'} is not a
subset of the assumptions {A} of the goal (up to alpha-conversion), then
{SUBST1_TAC (A'|-u=v)} results in an invalid tactic.

{SUBST1_TAC} automatically renames bound variables to prevent free variables in
{v} becoming bound after substitution.

FAILURE
{SUBST1_TAC th (A,t)} fails if the conclusion of {th} is not an equation.
No change is made to the goal if no free occurrence of the left-hand side
of {th} appears in {t}.

EXAMPLE
When trying to solve the goal

   ?- m * n = (n * (m - 1)) + n

substituting with the commutative law for multiplication

   SUBST1_TAC (SPECL ["m:num"; "n:num"] MULT_SYM)

results in the goal

   ?- n * m = (n * (m - 1)) + n




USES
{SUBST1_TAC} is used when rewriting with a single theorem using tactics such as
{REWRITE_TAC} is too expensive or would diverge. Applying {SUBST1_TAC} is also
much faster than using rewriting tactics.

SEEALSO
Rewrite.ONCE_REWRITE_TAC, Rewrite.PURE_REWRITE_TAC,
Rewrite.REWRITE_TAC, Tactic.SUBST_ALL_TAC, Tactic.SUBST_TAC.

----------------------------------------------------------------------