Suppose in this subsection that we have available the axioms ``COMM'': ?x+?y=?y+?x and ``ZERO'': 0+?x=?x+0.
An obvious theorem to prove (prove it) is ``COMMZERO'': ?x+0=?x.
But we usually feel that ``ZERO'' and ``COMMZERO'' are not really separate theorems; it would be nice to be able to express that adding zero on either side of a term leaves it unaffected. We will prove a theorem ``EITHERZERO'' which has this effect. The session proceeds as follows:
start "?x+?y"; ruleintro "ZER0"; ruleintro "COMMZERO"; prove "EITHERZERO1";
The theorem ``EITHERZERO1'' looks like this:
?x + ?y = COMMZERO => ZERO => ?x + ?y
Try applying it to terms ?x+0 and 0+?x. It seems to have the desired effect.
The reason that this works has to do with the way the ``execute'' command works. The command applies all embedded theorems, including ones introduced in the course of execution, always applying the innermost ones first. You can get a look at how it works by using the command
instead of ``execute'', then hitting return repeatedly. It will trace the execution of the various embedded theorems for you. The ``steps'' command can be used as a debugging tool. Use ``q'' to break out (it will stop automatically if the term stabilizes).
Now try applying the theorem ``EITHERZERO1'' to 0+?x+0. You should get ?x; the tactic got a little overenthusiastic. You can figure out why on your own or look at the execution using ``steps''. This behaviour can be corrected:
start "?x+?y"; ruleintro "COMM"; ruleintro "COMMZERO"; altrule(); (* see what happens? *) prove "EITHERZERO"; (* note difference in theorem names *)
The new theorem looks like this:
?x + ?y = COMMZERO =>> ZERO => ?x + ?y
The =>> infix represents an embedded theorem which will be applied only if the theorem which was to be applied immediately before was inapplicable to its target; so, if ``ZERO'' is applied, ``COMMZERO'' will not be applied; applying ``EITHERZERO'' to 0+?x+0 will give ?x+0 instead of ?x. An example of its use: apply the first of the four theorems x1, x2, x3, and x4 which can be applied to a term y, use x4 =>> x3 =>> x2 =>> x1 => y (the last one must be a => or nothing will happen at all!); this avoids the possibility that x1 might apply to y, and, say, x3 apply as well to the result, which might happen if => were used throughout. To apply a theorem in reverse only on failure of previous theorem, use <<=, which has the same relation to <= that =>> has to =>. The ability to construct a list of alternative theorems to be applied while being certain that the outcome will not be that several of them will be applied in sequence helps to make behaviour of complex theorems of this kind more predictable.
With ``EITHERZERO1'' and ``EITHERZERO'', we are already doing programming (recall that theorems which function as programs are called ``tactics''). But we can do much more impressive things.
We now develop a tactic which applies ``ZERO'' aggressively, removing every addition of zero that it can find!
The ``declarepretheorem'' command declares the identifier ``ZEROES'' and tells the prover that a theorem by this name will be forthcoming. Normally, the ``prove'' command takes care of this automatically, but this will not work in this case.
start "?x+?y"; right(); ruleintro "ZEROES"; up(); left(); ruleintro "ZEROES"; up();
The prover takes our word for it that there will soon be a theorem called ``ZEROES''.
ruleintro "EITHERZERO"; prove "ZEROES";
Something is very fishy here. The theorem ``ZEROES'', which looks like this:
?x + ?y = EITHERZERO => (ZEROES => ?x) + ZEROES => ?y
seems to be defined in terms of itself (which was why it was necessary to declare it)! Try applying this theorem to a complex sum with lots of parentheses and zeroes; it should hunt down and eliminate all the zeroes. Watch it at work with ``steps'' (use ``q'' to break out of ``steps'').
The reason that the recursion terminates is that embedded theorems simply disappear when applied to terms to which they are inapplicable; notice if you use ``steps'' that the applications of ``ZEROES'' to atomic terms do not produce further occurrences of ``ZEROES''. It is definitely possible to write recursive tactics which will not terminate, by the way; to break out of such a process, use Control-C and then use the top command to reset environment variables (and then use ``steps'' to see what went wrong).
The possibility of defining tactics in terms of themselves gives us the ``looping'' (actually recursive) control structure; the fact that theorems or tactics fail where they do not apply gives us a limited ``conditional'' control structure (refined by the use of =>> and <<= to construct lists of alternative theorems to be applied), which proves to be sufficient to break out of recursions. Elaborate mutual recursions are possible, and are useful in practice.
The tactic language built into MARK2 is itself a programming language. And programs written in this language are treated by the prover as equational theorems, stored with other theorems in saved theories on an equal footing.
An exercise would be to use the experience gained in writing the theorem ``FOIL'' assigned above to write a tactic ``EXPAND'' which aggressively expands terms written using addition and multiplication as far as possible, applying the distributive law (in either form) wherever possible. Another exercise is to write a theorem ``SUPERASSOC'' which will eliminate all parentheses from a complicated sum, by applying the theorem ``ASSOC'' until it is no longer possible to do so.