SUBS : thm list -> thm -> thm
Makes simple term substitutions in a theorem using a given list of theorems.
Term substitution in HOL is performed by replacing free subterms according to
the transformations specified by a list of equational theorems. Given a list
of theorems A1|-t1=v1,...,An|-tn=vn and a theorem A|-t, SUBS
simultaneously replaces each free occurrence of ti in t with vi:
No matching is involved; the occurrence of each ti being
substituted for must be a free in t (see SUBST_MATCH). An occurrence which
is not free can be substituted by using rewriting rules such as REWRITE_RULE,
PURE_REWRITE_RULE and ONCE_REWRITE_RULE.
A1|-t1=v1 ... An|-tn=vn A|-t
A1 u ... u An u A |- t[v1,...,vn/t1,...,tn] (A|-t)
- FAILURE CONDITIONS
SUBS [th1;...;thn] (A|-t) fails if the conclusion of each theorem in the list
is not an equation. No change is made to the theorem A |- t if no occurrence
of any left-hand side of the supplied equations appears in t.
Substitutions are made with the theorems
depending on the occurrence of free subterms
# let thm1 = SPEC_ALL ADD_SYM
and thm2 = SPEC_ALL(CONJUNCT1 ADD_CLAUSES);;
val thm1 : thm = |- m + n = n + m
val thm2 : thm = |- 0 + n = n
# SUBS [thm1; thm2] (ASSUME `(n + 0) + (0 + m) = m + n`);;
val it : thm = (n + 0) + 0 + m = m + n |- (n + 0) + 0 + m = n + m
# SUBS [thm1; thm2] (ASSUME `!n. (n + 0) + (0 + m) = m + n`);;
val it : thm = !n. (n + 0) + 0 + m = m + n |- !n. (n + 0) + 0 + m = m + n
SUBS can sometimes be used when rewriting (for example, with REWRITE_RULE)
would diverge and term instantiation is not needed. Moreover, applying the
substitution rules is often much faster than using the rewriting rules.
- SEE ALSO
ONCE_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE, SUBS_CONV.