SUBS_OCCS

Drule.SUBS_OCCS : (int list * thm) list -> thm -> thm

Makes substitutions in a theorem at specific occurrences of a term, using a list of equational theorems.

Given a list (l1,A1|-t1=v1),...,(ln,An|-tn=vn) and a theorem (A|-t), SUBS_OCCS simultaneously replaces each ti in t with vi, at the occurrences specified by the integers in the list li = [o1,...,ok] for each theorem Ai|-ti=vi.

     (l1,A1|-t1=v1) ... (ln,An|-tn=vn)  A|-t
   -------------------------------------------  SUBS_OCCS[(l1,A1|-t1=v1),...,
    A1 u ... An u A |- t[v1,...,vn/t1,...,tn]            (ln,An|-tn=vn)] (A|-t)

Failure

SUBS_OCCS [(l1,th1),...,(ln,thn)] (A|-t) fails if the conclusion of any theorem in the list is not an equation. No change is made to the theorem if the supplied occurrences li of the left-hand side of the conclusion of thi do not appear in t.

Example

The commutative law for addition

   - val thm = SPECL [Term `m:num`, Term`n:num`] arithmeticTheory.ADD_SYM;
   > val thm = |- m + n = n + m : thm

can be used for substituting only the second occurrence of the subterm m + n

   - SUBS_OCCS [([2],thm)]
               (ASSUME (Term `(n + m) + (m + n) = (m + n) + (m + n)`));
   > val it =  [.] |- n + m + (m + n) = n + m + (m + n) : thm

SUBS_OCCS is used when rewriting at specific occurrences of a term, and rules such as REWRITE_RULE, PURE_REWRITE_RULE, ONCE_REWRITE_RULE, and SUBS are too extensive or would diverge.

See also

Rewrite.ONCE_REWRITE_RULE, Rewrite.PURE_REWRITE_RULE, Rewrite.REWRITE_RULE, Drule.SUBS, Thm.SUBST, Rewrite.SUBST_MATCH