next up previous contents
Next: Simple Programming and Debugging Up: Tutorial Previous: Starting to Prove Something


MARK2 provides a facility for defining new constants:

defineconstant "Four" "2+2";

The effect of this command is to create a theorem with the same name ``Four'' as the constant being declared. The constant ``Four'' must not have been declared previously! Notice that the list of axioms on which this new theorem depends is empty; it is a ``freebie''. One cannot define a constant which depends on variables.

It is also possible to define new operators. For example, we can define a new infix ``**'' with the meaning ``sum of the squares of its arguments'' as follows:

defineinfix "SUMOFSQUARES" "?x**?y"  "(?x*?x)+?y*?y";

Note that the user needs to supply a name for the theorem encoding the definition.

It is also possible to define functions in the same general style as a mathematical definition like

The equivalent MARK2 definition looks like this (try it):

defineconstant "SampleFunction@?x" "(?x*?x)+?x";

The infix @ is a predeclared infix used to represent function application: the mathematical term f(x) would be written ?f@?x. Another predeclared infix is the comma, which is used to represent the ordered pair construction, and can also be used in parameterized definitions:

defineconstant "Add@?x,?y" "?x+?y";

defines a function of two variables encoding the addition operation.

It is possible to define higher-order functions and to define operator terms (prefix or infix) via their function values. Examples follow:

defineconstant "(Comp@?f,?g)@?x" "?f@?g@?x"  (* composition of
     functions *)
defineinfix "ADDFNS" "(?f++?g)@?x" "(?f@?x)+?g@?x"

There are restrictions on definitions having to do with the underlying type system of the prover. An example of a definition which will not succeed is

defineconstant "Diag@?x" "?x@?x";

We will not go into the details at this point; generally, if one defines functions which make sense mathematically, one will not run afoul of the type system (but don't try to define general terms from -calculus without reading about the details of the type system below).

The definition system is secure against circular definition or the presence of unacknowledged parameters.

The definition of any concept creates a theorem; one uses that theorem with ``ruleintro'' to eliminate the defined concept and that theorem with ``revruleintro'' to introduce the concept. Try out the following session:

defineconstant "Square@?x" "?x*?x";
start "(?a+?b)*(?a+?b)";
revruleintro "Square"; execute();
ruleintro "Square"; execute();

next up previous contents
Next: Simple Programming and Debugging Up: Tutorial Previous: Starting to Prove Something

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997