SUBST1_TAC : thm_tactic

- STRUCTURE
- SYNOPSIS
- Makes a simple term substitution in a goal using a single equational theorem.
- DESCRIPTION
- 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: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.
A ?- t ============= SUBST1_TAC (A'|-u=v) A ?- t[v/u]

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 goalsubstituting with the commutative law for multiplication
?- m * n = (n * (m - 1)) + n

results in the goalSUBST1_TAC (SPECL ["m:num"; "n:num"] MULT_SYM)

?- n * m = (n * (m - 1)) + n

- USES
- 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.
- SEEALSO

HOL Kananaskis-14