Tactic.SUBST

STRUCTURE

SYNOPSIS

Makes term substitutions in a goal using a list of theorems.

DESCRIPTION

Given a list of theorems A1|-u1=v1,...,An|-un=vn and a goal (A,t), SUBST_TAC rewrites the term t into the term t[v1,...,vn/u1,...,un] by simultaneously substituting vi for each occurrence of ui in t with vi:

              A ?- t
   =============================  SUBST_TAC [A1|-u1=v1,...,An|-un=vn]
    A ?- t[v1,...,vn/u1,...,un]

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 SUBST_TAC [A1|-u1=v1,...,An|-un=vn] results in an invalid tactic.

SUBST_TAC automatically renames bound variables to prevent free variables in vi becoming bound after substitution.

FAILURE

SUBST_TAC [th1,...,thn] (A,t) fails if the conclusion of any theorem in the list is not an equation. No change is made to the goal if no occurrence of the left-hand side of the conclusion of thi appears in t.

EXAMPLE

When trying to solve the goal

   ?- (n + 0) + (0 + m) = m + n

by substituting with the theorems

   - val thm1 = SPEC_ALL arithmeticTheory.ADD_SYM
     val thm2 = CONJUNCT1 arithmeticTheory.ADD_CLAUSES;
   thm1 = |- m + n = n + m
   thm2 = |- 0 + m = m

applying SUBST_TAC [thm1, thm2] results in the goal

   ?- (n + 0) + m = n + m

USES

SUBST_TAC is used when rewriting (for example, with REWRITE_TAC) is extensive or would diverge. Substituting is also much faster than rewriting.

SEEALSO

ONCE_REWRITE_TAC, PURE_REWRITE_TAC, REWRITE_TAC, SUBST1_TAC, SUBST_ALL_TAC