next up previous contents
Next: Semantics of Other Special Up: The Tactic Language Previous: Execution Order of the

Semantics of Alternative Rule Infixes

The semantics of the alternative rule infixes =>> and <<= reflect a need for finer control of the circumstances under which rules are applied. These should appear only in contexts like thm1 =>> thm2 =>> ... thmn =>> firstthm => term, where the directions of any arrows that appear can be reversed. Note that the last rule infix is not an alternative infix!

Once term becomes free of embedded theorems in the course of the execution of the tactic interpreter, an attempt is made to apply each of the theorems in the list, working from the inside out, until one applies, after which the remaining theorems linked with alternative infixes are ignored. Lists of alternative theorems linked with the standard rule infixes have the undesirable feature that more than one of the theorems might apply in an unexpected way.

The precise way in which this effect is achieved is that a theorem embedded via an alternative infix is executed only if the term to which it is applied is the result of an immediately preceding rewrite rule application at the top level which failed. Once an application succeeds, alternative rule applications are ignored (this will be iterated). This is the reason why the innermost infix must be standard; there is no preceding rule application to consider.

Theorems embedded with alternative infixes can be introduced using altruleintro, altrevruleintro. altrule can be used to toggle between alternative and standard infixes.

There is a theoretical inelegance about the alternative rule infixes; they probably ought to have the same structure as the ``on-sucess'' infixes discussed in the next subsection (i.e., the construction ?thm1 =>> ?thm2 => term ought to be (?thm1 =>> ?thm2) => term; the behaviour of the alternative infixes makes the effects of the tactic interpreters non-local in a way which would be avoided by such a change. However, non-locality is now pervasive, given variable binding and local hypotheses, so we are not planning to change this situation. It is interesting to observe that if the change described above were made and the precedence of the alternative infixes were set to 1, there would be no effect on the appearance of terms.


next up previous contents
Next: Semantics of Other Special Up: The Tactic Language Previous: Execution Order of the

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