next up previous contents
Next: Abstraction and Reduction Algorithms Up: Programming Style Previous: Basic Control Structures


The real power of the tactic language arises from the possibility of proving recursive or mutually recursive tactics. A simple example is an expansion tactic for algebra:

Suppose we have the following theorems available:

COMM:  ?x * ?y = ?y * ?x

DIST:  ?x * (?y + ?z) = (?x * ?y) + (?x * ?z)

COMMDIST:  (?x + ?y) * ?z = (?x * ?z) + (?y * ?z)

     (* COMMDIST is obviously provable from axioms COMM and DIST *)

We declare a pretheorem X and prove the following theorems (tactics):

X1:  ?x + ?y = (X => ?x) + (X => ?y)

X2:  ?x * ?y = X1 => COMMDIST =>> DIST => (X => ?x) * (X => ?y)

The tactic X1 is used to expand sums: it can be summarized by ``expand each term''.

The tactic X2 is used to expand products: it can be summarized by ``expand each factor, then apply the first appropriate of distributivity from the left and the right, then expand each term if the result is a sum''.

After proving these, the theorem X is anticlimactic:

X:  ?x = X1 =>> X2 => ?x

All that this tells us to do is to apply whichever of X1 and X2 might be appropriate. Note that X applies successfully to any term whatever; if one wanted to restrict circumstances under which X would be applied, one might want to use the *> or <* operator.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997