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