SUBST_ALL_TAC : thm_tactic

- STRUCTURE
- SYNOPSIS
- Substitutes using a single equation in both the assumptions and conclusion of a goal.
- DESCRIPTION
- SUBST_ALL_TAC breaches the style of natural deduction, where the assumptions are kept fixed. Given a theorem A|-u=v and a goal ([t1;...;tn], t), SUBST_ALL_TAC (A|-u=v) transforms the assumptions t1,...,tn and the term t into t1[v/u],...,tn[v/u] and t[v/u] respectively, by substituting v for each free occurrence of u in both the assumptions and the conclusion of the goal.The assumptions of the theorem used to substitute with are not added to the assumptions of the goal, but they are recorded in the proof. If A is not a subset of the assumptions of the goal (up to alpha-conversion), then SUBST_ALL_TAC (A|-u=v) results in an invalid tactic.
{t1,...,tn} ?- t ================================= SUBST_ALL_TAC (A|-u=v) {t1[v/u],...,tn[v/u]} ?- t[v/u]

SUBST_ALL_TAC automatically renames bound variables to prevent free variables in v becoming bound after substitution.

- FAILURE
- SUBST_ALL_TAC th (A,t) fails if the conclusion of th is not an equation. No change is made to the goal if no occurrence of the left-hand side of th appears free in (A,t).
- EXAMPLE
- Simplifying both the assumption and the term in the goalby substituting with the theorem |- 0 + m = m for addition
{0 + m = n} ?- 0 + (0 + m) = n

results in the goalSUBST_ALL_TAC (CONJUNCT1 ADD_CLAUSES)

{m = n} ?- 0 + m = n

- SEEALSO

HOL Kananaskis-14