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 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.