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