new_specification : string * string list * thm  -> thm
STRUCTURE
SYNOPSIS
Introduce a constant or constants satisfying a given property.
DESCRIPTION
The ML function new_specification implements the primitive rule of constant specification for the HOL logic. Evaluating:
   new_specification (name, ["c1",...,"cn"], |- ?x1...xn. t)
simultaneously introduces new constants named c1,...,cn satisfying the property:
   |- t[c1,...,cn/x1,...,xn]
This theorem is stored, with name name, as a definition in the current theory segment. It is also returned by the call to new_specification.
FAILURE
new_specification fails if the theorem argument has assumptions or free variables. It also fails if the supplied constant names c1, ..., cn are not distinct. It also fails if the length of the existential prefix of the theorem is not at least n. Finally, failure occurs if some ci does not contain all the type variables that occur in the term ?x1...xn. t.
USES
new_specification can be used to introduce constants that satisfy a given property without having to make explicit equational constant definitions for them. For example, the built-in constants MOD and DIV are defined in the system by first proving the theorem:
   th |- ?MOD DIV.
           !n. 0 < n ==> !k. (k = (DIV k n * n) + MOD k n) /\ MOD k n < n
and then making the constant specification:
   new_specification ("DIVISION", ["MOD","DIV"], th)
This introduces the constants MOD and DIV with the defining property shown above.
COMMENTS
The introduced constants have a prefix parsing status. To alter this, use set_fixity. Typical fixity values are Binder, Infixl n, Infixr n, Prefix n, Suffix n, or Closefix.
SEEALSO
HOL  Trindemossen-1