VDM recursive functions in Isabelle/HOL

For recursive functions general principles of induction needs to be applied. Instead of verifying them directly using the Vienna Development Method Specification Language (VDM-SL), we suggest a translation to Isabelle/HOL. In this paper, the challenges of such a translation for recursive functions are presented. This is an extension of an existing translation and a VDM mathematical toolbox in Isabelle/HOL enabling support for recursive functions.