next up previous contents
Next: The Special Theorems RAISE Up: The Tactic Language Previous: Theorems with Parameters

Functional Programming in the Tactic Language

It is possible to use the proveprogram command to bind a theorem to a constant (representing a function) or operator in the object language. The theorem must have a form similar to that which a definition of the constant or operator would have if it had one, except that variables on the left side can be specialized and new variables might be introduced. The theorem will then be automatically applied by the tactic interpreter wherever the constant or operator appears. The effect is to implement higher order functional programming in the tactic language.

The unary delay operator # can be used to suppress application of the theorem bound to the appropriate constant or operator in a term (if f were a function with a bound theorem, #(f @ ?x) would be a term in which ``execution'' of f (application of the associated theorem) was suppressed; if ** were an operator to which a theorem was bound, #(?x ** ?y) would be a term in which its execution was suppressed. The delay operator is ignored by the matching function, and if a theorem is successfully applied to the ``delayed'' term, the delay operator is eliminated.

The unary operator ## implements full laziness; the term to which it is applied does not have embedded theorems applied at all unless and until a theorem is applied to the lazy term.

Use of the delay operator proves necessary when the bound theorem has several steps or cases, and so takes the form of the introduction of a number of other theorems to be applied in turn or as alternatives to the original term.

The execution order of conditional expressions of the form x || T , U is that the subterm x has all theorem applications carried out before T or U is touched; this is a context in which ``laziness'' can be implemented without any use of the delay prefixes.


next up previous contents
Next: The Special Theorems RAISE Up: The Tactic Language Previous: Theorems with Parameters

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