Next: Theorems with Parameters Up: The Tactic Language Previous: Semantics of Alternative Rule

Semantics of Other Special Operators

The operators *> and <* are binary operators on theorems; the result of the application of thm1 *> thm2, for example, is that thm2 is applied (in the usual direction) and then thm1 is applied if the application of thm2 succeeded.

The unary operator !! functions as a kind of ``inlining'' operator. The success or failure of application reported by !!thm => term is either failure if thm does not apply (this operator should normally be used with theorems which do not fail) or the success or failure of the last embedded theorem application at the top level of the term which results from the application of thm. The typical use of this is in case thm is of the form

?x = (thm1 => thm2 => ... thmn => ?x);
such a theorem is always applicable (and clearly true) and has the effect of causing a sequence of theorems to be applied; success/failure of !!thm would be success/failure of the application of thm1 in this example.

The on-success commands can be used for building guarded lists of commands to be executed; the inlining operator is provided to make certain kinds of defined operations on theorems behave sensibly. They do not interact with each other too well: theorems of the form (!! thm2) *> thm1 or thm2 *> (!! thm1) do not work in any useful way, but a theorem of the form !!(thm2 *> thm1) will work as expected. The problem is that the notion of success/failure is determined in different ways by the infixes *> and <* on the one hand and the inlining operator on the other. Using the criterion used by the guard infixes, the application of an inlined theorem always succeeds, though this may not be what the inlined theorem may report to a following theorem.

An equation term1 = term2 can be applied as an embedded theorem; the tactic interpreter will search for a theorem which justifies the equation, and apply such a theorem if it finds it. This is useful if one has forgotten the name of a theorem whose form one knows; more powerful possibilities arise from this, since it allows the tactic interpreter to construct possible theorems ``dynamically''.

Next: Theorems with Parameters Up: The Tactic Language Previous: Semantics of Alternative Rule

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997