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.