One of the atomic types available in Nuprl is the type integer, called int. The availability of integers as an atomic type allows one to express a great deal of elementary number theory without much effort. The type int comes equipped with an induction form so that one can inductively define functions from integers to integers. In this section we illustrate how some number--theoretic predicates and functions can be defined in Nuprl and how number--theoretic theorems are stated.
We begin this section with an example of a simple theorem which will be proved
in chapter 4; we use this theorem to review how one enters theorems in the
system. The theorem asserts that for every pair of integers one can
find an integer whose value is 0 if the first of the original pair of
integers is less than the second and whose value is 1 if the first of the
original pair of integers is not less that the second. In this statement
there are a pair of quantifiers; the first is universal and the second is
existential. Accordingly we need the definitions for universal quantifiers
and existential quantifiers from figure 
. To state the theorm
in Nuprl
, one would first
create a name and place for the theorem using the commands discussed in
section 3.2. Then the theorem would be viewed and finally the text editor
would be invoked by clicking R on the mouse in <main proof goal>.
Once in the text editor the first symbols typed would be >>; after
this the text of the theorem can be typed. At this stage the definition
all2 is needed. We use it by first typing 
; this will put
the cursor in the command window with the I> prompt. Now one
types all2 followed by a carriage return. The definition will be
instantiated in the text editor. The appearance of the definition template
will be all <var>,<var>:<type>.<prop>. The variables x
and y can now
be entered as the first two parameters, and int can be entered as the
third parameter. The body of this universally quantified statement is
an existentially quantified statement. The last parameter, <prop>, in
the definition is instantiated by invoking the definition for some.
The first two arguments of this quantifier can be filled in as before.
The body of the inner quantified statement is a conjunction of the two
conditions appearing in the statement of the theorem and can be expressed
using the built--in relation < between integers and the definitions for
conjunction and negation. The final appearance of the theorem is as follows.
>>all x,y:int. some z:int.
(x<y => z=0) & (~x<y => z= 1)
This is a theorem whose proof will embody some computational content; the
existence proof will involve a procedure which computes z,
given x and y.
The following definitions suggest what some standard number theory looks like in Nuprl . We first define the predicate divides using the (built--in) mod function.
divides(<n>:int,<m>:int) == ( <m> mod <n> = 0 in int)The next definition defines the predicate prime on integers.
prime(<n:int>) ==
(1 < <n>) &
all k:int. ( (0 < k) &
(<n> mod k = 0 in int) ) =>
(k=1 in int) | (k=<n> in int)
Now these number--theoretic predicates can be used in conjunction with the
logic definitions to state theorems in number theory in the following
fashion.
>> all n:int. prime(n) | ~prime(n)
>> all n:int. some p:int. n<p & prime(p)
In stating number--theoretic propositions we come across our first examples of
Nuprl
theorems that have manifestly interesting
computational content.
The Nuprl
system can extract the procedure from the
proof. If we call the theorem t,
then
\n.(term_of(t)(n))is a function which takes a natural number to a prime which is greater than it, where the function term_of is the system function that performs function extraction . Similarly the proof of the first theorem above will involve giving a decision procedure for primality.
Another interesting theorem one can state in Nuprl is the remainder theorem :
>>all x:int. all y: int. some q:int. some r:int.
(y = (q*x + r) in int) & (0 <= r < x).
We assume that the term (0 <= r < x) has been defined to have its
usual meaning via a
definition.
Once again a proof would give rise to an algorithm for finding the
quotient and remainder resulting
from dividing two integers, and the
corresponding function would be extracted by the
system. This illustrates, in a very simple setting, the use of Nuprl
as a program synthesis tool.