1\DOC new_binder_definition
2
3\TYPE {new_binder_definition : string * term -> thm}
4
5\SYNOPSIS
6Defines a new constant, giving it the syntactic status of a binder.
7
8\DESCRIBE
9The function {new_binder_definition} provides a facility for making
10definitional extensions to the current theory by introducing a constant
11definition.  It takes a pair of arguments, consisting of the name under which
12the resulting theorem will be saved in the current theory segment and a term
13giving the desired definition.  The value returned by {new_binder_definition}
14is a theorem which states the definition requested by the user.
15
16Let {v1}, ..., {vn} be syntactically distinct tuples constructed from the
17variables {x1,...,xm}.  A binder is defined by evaluating
18{
19new_binder_definition (name, `b v1 ... vn = t`)
20}
21where {b} does not occur in {t}, all the free variables that
22occur in {t} are a subset of {x1,...,xn}, and the type
23of {b} has the form {(ty1->ty2)->ty3}.  This declares {b} to be a new
24constant with the syntactic status of a binder in the current theory, and with
25the definitional theorem
26{
27   |- !x1...xn. b v1 ... vn = t
28}
29as its specification.  This constant specification for {b} is saved
30in the current theory under the name {name} and is returned as a theorem.
31
32The equation supplied to {new_binder_definition} may optionally have any of its
33free variables universally quantified at the outermost level.  The constant {b}
34has binder status only after the definition has been made.
35
36\FAILURE
37{new_binder_definition} fails if {t} contains free
38variables that are not in any one of the variable structures {v1}, ..., {vn} or
39if any variable occurs more than once in {v1, ..., v2}.  Failure also occurs if
40the type of {b} is not of the form appropriate for a binder, namely a type of
41the form {(ty1->ty2)->ty3}.  Finally, failure occurs if there is a type
42variable in {v1}, ..., {vn} or {t} that does not occur in the type of {b}.
43
44\EXAMPLE
45The unique-existence quantifier {?!} is defined as follows.
46{
47- new_binder_definition
48     (`EXISTS_UNIQUE_DEF`,
49      Term`$?! = \P:(*->bool). ($? P) /\ (!x y. ((P x) /\ (P y)) ==> (x=y))`);
50
51> val it = |- $?! = (\P. $? P /\ (!x y. P x /\ P y ==> (x = y))) : thm
52}
53
54
55\COMMENTS
56It is a common practice among HOL users to write a {$} before the constant
57being defined as a binder to indicate that it will have a special syntactic
58status after the definition is made:
59{
60new_binder_definition(name, Term `$b = ... `);
61}
62This use of {$} is not necessary; but after the definition
63has been made {$} must, of course, be used if the syntactic status of {b}
64needs to be suppressed.
65
66\SEEALSO
67Definition.new_definition, boolSyntax.new_infixl_definition, boolSyntax.new_infixr_definition, Prim_rec.new_recursive_definition, TotalDefn.Define.
68\ENDDOC
69