Recursive Boolean Functions In HOL
Flemming Littrup Andersen, Kim Dam Petersen · 2005
The HOL system supports mechanized verification of specifications in polymorphic Higher Order Logic. HOL has facilities for defining primitive recursive functions, but no support for defining non-primitive recursive functions. This paper presents a package for defining recursive boolean functions in HOL as the minimal or maximal fixed point of a boolean function transformer. The implementation of the package is based on the results on fixed points in complete lattices by Tarski. Two examples on how to use the package are given. Both examples describe the definition of recursive boolean functions for specifying properties of parallel programs. 1 Introduction The proof generating system HOL includes facilities for constructing primitive recursive functions over the predefined types num (non-negative numbers) and list (finite lists), tools have been made for defining recursive data types and primitive recursive functions over these [13, 5], but no facilities exist for constructing funct...