SPEC : term -> thm -> thm

SYNOPSIS
Specializes the conclusion of a theorem.

DESCRIPTION
When applied to a term u and a theorem A |- !x. t, then SPEC returns the theorem A |- t[u/x]. If necessary, variables will be renamed prior to the specialization to ensure that u is free for x in t, that is, no variables free in u become bound after substitution.
     A |- !x. t
   --------------  SPEC `u`
    A |- t[u/x]

FAILURE CONDITIONS
Fails if the theorem's conclusion is not universally quantified, or if x and u have different types.

EXAMPLE
The following example shows how SPEC renames bound variables if necessary, prior to substitution: a straightforward substitution would result in the clearly invalid theorem |- ~y ==> (!y. y ==> ~y).
  # let xv = `x:bool` and yv = `y:bool` in
         (GEN xv o DISCH xv o GEN yv o DISCH yv) (ASSUME xv);;
  val it : thm = |- !x. x ==> (!y. y ==> x)

  # SPEC `~y` it;;
  val it : thm = |- ~y ==> (!y'. y' ==> ~y)

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

SEE ALSO
GEN, GENL, GEN_ALL, ISPEC, ISPECL, SPECL, SPEC_ALL, SPEC_VAR.