new_specification : string list -> thm -> thm

SYNOPSIS

Introduces 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 ["c1";...;"cn"] |- ?x1...xn. t

simultaneously introduces new constants named c1, ..., cn satisfying the property:

   |- t[c1,...,cn/x1,...,xn]

This theorem is returned by the call to new_specification.

FAILURE CONDITIONS

new_specification fails if any one of `c1`, ..., `cn` is already a constant.

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:

  # DIVMOD_EXIST_0;;
  val it : thm =
    |- !m n. ?q r. if n = 0 then q = 0 /\ r = 0 else m = q * n + r /\ r < n

Skolemizing it to made the parametrization explicit:

  # let th = REWRITE_RULE[SKOLEM_THM] DIVMOD_EXIST_0;;
  val th : thm =
    |- ?q r.
           !m n.
               if n = 0
               then q m n = 0 /\ r m n = 0
               else m = q m n * n + r m n /\ r m n < n

and then making the constant specification:

  # new_specification ["DIV"; "MOD"] th;;

giving the theorem:

  # DIVISION_0;;
  val it : thm =
    |- !m n.
           if n = 0
           then m DIV n = 0 /\ m MOD n = 0
           else m = m DIV n * n + m MOD n /\ m MOD n < n

SEE ALSO

define, new_definition.