SUBST1_TAC : thm_tactic
STRUCTURE
SYNOPSIS
Makes a simple term substitution in a goal using a single equational theorem.
DESCRIPTION
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
HOL  Trindemossen-1