1\DOC new_definition 2 3\TYPE {new_definition : string * term -> thm} 4 5\SYNOPSIS 6Declare a new constant and install a definitional axiom in the current theory. 7 8\DESCRIBE 9The function {new_definition} provides a facility for definitional 10extensions to the current theory. It takes a pair argument consisting 11of the name under which the resulting definition will be saved 12in the current theory segment, and a term giving the desired definition. The 13value returned by {new_definition} is a theorem which states the definition 14requested by the user. 15 16Let {v_1},...,{v_n} be tuples of distinct variables, containing the 17variables {x_1,...,x_m}. Evaluating 18{new_definition (name, c v_1 ... v_n = t)}, where {c} is not 19already a constant, declares the sequent {({},\v_1 ... v_n. t)} to 20be a definition in the current theory, and declares {c} to be a new 21constant in the current theory with this definition as its 22specification. This constant specification is returned as a theorem 23with the form 24{ 25 |- !x_1 ... x_m. c v_1 ... v_n = t 26} 27and is saved in the current theory under 28{name}. Optionally, the definitional term argument 29may have any of its variables universally quantified. 30 31\FAILURE 32{new_definition} fails if {t} contains free variables that are not 33in {x_1}, ..., {x_m} (this is equivalent to requiring 34{\v_1 ... v_n. t} to be a closed term). Failure also occurs if 35any variable occurs more than once in {v_1, ..., v_n}. Finally, 36failure occurs if there is a type variable in {v_1}, ..., {v_n} or 37{t} that does not occur in the type of {c}. 38 39\EXAMPLE 40A NAND relation can be defined as follows. 41{ 42 - new_definition ( 43 "NAND2", 44 Term`NAND2 (in_1,in_2) out = !t:num. out t = ~(in_1 t /\ in_2 t)`); 45 46 > val it = 47 |- !in_1 in_2 out. 48 NAND2 (in_1,in_2) out = !t. out t = ~(in_1 t /\ in_2 t) 49 : thm 50} 51 52 53\SEEALSO 54Definition.new_specification, boolSyntax.new_binder_definition, boolSyntax.new_infixl_definition, boolSyntax.new_infixr_definition, Prim_rec.new_recursive_definition, TotalDefn.Define. 55\ENDDOC 56