Lemma and Hypothesis Conversions

The conversions here derive rewrite rules from lemmas and hypotheses. Formulae that are lemma goals or hypotheses are treated as having the structure of either simple or general universal formulae (see Section for definitions of these) . The consequents of these formulae must each be of form where r usually (but not always) an equivalence relation. Any relation r that is going to be recognized by the rewrite package must be initially declared to it. See Section for details.

The conversions described here all rewrite in a left-to-right  direction: they replace instances of a's by instances of b's. Each has a twin conversion that works right-to-left . These twins have the prefix Rev  to their names. For example, RevLemmaC is the twin to LemmaC.

LemmaC name

Considering name as a simple universal formula with consequent , LemmaC creates a conversion to rewrite instances of a to instances of b.

Considering hyp i as a simple universal formula with consequent , HypC creates a conversion to rewrite instances of a to instances of b.

LemmaC is an instance of

and HypC is an instance of

The arguments to these conversions are as follows:

n

indicates that the nth consequent of a general universal formula. If -1 is used for n then the formula is always treated as simple. In particular, a relation is treated as the relation in the consequent rather than part of the structure of a general universal formula.

hints 

is for supplying bindings for variables in the lemma that Nuprl 's matching routines can't guess on their own.

Tacs 

is used for conditional rewriting  . Conditional rewriting is when the antecedents of a formula are checked for validity before the rewrite rule is used.

Tactics in Tacs are paired up with subgoals formed from instantiated antecedents and each tactic is run on its corresponding subgoal. The rewrite goes through only if every tactic completely proves its subgoal.

If there are fewer Ts than antecedents, Ts is padded on the left up to the length of the antecedents with copies of the head of Ts. If Ts is empty, then the rewrite goes through unconditionally.

name

is the name of the lemma.

i

is the number of a hypothesis. As with tactics, hypotheses are considered to be numbered positively from the beginning of the list onwards, and numbered negatively from the end backwards. Occasionally, negative numbers can have unexpected results. See below for an explanation.

Other useful specializations of GenLemmaWithThenLC and GenHypWithThenLC are:

The hypothesis conversions described here derive their rewrite rules from local hypotheses  in the environments that they are presented with on their first applications (see Section ) for a description of what local hypotheses are). If the conversions are applied with conversionals such as HigherC or NthC that start applying their argument conversion at the top of a term, then the local hypothesis list is always the same as the hypothesis list of the sequent containing the clause being rewritten.

Older versions of the hypothesis conversions required that the environment from which the rewrite rule was to be captured be provided as a seperate argument to the conversion. This turned out in most instances to be rather clumsy.