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
|
\DOC new_definition
\TYPE {new_definition : ((string # term) -> thm)}
\SYNOPSIS
Declare a new constant and install a definitional axiom in the current theory.
\DESCRIBE
The function {new_definition} provides a facility for definitional
extensions to the current theory. It takes a pair argument consisting
of the name under which the resulting definition will be saved
in the current theory segment, and a term giving the desired definition. The
value returned by {new_definition} is a theorem which states the definition
requested by the user.
Let {v_1},...,{v_n} be tuples of distinct variables, containing the variables
{x_1,...,x_m}. Evaluating {new_definition (`name`, "c v_1 ... v_n = t")},
where {c} is not already a constant, declares the sequent {({{}},"\v_1 ...
v_n. t")} to be a definition in the current theory, and declares {c} to be
a new constant in the current theory with this definition as its specification.
This constant specification is returned as a theorem with the form
{
|- !x_1 ... x_m. c v_1 ... v_n = t
}
\noindent and is saved in the current theory under
(the name) {name}. Optionally, the definitional term argument
may have any of its variables universally quantified.
\FAILURE
{new_definition} fails if called when HOL is not in draft mode. It also
fails if there is already an axiom, definition or specification of the given
name in the current theory segment; if {`c`} is already a constant in the
current theory or is not an allowed name for a constant; if {t} contains free
variables that are not in any of the variable structures {v_1}, ..., {v_n}
(this is equivalent to requiring {\v_1 ... v_n. t} to be a closed term); or if
any variable occurs more than once in {v_1, ..., v_n}. Finally, failure occurs
if there is a type variable in {v_1}, ..., {v_n} or {t} that does not occur in
the type of {c}.
\EXAMPLE
A NAND relation can be defined as follows.
{
#new_definition
(`NAND2`, "NAND2 (in_1,in_2) out = !t:num. out t = ~(in_1 t /\ in_2 t)");;
|- !in_1 in_2 out.
NAND2 (in_1,in_2)out = (!t. out t = ~(in_1 t /\ in_2 t))
}
\SEEALSO
new_binder_definition, new_gen_definition, new_infix_definition,
new_infix_list_rec_definition, new_prim_rec_definition,
new_list_rec_definition, new_prim_rec_definition, new_recursive_definition,
new_specification.
\ENDDOC
|
