SUBST1_TAC

Tactic.SUBST1_TAC : thm_tactic

Makes a simple term substitution in a goal using a single equational theorem.

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

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.

See also

Rewrite.ONCE_REWRITE_TAC, Rewrite.PURE_REWRITE_TAC, Rewrite.REWRITE_TAC, Tactic.SUBST_ALL_TAC, Tactic.SUBST_TAC