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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
\DOC new_binder_definition
\TYPE {new_binder_definition : ((string # term) -> thm)}
\SYNOPSIS
Defines a new constant, giving it the syntactic status of a binder.
\DESCRIBE
The function {new_binder_definition} provides a facility for making
definitional extensions to the current theory by introducing a constant
definition. It takes a pair of arguments, consisting of the name under which
the resulting theorem will be saved in the current theory segment and a term
giving the desired definition. The value returned by {new_binder_definition}
is a theorem which states the definition requested by the user.
Let {v1}, ..., {vn} be syntactically distinct tuples constructed from the
variables {x1,...,xm}. A binder is defined by evaluating
{
new_binder_definition (`name`, "b v1 ... vn = t")
}
\noindent where {b} is not already a constant, {b} does not occur in {t}, all
the free variables that occur in {t} are a subset of {x1,...,xn}, and the type
of {b} has the form `{(ty1->ty2)->ty3}'. This declares {b} to be a new
constant with the syntactic status of a binder in the current theory, and with
the definitional theorem
{
|- !x1...xn. b v1 ... vn = t
}
\noindent as its specification. This constant specification for {b} is saved
in the current theory under the name {name} and is returned as a theorem.
The equation supplied to {new_binder_definition} may optionally have any of its
free variables universally quantified at the outermost level. The constant {b}
has binder status only after the definition has been made.
\FAILURE
{new_binder_definition} fails if called when HOL is not in draft mode. It also
fails if there is already an axiom, definition or specification with the given
name in the current theory segment, if {`b`} 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 one of the variable structures {v1}, ..., {vn} or
if any variable occurs more than once in {v1, ..., v2}. Failure also occurs if
the type of {b} is not of the form appropriate for a binder, namely a type of
teh form `{(ty1->ty2)->ty3}'. Finally, failure occurs if there is a type
variable in {v1}, ..., {vn} or {t} that does not occur in the type of {b}.
\EXAMPLE
The unique-existence quantifier {?!} is defined as follows.
{
#new_binder_definition
(`EXISTS_UNIQUE_DEF`,
"$?! = \P:(*->bool). ($? P) /\ (!x y. ((P x) /\ (P y)) ==> (x=y))");;
|- $?! = (\P. $? P /\ (!x y. P x /\ P y ==> (x = y)))
}
\COMMENTS
It is a common practice among HOL users to write a {$} before the constant
being defined as a binder to indicate that it will have a special syntactic
status after the definition is made:
{
new_binder_definition(`name`, "$b = ... ");;
}
\noindent This use of {$} is not necessary; but after the definition
has been made {$} must, of course, be used if the syntactic status of {b}
needs to be suppressed.
\SEEALSO
new_definition, new_gen_definition, new_infix_definition,
new_infix_list_rec_definition, new_prim_rec_definition,
new_list_rec_definition, new_prim_rec_definition.
\ENDDOC
|
