1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
\DOC new_type_definition
\TYPE {new_type_definition : string -> string * string -> thm -> thm}
\SYNOPSIS
Introduces a new type in bijection with a nonempty subset of an existing type.
\DESCRIBE
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)
}
\noindent 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)
}
\noindent 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)
}
\noindent so now types like {:(num)finiteset} make sense.
\FAILURE
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.
\SEEALSO
define_type, new_basic_type_definition, new_type_abbrev.
\ENDDOC
|
