We now examine how some simple tactics are written.
One should think of tactics as mappings from proofs to proofs which may take
additional arguments.
The simplest tactics are formed using the ML
function ` refine_using_prl_rule`
.
This function takes two arguments, a token (the ML equivalent of a string)
and a proof. The token is parsed as a rule, and then the goal of the proof
is refined by this rule. Conceptually the result is a proof with
the top goal refined by the rule indicated by the token and with
the appropriate
subgoals for this refinement. Thus ` refine_using_prl_rule`
is a procedural embodiment
of the primitive refinement rules of
. The function ` refine_using_prl_rule`
is
an example of a tactic.

Atomic refinement steps and existing tactics may be combined using a
combining form called a * tactical* . For example, the
following tactic
refines a goal by ` intro`; then, each of the resultant subgoals is
again refined by ` intro`. To each of the subgoals of this the predefined
tactic ` immediate`
is applied.

let two_intro proof = (refine_using_prl_rule `intro` THEN refine_using_prl_rule `intro` THEN immediate) proof;;

The tactical ` THEN`
is an infix operator; it takes two tactics and produces
a new tactic. When applied to a proof this new tactic applies the tactic on
the left--hand side of the ` THEN`
and then, to each of the subgoals
resulting from the left--hand tactic, the right--hand tactic.
Note that ` two_intro` will only work if it * makes sense* to perform
two levels of introductions. For example, if the tactic is applied to a
dependent product (where an intro rule requires an object of the
left type) the refinement will fail, causing the tactic to fail.

In addition to
` THEN`
, two other tacticals are of general
usefulness: ` REPEAT`
and ` ORELSE`

. The
tactical ` REPEAT`
will repeatedly apply a tactic until the
tactic fails (or fails to do anything). That is, the tactic is applied to
the argument proof, and then to the children produced by tactics, and so on.
The ` REPEAT`
tactical will catch all failures of the argument tactic and can
not generate a failure. For example,

let intros = REPEAT (refine_using_prl_rule `intro`);;

will perform (simple) introduction until it no longer applies.
The ` ORELSE`
tactical takes two tactics as arguments and produces a tactic
that applies the --hand tactic to a proof and, if that tactic fails,
the right--hand tactic. The following tactic performs all simple
introductions and eliminations which are possible.

let goal_simplify = REPEAT ((refine_using_prl_rule `intro`) ORELSE (refine_using_prl_rule `elim`));;

Using ` refine_using_prl_rule`
, the four tacticals given here and the predefined
tactics, many useful tactics can be written. We hope that tactics are easy
enough to write and convenient enough to use that the user will be
encouraged to experiment with them. In particular, we hope that the user
will write tactics for any aspect of theorem proving that is repetitious,
stylized or routine.

The power and flexibility of the tactic mechanism go well beyond these simple examples. In chapter 9 we continue the discussion begun here.

Thu Sep 14 08:45:18 EDT 1995