new_type_definition : string -> string * string -> thm -> thm

SYNOPSIS

Introduces a new type in bijection with a nonempty subset of an existing type.

DESCRIPTION

The call new_basic_type_definition "ty" ("mk","dest") th where th is a theorem of the form |- ?x. P[x] (say x has type rep) will introduce a new type called ty plus two new constants mk:rep->ty and dest:ty->rep, and return a theorem asserting that mk and dest establish a bijection between the universe of the new type ty and the subset of the type rep identified by the predicate P:

  |- (!a. mk(dest a) = a) /\ (!r. P[r] <=> dest(mk r) = r)

If the theorem involves type variables A1,...,An then the new type will be an $n$-ary type constructor rather than a basic type. The theorem is needed to ensure that that set is nonempty; all types in HOL are nonempty.

EXAMPLE

Here we define a basic type with 7 elements:

  # let th = prove(`?x. x < 7`,EXISTS_TAC `0` THEN ARITH_TAC);;
  val th : thm = |- ?x. x < 7

  # let tybij = new_type_definition "7" ("mk_7","dest_7") th;;
  val tybij : thm =
    |- (!a. mk_7 (dest_7 a) = a) /\ (!r. r < 7 <=> dest_7 (mk_7 r) = r)

and here is a declaration of a type of finite sets over a base type, a unary type constructor:

  # let th = MESON[FINITE_RULES] `?s:A->bool. FINITE s`;;
   0..0..solved at 2
  CPU time (user): 0.
  val th : thm = |- ?s. FINITE s

  # let tybij = new_type_definition "finiteset" ("mk_fin","dest_fin") th;;
  val tybij : thm =
    |- (!a. mk_fin (dest_fin a) = a) /\
       (!r. FINITE r <=> dest_fin (mk_fin r) = r)

so now types like :(num)finiteset make sense.

FAILURE CONDITIONS

Fails if any of the type or constant names is already in use, if the two names mk and dest are the same, if the theorem has a nonempty list of hypotheses, if the conclusion of the theorem is not an existentially quantified term, or the conclusion contains free variables.