SUBST_MATCH
Rewrite.SUBST_MATCH : (thm -> thm -> thm)
Substitutes in one theorem using another, equational, theorem.
Given the theorems A|-u=v and A'|-t, SUBST_MATCH (A|-u=v) (A'|-t)
searches for one free instance of u in t, according to a top-down
left-to-right search strategy, and then substitutes the corresponding
instance of v.
A |- u=v A' |- t
-------------------- SUBST_MATCH (A|-u=v) (A'|-t)
A u A' |- t[v/u]
SUBST_MATCH allows only a free instance of u to be substituted for
in t. An instance which contain bound variables can be substituted for
by using rewriting rules such as REWRITE_RULE, PURE_REWRITE_RULE and
ONCE_REWRITE_RULE.
Failure
SUBST_MATCH th1 th2 fails if the conclusion of the theorem th1 is
not an equation. Moreover, SUBST_MATCH (A|-u=v) (A'|-t) fails if no
instance of u occurs in t, since the matching algorithm fails. No
change is made to the theorem (A'|-t) if instances of u occur in
t, but they are not free (see SUBS).
Example
The commutative law for addition
- val thm1 = SPECL [Term `m:num`, Term `n:num`] arithmeticTheory.ADD_SYM;
> val thm1 = |- m + n = n + m : thm
is used to apply substitutions, depending on the occurrence of free instances
- SUBST_MATCH thm1 (ASSUME (Term `(n + 1) + (m - 1) = m + n`));
> val it = [.] |- m - 1 + (n + 1) = m + n : thm
- SUBST_MATCH thm1 (ASSUME (Term `!n. (n + 1) + (m - 1) = m + n`));
> val it = [.] |- !n. n + 1 + (m - 1) = m + n : thm
SUBST_MATCH is used when rewriting with the rules such as
REWRITE_RULE, using a single theorem is too extensive or would
diverge. Moreover, applying SUBST_MATCH can be much faster than using
the rewriting rules.
See also
Rewrite.ONCE_REWRITE_RULE,
Rewrite.PURE_REWRITE_RULE,
Rewrite.REWRITE_RULE,
Drule.SUBS, Thm.SUBST