SUBST_ALL_TAC : thm_tactic
STRUCTURE
SYNOPSIS
Substitutes using a single equation in both the assumptions and conclusion of a goal.
DESCRIPTION
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
HOL  Trindemossen-1