next up previous contents index
Next: Equality and Simplification Up: Differences in the Previous: Introduction Rules

Elimination Rules

There is also a dual relationship between the elimination rules and an introduction rule for the corresponding elimination form. For instance, the union elimination rule has a goal of the form H >> T; the extracted code is a term of the form decide(z;;). Correspondingly there is an introduction rule with a goal of the form H >> decide(e;;) in . This rule states the general conditions under which we may introduce a decide. Notice that any decide introduced by an elimination rule will have a variable in the first argument position. However, the additional generality of the introduction is obtained at a price; it is not possible to produce the subgoals of the rule instance from the goal alone. Two parameters are needed: one to specify the union type, written using A|B, and one to specify the range type, written using . This additional complexity is part of the price of the increased expressiveness of the Nuprl logic.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995