Isabelle/HOL has recently been enriched with a 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 commands internally reduce the specifications to arguments to the (co)recursors and generate a number of theorems about the function definition, automating an tedious process.
Paper draft