SUBST_TAC : (thm list -> tactic)

- 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: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.
A ?- t ============================= SUBST_TAC [A1|-u1=v1,...,An|-un=vn] A ?- t[v1,...,vn/u1,...,un]

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 goalby substituting with the theorems
?- (n + 0) + (0 + m) = m + n

applying SUBST_TAC [thm1, thm2] results in the goal- val thm1 = SPEC_ALL arithmeticTheory.ADD_SYM val thm2 = CONJUNCT1 arithmeticTheory.ADD_CLAUSES; thm1 = |- m + n = n + m thm2 = |- 0 + m = m

?- (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

HOL Kananaskis-14