1\DOC new_definition
2
3\TYPE {new_definition : string * term -> thm}
4
5\SYNOPSIS
6Declare a new constant and install a definitional axiom in the current theory.
7
8\DESCRIBE
9The function {new_definition} provides a facility for definitional
10extensions to the current theory.  It takes a pair argument consisting
11of the name under which the resulting definition will be saved
12in the current theory segment, and a term giving the desired definition.  The
13value returned by {new_definition} is a theorem which states the definition
14requested by the user.
15
16Let {v_1},...,{v_n} be tuples of distinct variables, containing the
17variables {x_1,...,x_m}.  Evaluating
18{new_definition (name, c v_1 ... v_n = t)}, where {c} is not
19already a constant, declares the sequent {({},\v_1 ... v_n. t)} to
20be a definition in the current theory, and declares {c} to be a new
21constant in the current theory with this definition as its
22specification. This constant specification is returned as a theorem
23with the form
24{
25   |- !x_1 ... x_m. c v_1 ... v_n = t
26}
27and is saved in the current theory under
28{name}.  Optionally, the definitional term argument
29may have any of its variables universally quantified.
30
31\FAILURE
32{new_definition} fails if {t} contains free variables that are not
33in {x_1}, ..., {x_m} (this is equivalent to requiring
34{\v_1 ... v_n. t} to be a closed term). Failure also occurs if
35any variable occurs more than once in {v_1, ..., v_n}.  Finally,
36failure occurs if there is a type variable in {v_1}, ..., {v_n} or
37{t} that does not occur in the type of {c}.
38
39\EXAMPLE
40A NAND relation can be defined as follows.
41{
42   - new_definition (
43       "NAND2",
44       Term`NAND2 (in_1,in_2) out = !t:num. out t = ~(in_1 t /\ in_2 t)`);
45
46   > val it =
47       |- !in_1 in_2 out.
48              NAND2 (in_1,in_2) out = !t. out t = ~(in_1 t /\ in_2 t)
49       : thm
50}
51
52
53\SEEALSO
54Definition.new_specification, boolSyntax.new_binder_definition, boolSyntax.new_infixl_definition, boolSyntax.new_infixr_definition, Prim_rec.new_recursive_definition, TotalDefn.Define.
55\ENDDOC
56