SUBST_TAC : (thm list -> tactic)
STRUCTURE
SYNOPSIS
Makes term substitutions in a goal using a list of theorems.
DESCRIPTION
Given a list of theorems A1|-u1=v1,...,An|-un=vn and a goal (A,t), SUBST_TAC rewrites the term t into the term t[v1,...,vn/u1,...,un] by simultaneously substituting vi for each occurrence of ui in t with vi:
              A ?- t
   =============================  SUBST_TAC [A1|-u1=v1,...,An|-un=vn]
    A ?- t[v1,...,vn/u1,...,un]
The assumptions of the theorems used to substitute with are not added to the assumptions A of the goal, while they are recorded in the proof. If any Ai is not a subset of A (up to alpha-conversion), then SUBST_TAC [A1|-u1=v1,...,An|-un=vn] results in an invalid tactic.

SUBST_TAC automatically renames bound variables to prevent free variables in vi becoming bound after substitution.

FAILURE
SUBST_TAC [th1,...,thn] (A,t) fails if the conclusion of any theorem in the list is not an equation. No change is made to the goal if no occurrence of the left-hand side of the conclusion of thi appears in t.
EXAMPLE
When trying to solve the goal
   ?- (n + 0) + (0 + m) = m + n
by substituting with the theorems
   - val thm1 = SPEC_ALL arithmeticTheory.ADD_SYM
     val thm2 = CONJUNCT1 arithmeticTheory.ADD_CLAUSES;
   thm1 = |- m + n = n + m
   thm2 = |- 0 + m = m
applying SUBST_TAC [thm1, thm2] results in the goal
   ?- (n + 0) + m = n + m

USES
SUBST_TAC is used when rewriting (for example, with REWRITE_TAC) is extensive or would diverge. Substituting is also much faster than rewriting.
SEEALSO
HOL  Kananaskis-13