Tactic.GSUBST

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.