We introduce AmiCo, a tool that extends a proof assistant, Isabelle/HOL, with flexible function definitions well beyond primitive corecursion. All definitions are certified by the assistant's inference kernel to guard against inconsistencies. A central notion is that of friends: functions that preserve the productivity of their arguments and that are allowed in corecursive call contexts. As new friends are registered, corecursion benefits by becoming more expressive. We describe the algorithms that allow the automatic synthesis and maintenance of friend infrastructure, ensuring a safe and comfortable journey from the user high-level specifications to the low-level foundational definitions. We show some substantial case studies where our approach makes a difference.
The final publication is available at link.springer.com.
Paper draft Supplementary material