Download The Nuprl Proof Development System, Version 5 Reference Manual

4.1
The Library
Nuprl’s library is a mathematical and logical database. All library contents are represented by a
common basic data structure called objects. There are objects for theorems, definitions, inference
rules, tactics and other algorithms, comments and articles, objects that control the visual appearance of the mathematical notation, and objects that are used to organize other objects in theories
and directories. A library table binds objects to identifiers that are used when referring to them.
In contrast to previous releases of Nuprl, all library contents are kept in a persistent library
and are accessible (modulo permission restrictions) as soon as the Nuprl 5 system is started. The
library roughly operates like a data base: modifications to theories, such as creating, deleting, or
editing objects are immediately committed to the library. However, all changes may be undone if
necessary. A backup of all previous versions of an object is kept until is explicitly destroyed in a
garbage collection process, which enables a user to recover previous versions if needed.
The navigator shows information on a segment of the library, which is sometimes called the
user’s work space. The format of the navigator window is discussed in Section 4.2.1. Commands
for for browsing, searching, editing, and structuring library contents as well as for controlling the
navigator window and are discussed in Section 4.3. In the rest of this section we briefly explain the
internal structure of Nuprl’s library and its relation to the externally visible behavior of Nuprl.
4.1.1
Library Objects
Library objects the common representation of all the contents of Nuprl’s library. They are abstract
terms that are associated with a kind , a variety of properties, and possibly with extra data.
Abstract terms provide a uniform data structure for representing almost any kind of formal
content. They consist of an operator identifier, a list of parameters, and a list of bound subterms
(see Chapter 5 for a detailed description). The abstract term syntax makes sure that no predefined
structure is imposed on the contents of the library and makes parsing unnecessary. All visible
structure and notation is generated by the editor process, which consults display forms that describe
how to “read” an abstract term. The separation between internal representation and external
presentation makes formal notation extremely flexible and expressive, as it supports an almost
arbitrary syntax and allows information to be presented differently depending on context and the
preferences of the users of Nuprl.
The kind of an object is a description of the intended role of the abstract term. It allows making a distinction between theorems, definitions, tactics, comments, etc., and identifying structure
information when assembling theories. Currently the following kinds are defined
statement objects contain a proposition and (reference to) a proof. If the proof is complete, the
proposition is considered a theorem (or a lemma). Otherwise it is a conjecture. A statement
object for a complete theorem also contains the extract term of the theorem
proof objects contain Nuprl proofs, i.e. directed acyclic graphs of (references to) inference steps,
where the conclusion of a child inference is a premise of its parent inference. A proof is
complete if all its leaves are closed by inferences.
inference objects contain records of actual inference steps. These may consists of instances of
primitive rules, of tactics executions, or more generally of applications of inference engines
that are connected to the Nuprl library.
abstraction objects introduce the abstract definition of a new term.
32