SPEC_ALL : thm -> thm

SYNOPSIS

Specializes the conclusion of a theorem with its own quantified variables.

DESCRIPTION

When applied to a theorem A |- !x1...xn. t, the inference rule SPEC_ALL returns the theorem A |- t[x1'/x1]...[xn'/xn] where the xi' are distinct variants of the corresponding xi, chosen to avoid clashes with any variables free in the assumption list. Normally xi' is just xi, in which case SPEC_ALL simply removes all universal quantifiers.

       A |- !x1...xn. t
   ---------------------------  SPEC_ALL
    A |- t[x1'/x1]...[xn'/xn]

FAILURE CONDITIONS

Never fails.

EXAMPLE

The following example shows how variables are also renamed to avoid clashing with those in assumptions.

  # let th = ADD_ASSUM `m = 1` ADD_SYM;;
  val th : thm = m = 1 |- !m n. m + n = n + m

  # SPEC_ALL th;;
  val it : thm = m = 1 |- m' + n = n + m'