Abstract
We implemented a command that can be used to easily generate
elements of a restricted type {x :: 'a. P x},
provided the definition is of the form
f ys = (if check ys then Some(generate ys :: 'a) else None) where
ys is a list of variables y1 ... yn and
check ys ==> P(generate ys) can be proved.
In principle, such a definition is also directly possible using the lift_definition command. However, then this definition will not be suitable for code-generation. To this end, we automated a more complex construction of Joachim Breitner which is amenable for code-generation, and where the test check ys will only be performed once. In the automation, one auxiliary type is created, and Isabelle's lifting- and transfer-package is invoked several times.