Drule.SPECL

STRUCTURE

SYNOPSIS

Specializes zero or more variables in the conclusion of a theorem.

DESCRIPTION

When applied to a term list [u1;...;un] and a theorem A |- !x1...xn. t, the inference rule SPECL returns the theorem A |- t[u1/x1]...[un/xn], where the substitutions are made sequentially left-to-right in the same way as for SPEC, with the same sort of alpha-conversions applied to t if necessary to ensure that no variables which are free in ui become bound after substitution.

       A |- !x1...xn. t
   --------------------------  SPECL [u1,...,un]
     A |- t[u1/x1]...[un/xn]

It is permissible for the term-list to be empty, in which case the application of SPECL has no effect.

FAILURE

Fails unless each of the terms is of the same type as that of the appropriate quantified variable in the original theorem.

EXAMPLE

The following is a specialization of a theorem from theory arithmetic.

   - arithmeticTheory.LESS_EQ_LESS_EQ_MONO;
   > val it = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q : thm

   - SPECL (map Term [`1`, `2`, `3`, `4`]) it;
   > val it = |- 1 <= 3 /\ 2 <= 4 ==> 1 + 2 <= 3 + 4 : thm

SEEALSO

GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPEC_ALL, SPEC_TAC