ISPEC : term -> thm -> thm

SYNOPSIS

Specializes a theorem, with type instantiation if necessary.

DESCRIPTION

This rule specializes a quantified variable as does SPEC; it differs from it in also instantiating the type if needed, both in the conclusion and hypotheses:

     A |- !x:ty.tm
  -----------------------  ISPEC `t:ty'`
   A[ty'/ty] |- tm[t/x]

(where t is free for x in tm, and ty' is an instance of ty).

FAILURE CONDITIONS

ISPEC fails if the input theorem is not universally quantified, or if the type of the given term is not an instance of the type of the quantified variable.

EXAMPLE

  # ISPEC `0` EQ_REFL;;
  val it : thm = |- 0 = 0

Note that the corresponding call to SPEC would fail because of the type mismatch:

  # SPEC `0` EQ_REFL;;
  Exception: Failure "SPEC".