Tacticals

Tacticals  allow existing tactics to be combined to form new tactics. In chapter 6 we saw several example tactics formed by refine_using_prl_rule and the tacticals THEN, ORELSE and REPEAT. In this section we summarize all of the currently existing tacticals.

THEN :

The THEN  tactical is the composition functional for tactics. THEN defines a tactic which when invoked on a proof first applies and then, to each subgoal produced by , applies .

tac THENL :

The THENL  tactical is similar to the THEN tactical except that the second argument is a list of tactics rather than just one tactic. The resulting tactic applies tac, and then to each of the subgoals (a list of proofs) it applies the corresponding tactic from . If the number of subgoals is different from the number of tactics in , the tactic fails.

ORELSE :

The ORELSE  tactical creates a tactic which when applied to a proof first applies . If this application fails, or fails to make progress, then the result of the tactic is the application of to the proof. Otherwise it is the result that was returned by . This tactical gives a simple mechanism for handling failure of tactics.

REPEAT tac:

The REPEAT  tactical will repeatedly apply a tactic until the tactic fails. That is, the tactic is applied to the goal of the argument proof, and then to the subgoals produced by the tactic, and so on. The REPEAT tactical will catch all failures of the argument tactic and can not generate a failure.

COMPLETE tac:

The COMPLETE  tactical constructs a tactic which operates exactly like the argument tactic except that the new tactic will fail unless a complete proof was constructed by tac, i.e., the subgoal list is null.

PROGRESS tac:

The PROGRESS  tactical constructs a tactic which operates exactly like the argument tactic except that it fails unless the tactic when applied to a proof makes some progress toward a proof. In particular, it will fail if the subgoal list is the singleton list containing exactly the original proof.

TRY tac:

The TRY  tactical constructs a tactic which tries to apply tac to a proof; if this fails it returns the result of applying IDTAC to the proof. This insulates the context in which tac is being used from failures. This is often useful for the second argument of an application of the THEN tactical.