A few exercises in theorem processing

The realization of inference rules as the primitive operations of a type “theorem” in a type-safe programming language that has so well served LCF and its descendants may, it is suggested, be of interest aside from any immediate context of theorem proving or hardware or software verification. Using the general “conversions” introduced by Paulson, a couple of simple programming exercises with theorem data, imitative of list processing, are presented. An example of a potentially useful notational definition in the HOL object language is given as an application.