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.

Fri Sep 5 16:28:58 MDT 1997