1\DOC new_infixl_definition
2
3\TYPE {new_infixl_definition : string * term * int -> thm}
4
5\SYNOPSIS
6Declares a new left associative infix constant and installs a
7definition in the current theory.
8
9\DESCRIBE
10The function {new_infix_definition} provides a facility for
11definitional extensions to the current theory.  It takes a triple
12consisting of the name under which the resulting definition will be
13saved in the current theory segment, a term giving the desired
14definition and an integer giving the precedence of the infix.  The
15value returned by {new_infix_definition} is a theorem which states the
16definition requested by the user.
17
18Let {v_1} and {v_2} be tuples of distinct variables, containing the variables
19{x_1,...,x_m}.  Evaluating {new_infix_definition (name, ix v_1 v_2 = t)}
20declares the sequent {({},\v_1 v_2. t)} to be a definition in the
21current theory, and declares {ix} to be a new constant in the
22current theory with this definition as its specification.
23This constant specification is returned as a theorem with the form
24{
25   |- !x_1 ... x_m. v_1 ix v_2 = t
26}
27and is saved in the current theory under
28(the name) {name}.  Optionally, the definitional term argument
29may have any of its variables universally quantified.
30The constant {ix} has infix status only after the infix
31declaration has been processed.  It is therefore necessary to use
32the constant in normal prefix position when making the definition.
33
34\FAILURE
35{new_infixl_definition} fails if {t} contains free
36variables that are not in either of the variable structures {v_1} and
37{v_2} (this is equivalent to requiring {\v_1 v_2. t} to be a closed
38term); or if any variable occurs more than once in {v_1, v_2}.  It
39also fails if the precedence level chosen for the infix is already
40home to parsing rules of a different form of fixity (infixes
41associating in a different way, or suffixes, prefixes etc).  Finally,
42failure occurs if there is a type variable in {v_1}, ..., {v_n} or {t}
43that does not occur in the type of {ix}.
44
45\EXAMPLE
46The nand function can be defined as follows.
47{
48   - new_infix_definition
49    ("nand", ���$nand in_1 in_2 = ~(in_1 /\ in_2)���, 500);;
50   > val it = |- !in_1 in_2. in_1 nand in_2 = ~(in_1 /\ in_2) : thm
51}
52
53
54\COMMENTS
55It is a common practice among HOL users to write a {$} before
56the constant being defined as an infix to indicate that after the
57definition is made, it will have a special syntactic status; ie. to
58write:
59{
60   new_infixl_definition("ix_DEF", Term `$ix m n = ... `)
61}
62This use of {$} is not necessary; but after the definition
63has been made {$} must, of course, be used if the syntactic status
64needs to be suppressed.
65
66In releases of hol98 past Taupo 1, {new_infixl_definition} and its
67sister {new_infixr_definition} replace the old {new_infix_definition},
68which has been superseded.  Its behaviour was to define a right
69associative infix, so can be freely replaced by
70{new_infixr_definition}.
71
72\SEEALSO
73boolSyntax.new_binder_definition, Definition.new_definition, Definition.new_specification, boolSyntax.new_infixr_definition, Prim_rec.new_recursive_definition, TotalDefn.Define.
74\ENDDOC
75