Primitively (Co)recursive Definitions for Isabelle/HOL

ABSTRACT. Isabelle/HOL has recently been enriched with a new definitional package for datatypes and codatatypes. The package introduces the specified types and derives auxiliary constants and characteristic theorems, notably (co)recursors and (co)induction principles. We now introduce support for high-level specifications of (co)recursive functions, in the form of three commands: primrec, primcorec, and primcorecursive. The new commands internally reduce the specifications to arguments to the (co)recursor and generate a number of theorems about the function definition, automating an otherwise tedious process.