SPECL : term list -> thm -> thm

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 CONDITIONS

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

EXAMPLE

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

  # let t = ARITH_RULE `!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)`;;
  val t : thm = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q

  # SPECL [`1`; `2`; `3`; `4`] t;;
  val it : thm = |- 1 <= 3 /\ 2 <= 4 ==> 1 + 2 <= 3 + 4

COMMENTS

In order to specialize variables while also instantiating types of polymorphic variables, use ISPECL instead.