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.

Fri Sep 5 16:28:58 MDT 1997