Theory Commands

  Each theory has an identifier and is associated with a file  . Each theory also has a set of immediate ancestors which it is dependent on. Commands are provided to set up new theories, load theories, dump theories, and print theories.

Theories are named by ML strings. The conventions for naming theories are the same as for naming library objects explained at the beginning of this section. Each theory is associated with a file. The value of the ML reference variable theory_filenames : (string # string) list  is a list of pairs of theory names and names of associated files. The filenames include a full pathname, but do not have any extension. For example, a valid filename string is ~nuprl/lib/standard/core_1 . The actual file associated with a theory is this name with a .thy extension. Examine the theory_filenames variable to find out the theories that Nuprl knows about at a given time.

set_theory_filename theory-name file-name

Add entry in theory_filenames list for theory-name. If an entry already exists for theory-name, update that entry.

Show entry in theory_filenames list for theory-name.

Theory dependencies  are recorded by the value of the theory_ancestors : (string # string list) list  reference variable. Each entry in this list is a pair of a theory's name and a list of names of other theories that the theory is immediately dependent on. There are ML functions to compute the closure  of this graph  as and when necessary.

set_theory_ancestors theory-name theory-ancestor-list

Add entry in theory_ancestors list for theory-name. If an entry already exists for theory-name, update that entry.

Show entry in theory_ancestors list for theory-name.

Typically one adds a few dummy theories  to theory_ancestors to simplify the description of the ordering of theories.

The theories loaded in a Nuprl session are generally a subset of the theories that Nuprl knows about. Between sessions, modified theories should always be explicitly saved. The functions for loading and dumping theories are: load_theory theory-name

Load theory-name at the end of the library from the associated file. If theory-name has already been loaded, this function has no effect. Every non-theorem object is checked as it is loaded.

Load the theories named in theory-name-list at the end of the library, together with any ancestor theories that haven't yet been loaded. Theories are loaded in an order consistent with their dependencies. Every non-theorem object is checked as it is loaded.

dump theory-name to the associated file. This leaves the theory theory-name in place in the library.

Other utility functions are: list_theories () 

List all the currently loaded theories. This is very useful if you are not sure which theories are loaded and which not.

delete_theory theory-name

Delete theory-name from the current library. Does not affect the file associated with the theory.

Create print-files for theory-name. theory-name must be loaded for this to work. If the associated file-name is file-name, then two files are created; file-name.prl and file-name.tex. file-name.prl is a file viewable by an editor running with Nuprl's special 8-bit font. file-name.tex is a self-contained LaTeX version of the theory listing.

This is similar to short_print_theory except that proofs and extracts of all theorems are also included. The files created have names file-name _long.prl and file-name_long.tex.

The theory theory-name always begins with comment object theory-name _begin  and ends with comment object theory-name _end . The names of these objects are important. Most of the theory functions rely on these delimiter objects being named the way they are. However, the user is free to alter the contents of these objects to his or her liking. A useful function is:

add_theory_delimiters

theory-name

Add delimiter objects for the new theory theory-name to the end of the library.  

There are variants on the load functions which check (and therefore expand) theorem objects at load time. They are: load_fully_theory theory-name

Load theory-name at the end of the library from the associated file. If theory-name has already been loaded, this function has no effect. Every object is checked as it is loaded.

Load the theories named in theory-name-list at the end of the library, together with any ancestor theories that haven't yet been loaded. Theories are loaded in an order consistent with their dependencies. Every object is checked as it is loaded.