Definition.new_specification

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

gen_new_specification, new_definition, new_binder_definition, new_infixl_definition, new_infixr_definition, Define, set_fixity