----------------------------------------------------------------------
SUBST_ALL_TAC                                                 (Tactic)
----------------------------------------------------------------------
SUBST_ALL_TAC : thm_tactic

SYNOPSIS
Substitutes using a single equation in both the assumptions and conclusion of a
goal.

KEYWORDS
tactic.

DESCRIBE
{SUBST_ALL_TAC} breaches the style of natural deduction, where the assumptions
are kept fixed.  Given a theorem {A|-u=v} and a goal {([t1;...;tn], t)},
{SUBST_ALL_TAC (A|-u=v)} transforms the assumptions {t1},...,{tn} and the term
{t} into {t1[v/u]},...,{tn[v/u]} and {t[v/u]} respectively, by substituting {v}
for each free occurrence of {u} in both the assumptions and the conclusion of
the goal.

           {t1,...,tn} ?- t
   =================================  SUBST_ALL_TAC (A|-u=v)
    {t1[v/u],...,tn[v/u]} ?- t[v/u]

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

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

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

EXAMPLE
Simplifying both the assumption and the term in the goal

   {0 + m = n} ?- 0 + (0 + m) = n

by substituting with the theorem {|- 0 + m = m} for addition

   SUBST_ALL_TAC (CONJUNCT1 ADD_CLAUSES)

results in the goal

   {m = n} ?- 0 + m = n




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

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