Returns the hypotheses of a theorem.

Breaks a theorem into assumption list and conclusion.

Returns the name and assertion theorem for each asserted axiom.

Returns the name and assertion theorem for each defined constant.

Returns the constant names and assertion theorem for each group of specified constants.

Returns the name and assertion theorem for each defined type constant.

Returns the assertion theorem for the axiom with the supplied name.

Returns the assertion theorem for the defined constant with the supplied name.

Returns the assertion theorem for the specified constant with the supplied name.

Returns the assertion theorem for the defined type constant with the supplied name.

This is the assumption rule. It takes a boolean term, and returns a theorem stating that the term holds under the single assumption of the term itself.

This is the beta reduction rule. It takes a lambda abstraction application term, and returns a theorem stating that the application is equal to the lambda abstraction body but with all occurrences of the binding variable replaced with the application's argument, under no assumptions.

This is the implication introduction rule. It takes a boolean term and a theorem, and removes the term from the theorem's assumptions (if present) and adds it as an antecedent of the conclusion. Note that the term does not have to be in the assumptions of the supplied theorem for the rule to

This is the equality modus ponens rule. It takes an equality theorem and a second theorem, where the equality theorem's LHS is alpha-equivalent to the conclusion of the second theorem. It returns a theorem stating that the equality theorem's RHS holds, under the unioned assumptions of the supplied theorems.

This is the variable instantiation rule. It takes a variable instantiation list and a theorem, and performs a single parallel instantiation of the free variables in the theorem's assumptions and conclusion, according to the instantiation list. All free occurrences of instantiation list domain elements in the theorem get replaced. Each instantiation list domain element must be a variable, and each range element must have the same type as its corresponding domain element.

This is the type variable instantiation rule. It takes a type variable instantiation list and a theorem, and performs a single parallel instantiation of the type variables in the theorem's assumptions and conclusion, according to the instantiation list. All occurrences of instantiation list domain elements in the theorem get replaced. Each instantiation list domain element must be a type variable.

This is the equality congruence rule for lambda abstraction. It takes a variable and an equality theorem, and abstracts the variable from both sides of the theorem. The variable must not occur free in the assumptions of the supplied theorem.

This is the equality congruence rule for function application. It takes two equality theorems, and applies corresponding sides of the first theorem to the second, unioning the assumptions. The first theorem's LHS/ RHS must be functions with domain type equal to the type of the second theorem's LHS/RHS.

This is the modus ponens rule. It takes an implication theorem and a second theorem, where the implication theorem's antecedent is alpha- equivalent to the conclusion of the second theorem. It returns a theorem stating that the implication theorem's consequent holds, under the unioned assumptions of the supplied theorems.

This is the primitive axiom assertion command. It takes a string and a term. The string becomes the name of a new axiom in the theory, and must not be an existing axiom name. The term becomes the asserted axiom, and must be of boolean type and must not contain free variables. The resulting assertion theorem states that the supplied boolean term holds, under no assumptions. A note of the axiom is reported, and the assertion theorem is returned.

This is the primitive definition command for constants. It takes a string and a term. The string becomes the name of a new constant in the theory, and must not be the name of an existing constant. The term becomes the definition term for the new constant, and must not contain free vars, and must not contain tyvars that are not in its top-level type. The resulting definition theorem asserts that the new constant equals the supplied term, under no assumptions. A note of the definition is reported, and the definition theorem is returned.

This is the primitive specification command for constants. It takes a non-empty string list and an existentially quantified theorem. The strings correspond one-to-one to the names of the new constants to be added to the theory, and must not include any existing constant names. They also correspond one-to-one to the outer-quantified variables of the supplied existential theorem, in the same order, although they potentially have different names. The supplied existential theorem must have no free variables and no assumptions. Furthermore, its outer-quantified variables must each have the same type variables, and the body of the existential must not involve any other type variables.

This is the primitive definition command for type constants. It takes a string and a theorem. The string becomes the name of a new type constant in the theory, and must not be the name of an existing type constant. The theorem argument must have no assumptions and a conclusion of the form `?v. P v`, where `P` is the characteristic function (prescribing the subset of the representation type that is in bijection with a general instance of the new type constant), and the theorem itself establishes that the subset is non-empty. The predicate `P` must not contain free variables, and its number of type variables becomes the arity of the new type constant.

This is the reflexivity rule for equality. It takes a term, and returns a There are no restrictions on the supplied term. `t` -------- |- t = t

Axioms are stored in a dynamic lookup tree, indexed by axiom name.

Constant definitions are stored in a dynamic lookup tree, indexed by the name of the constant defined.

Constant specifications are stored in an association list, indexed by the list of names of the constants defined.