GSUBST_TACTactic.GSUBST_TAC : ((term * term) list -> term -> term) -> thm list -> tacticMakes term substitutions in a goal using a supplied substitution function.
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.
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.
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.