A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL

The nominal datatype package implements an infrastructure in Isabelle/HOL for defining languages involving binders and for reasoning conveniently about alpha-equivalence classes. Pitts stated some general conditions under which functions over alpha-equivalence classes can be defined by a form of structural recursion and gave a clever proof for the existence of a primitive-recursion combinator. We give a version of this proof that works directly over nominal datatypes and does not rely upon auxiliary constructions. We further introduce proving tools and a heuristic that made the automation of our proof tractable. This automation is an essential prerequisite for the nominal datatype package to become useful.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Christian Urban, Stefan Berghofer
• Keywords: Automated Reasoning, CADE 2006, Clever Proof, Nominal Datatype Package, Nominal Datatypes