GSUBST_TAC : ((term * term) list -> term -> term) -> thm list -> tactic
STRUCTURE
Tactic
SYNOPSIS
Makes term substitutions in a goal using a supplied substitution function.
DESCRIPTION
GSUBST_TAC is the basic substitution tactic by means of which other tactics such as SUBST_OCCS_TAC and SUBST_TAC are defined. Given a list [(v1,w1),...,(vk,wk)] of pairs of terms and a term w, a substitution function replaces occurrences of wj in w with vj according to a specific substitution criterion. Such a criterion may be, for example, to substitute all the occurrences or only some selected ones of each wj in w.

Given a substitution function sfn, GSUBST_TAC sfn [A1|-t1=u1,...,An|-tn=un] (A,t) replaces occurrences of ti in t with ui according to sfn. 

              A ?- t
   =============================  GSUBST_TAC sfn [A1|-t1=u1,...,An|-tn=un]
    A ?- t[u1,...,un/t1,...,tn]
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 GSUBST_TAC sfn [A1|-t1=u1,...,An|-tn=un] results in an invalid tactic.

GSUBST_TAC automatically renames bound variables to prevent free variables in ui becoming bound after substitution.

FAILURE
GSUBST_TAC sfn [th1,...,thn] (A,t) fails if the conclusion of each theorem in the list is not an equation. No change is made to the goal if the occurrences to be substituted according to the substitution function sfn do not appear in t.
USES
GSUBST_TAC is used to define substitution tactics such as SUBST_OCCS_TAC and SUBST_TAC. It may also provide the user with a tool for tailoring substitution tactics.
SEEALSO
SUBST1_TAC, SUBST_OCCS_TAC, SUBST_TAC
HOL  Kananaskis-13