define_finite_type : int -> thm

SYNOPSIS

Defines a new type of a specified finite size.

DESCRIPTION

The call define_finite_type n where n is a positive integer defines a new type also called simply `n', and returns a theorem asserting that its universe has size n, in the form:

  |- (:n) HAS_SIZE n

where (:n) is the customary HOL Light printing of the universe set UNIV:n->bool.

FAILURE CONDITIONS

Fails if n is zero or negative, or if there is a type of the same name (unless it was also defined by the same call for define_finite_type, which is perfectly permissible), or if the names of the type constructor and destructor functions are already in use:

  mk_auto_define_finite_type_n:num->n
  dest_auto_define_finite_type_n:32->num

EXAMPLE

Here we define a 32-element type, perhaps useful for indexing the bits of a word:

  # define_finite_type 32;;
  val it : thm = |- (:32) HAS_SIZE 32

USES

In conjunction with Cartesian powers such as real^3, where only the size of the indexing type is relevant and the simple name n is intuitive.

SEE ALSO

define_type, new_type_definition.