Overview of commands for OpenTheory article files

1. Deduction Rules

Equality

  1. Equality is reflexive, symmetric, and transitive (for any type):
    refl sym trans
  2. Carry equality to more complicated terms
    absThm appThm
  3. Replace a statement by an equivalent statement:
    eqMp

Simplify terms

A λ-abstraction applied to an argument is equal to the result of substituting the argument:
betaConv

Rules about the relation between hypotheses and conclusion

  1. Implication is transitive.
    proveHyp
  2. Implication is antisymmetric. Mutual implication implies equivalence.
    deductAntisym
  3. Implication is reflexive. A statement implies itself.
    assume

Substitution

Substitute type variables and free term variables by specific values
subst

Interface with other packages or articles

  1. Introduce an assumption, which can be an unproved axiom or a statement to be proved in another article and to be imported from there:
    axiom
  2. Mark a theorem that has been derived for export, to be listed as a result of the theory or to be used in other articles:
    thm
The assumptions and theorems generated in this way are the result of reading the article. If the article was processed without error, this means that the theorems can be deduced from the assumptions.

Other commands that create theorems (see below)

defineConst defineConstList defineTypeOp

2. Variables

Variables are characterized by name and type.
var

3. Constants

Constants can be of three kinds:
  1. A constant can be introduced by giving just a name, with the intention of referring to a constant defined in another package or article.
    const
  2. A constant can be introduced as an abbreviation for another more complicated expression. Its definition becomes a theorem, and it can be used in other packages or articles.
    defineConst

    Several constants can be defined simultaneously, and this is combined with a substitution in a theorem:
    defineConstList

  3. In the defineTypeOp operation, two constants for the representation and abstraction function (rep and abs) are implicitly defined.

When a constant of the second and third category is defined, a Const object is generated on the stack. To use such a constant several times, this object must be saved to the dictionary and retrieved from there.

When comparing two terms for α-equivalence, constants of the first category are considered equal if they have the same name (and type). Constants of the second category are considered equal if they have the same name and were introduced with the same definition (up to α-equivalence?) including identical types. Constants of the third category are considered equal if they originate from the same defineTypeOp operation? (and have the same type). Constants of different categories are never considered equal.

It is possible to define and use different constants with the same name. However it is illegal to use two or more such constants which are not equal by the above rules in the assumptions and theorems that are the result of reading the article.

4. Terms

Basic terms

The basic building blocks for terms are variables and constants. To use them in a term, use the following commands:
varTerm constTerm

Build more complicated terms

Such a term is either a λ-abstraction "λx. A" or an application "f A":
absTerm appTerm

5. Types

Types are built up from more elementary types by using type operators. Type variables and nullary type operators are used as the basic building blocks. The following command applies a type operator to its argument types.
opType

Type variables
varType

Similar as for constants, there are two ways to make a type operator:

  1. By name
    typeOp
  2. By an explicit definition
    defineTypeOp
    This definition implicitly defines also two constants rep and abs, as mentioned above.
The rules governing the use of such defined type operators and the comparison between them are analogous to the rules for constants.

6. The dictionary and the stack; lists, strings, and numbers

The dictionary

Entries from the top of the stack can be stored in the dictionary and later retrieved from there (either keeping them in the dictionary or removing them).
def ref remove

The stack

pop

Lists

Lists are used to build parameters for other commands such as the arguments of type operators or the elements of a substitution.

Construction:
nil cons

Deconstruction into head and tail:
hdTl

Strings

Strings are used as names for variables, constants, type variables, and type operators; in addition, they can be arguments for the pragma command.

Numbers

Numbers are used as indices into the dictionary; and as an argument of the version command. (In addition, they might be arguments for the pragma command in future versions.)

7. Directives for the article reader

version pragma
Günter Rote, Aug 2015