Theory

A theory consists of a list of theorems, a list of constant declarations, and some auxiliary lists of declarations. Theories can be saved to and loaded from files.

The lists which comprise a theory at this time (other than lists used by the parser which will be discussed below under Term) are

CONSTANTS:

Master list of constant declarations. Contains all identifiers and operators; for operators, reports the relative types of their arguments. Now contains comments.

THEOREMS:

Master list of theorems. For the structure of a theorem, see above.

PRETHEOREMS:

List of identifiers or operators which will eventually be proved as theorems (needed for recursive theorem definitions).

DEFINITIONS:

List of defined identifiers and operators with their defining theorems.

PROGRAMS:

List of bindings of identifiers and operators to theorems used for simulation of functional programming.

OPAQUE:

List of operators declared as opaque to abstraction.

These could reasonably be collapsed into one or two master lists. Additional lists used by the parser referenced under Term below are also an essential part of a theory.

Theory commands include the following:

declareconstant <string>:

Declare an identifier as a constant.

declaretypedinfix <integer> <integer> <string>:

Declare an infix. The string is its form; the integers are the ``relative types'' of its left and right arguments.

declareinfix <string>:

Declare a ``flat'' infix (with both relative types 0)

declareunary <string>:

Declare a unary prefix (its default left argument will be defaultprefix).

newcomment <string> <string>:

Enter new comments (the second string) on the declared object named by the first string (any older comments will be superseded). These will be displayed by declaration and theorem display commands.

appendcomment <string> <string>:

As newcomment, except that comments are appended to existing comments.

makeunary <string>:

Give an existing infix the default left argument defaultprefix.

declarepretheorem <string>:

Declare an identifier (or infix) as a prospective theorem (so that it can be introduced as an embedded theorem; useful in cases of recursion).

declareopaque <string>:

Declare an operator as opaque to abstraction. Used to declare new operator; an existing operator cannot be made opaque.

makescin or makescout <string> <string>:

These commands allow the user to declare the function or operator denoted by the first string argument to have input or output (resp.) restricted to absolute types (strongly Cantorian sets). The second string argument must be the name of a theorem witnessing this fact.

proveprogram <string> <string>:

Bind to the constant or operator named by the first argument the theorem named by the second as a ``functional program''.

deprogram <string>:

Remove any program bound to the constant or operator named by the argument.

pushtheorem or pushtheorem2 <string> <string>:

Hide the theorem named by the first string in the module associated with the theorem named by the second string. The hidden theorem is only visible when the parent theorem is executing, but its name remains reserved. The first version of the command posts a comment to the declaration of the hidden theorem automatically; the second does not.

poptheorem or poptheorem2 <string> <string>:

Reverses the effect of pushtheorem. poptheorem posts a comment automatically to the declaration of the no longer hidden object; poptheorem2 does not.

axiom <string> <term> <term>:

Creates an axiom with name the first string argument, left side the second argument and right side the third argument. An axiom can be recognized by its list of axiom dependencies consisting of its own name. Axioms cannot take parameters, so the first argument does not need to be a term.

interaxiom <string>:

If the current subterm is an equation, makes it an axiom.

prove <term>:

Causes the equation expressed in the current proof environment to be recorded as a theorem with name and ``format'' determined by the term argument (the argument will be either the theorem name alone or the theorem name with a list of parameters). The theorem to be proved cannot already be a theorem, though it can be a pretheorem.

reprove <term>:

Allows one to change an existing theorem; the only restriction enforced is that the dependencies of the theorem cannot get stronger. Axioms and definitions cannot be reproven.

autoprove or autoreprove:

As ``prove'' or ``reprove'', except that the format of the theorem proved is the name of the current workspace. Especially useful in a workspace created by ``getleftside'', ``getrightside'' or ``autoedit''.

impredicative:

This command allows definitions of more general form and allows the built-in RAISE theorem to work on non-flat infixes. The default state of the prover is now impredicative.

defineconstant <term> <term>:

Introduce a theorem defining a constant, with the same name as that constant. The constant cannot previously have been declared. The first term is a constant name or a constant applied to a list or lists of parameters, which is the left side of the intended theorem; the second term is the right side of the intended theorem. The structure of the definition is checked. Definitions are recorded in dependency lists like axioms.

definetypedinfix <string> <integer> <integer> <term> <term>:

As defineconstant, except that an infix with specified left and right types is defined. The first string argument is the name of the theorem to be added (since a solitary infix is not a theorem name). The fourth and fifth arguments correspond to the arguments of defineconstant.

defineinfix <string> <term> <term>:

Defines ``flat'' infixes (with both relative types 0). The first argument is the theorem to be added; the second and third correspond to the arguments of defineconstant.

defineitconstant, defineittypedinfix, defineitinfix:

have arguments as above, except for the last, which is replaced by the current subterm.

defineopaque <string> <term> <term>:

Defines opaque operators. The arguments are as for ``definetypedinfix'', with the omission of relative types. Stratification restrictions on the definition are removed, but the use of the defined function in definitions of anything non-opaque or in variable binding contexts is strongly restricted.

makeanaxiom <string>:

Makes the theorem indicated by the argument an axiom.

proveanaxiom <string>:

If the current proof environment contains a proof of an axiom named by the argument, make that axiom a theorem with the appropriate dependencies, making the appropriate adjustments of dependencies through the whole theory.

undefine <string>:

Convert the definition of the constant or operator named by the parameter to an axiom.

defineprimitive <string>:

If the theorem named by the argument is of the appropriate form to serve as the definition of an undefined notion, make it so.

redefineconstant <string>:

If the current proof environment could serve as a definition of a constant now defined, make it so, with global dependency modifications as appropriate. The argument is the new name for the old definition theorem.

redefineinfix <string>:

If the current proof environment could serve as a definition of an operator now defined, make it so, with global dependency modifications as appropriate. The argument is the name of the new defining theorem.

Note:

The preceding commands support reaxiomatization of theories. This facility can also be used to support the use of as yet unproved lemmas.

thmdisplay <string>:

Displays a theorem. Displays comments. Displays names of module components (hidden theorems) but not their contents.

showalltheorems:

Displays all theorems (in a loop from which any key other than Enter breaks out).

moddisplay <string>:

Displays a module (a theorem and all theorems hidden in its module).

showallmodules:

Displays all modules (in a loop from which any key other than Enter breaks out).

showrelevantthms:

Displays all theorems which match (or whose converses match) the current subterm nontrivially (i.e., it does not display theorems which match all terms).

showmatchthm <term>:

Displays a theorem (if there are any) which justifies the equation given as the argument.

showdec <string>:

Displays a constant or operator declaration. it shows relative types and default left arguments in the case of operators usable as prefixes. Displays comments.

showalldecs:

Shows all declarations (in a loop as with showalltheorems).