Partial functions in ACL2

We describe a method for introducing "partial functions" into ACL2, that is, functions not defined everywhere. The function "definitions" are actually admitted via the encapsulation principle: the new function symbol is constrained to satisfy the appropriate equation. This is permitted only when a witness function can be exhibited, establishing that the constraint is satisfiable. Of particular interest is the observation that every tail recursive definition can be witnessed in ACL2. We describe a macro that allows the convenient introduction of arbitrary tail recursive functions, and we discuss how such functions can be used to prove theorems about state machine models without reasoning about "clocks" or counting the number of steps until termination. Our macro for introducing "partial functions" also permits a variety of other recursive schemes, and we briefly illustrate some of them.