next up previous contents
Next: Execution Order of the Up: The Tactic Language Previous: Predeclared Operators

Basic Semantics of Rule Infixes

The denotation of a term thm => term is the same as the denotation of the term term. thm is expected to denote a theorem which will be applied as a rewrite rule to term when the tactic interpreter execute or the tactic debugger steps are invoked. If it turns out that the left side of thm does not match the structure of term, its ``application'' will have no effect on the presentation of term.

The denotation of thm <= term is similar, except that the theorem thm is to be applied in the opposite sense (when term matches the right side of the equation represented by thm rather than the left side).

In both cases, the rule is applied only at the top level of term; it is not applied to proper subterms.

The prover commands ruleintro, revruleintro are used to introduce an application of a theorem (given as the argument of the command) to the selected subterm of the right side of the current equation. The prover command droprule will eliminate a theorem application at the top level (this works for all four infixes).

See above for relaxation of stratification rules where embedded theorem applications are involved.

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