Lemma Introduction
We often fail to prove something by reduction just because OBJ does not have a rewrite rule for some necessary fact, e.g., about the data values involved in the problem. In such a case, we can go off "to the side" to prove the result (in the form of an equation), assert it, and then use it to complete the reduction. Such an auxiliary result is called a lemma.

Our rule of lemma introduction is more general than this, because it allows introducing an auxiliary result at any point, provided it has been justified from the axioms available at that point. Here is how this looks as a proof goal reduction rule: 

     A |= P   ----> (A |= Q) and (A and Q) |= P
where Q is the "lemma". If Q has visible sort, and if the data algebra has been defined by initial algebra semantics, then in particular, induction can be used to prove Q.
[Next] [Prev] [Home] [BHome]
12 October 1996