next up previous contents
Next: The Special Theorems EVAL Up: The Tactic Language Previous: Functional Programming in the

The Special Theorems RAISE and VALUE

The built-in theorem RAISE implements the semantics of the : unary operation on operators. In the case of ``flat'' operators (left and right type 0), the effect is to implement all equations like

(?x@?z) + (?y@?z) = (?x :+ ?y) @ ?z;
in other words, the effect of the colon operation is to produce a parallel operator on functions. The effect on operators with nontrivial relative type is the same in intent, but it is necessary to adjust types by appropriate introduction of constant function operators. The best way to find out how this works is by experiment. The RAISE theorem can be applied in the converse direction as well. The RAISE theorem only works on flat operators (without nontrivial left or right types) in a predicative theory.

The built-in theorem VALUE takes a parameter, and is intended to be applied to variable-binding contexts: the effect of applying VALUE @ [thm] to [term] is the same as the effect of executing [thm => term]. The reasons for the appearance of brackets around the parameter are technical. Limitations of matching into variable binding contexts originally forced this tactic to be provided as a primitive. These limitations no longer obtain; an equivalent theorem can be proved using limited higher-order matching.

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