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.

Thu Sep 14 08:45:18 EDT 1995