SPEC

Thm.SPEC : term -> thm -> thm

Specializes the conclusion of a theorem.

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

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 val xv = Term `x:bool`
         and yv = Term `y:bool`
     in
       (GEN xv o DISCH xv o GEN yv o DISCH yv) (ASSUME xv)
     end;
   > val it = |- !x. x ==> !y. y ==> x : thm

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

See also

Drule.ISPEC, Drule.SPECL, Drule.SPEC_ALL, Drule.SPEC_VAR, Thm.GEN, Thm.GENL, Drule.GEN_ALL