Alexander Krauss
## Partial and Nested Recursive Function Definitions in Higher-Order Logic

Based on inductive definitions, we develop a tool that automates the
definition of partial recursive functions in higher-order logic (HOL) and
provides appropriate proof rules for reasoning about them.
Termination is modeled by an inductive domain predicate which follows
the structure of the recursion. Since a partial induction rule is
available immediately, partial correctness properties can be proved
before termination is established. It turns out that this modularity
also facilitates termination arguments for total functions, in
particular for nested recursions.
Our tool is implemented as a definitional package extending
Isabelle/HOL. Various extensions provide convenience to the user:
pattern matching, default values, tail recursion, mutual recursion and
currying.

PDF document

Official version published at SpringerLink