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 codegeneration. To this end, we automated a more complex
construction of Joachim Breitner which is amenable for codegeneration, and
where the test check ys will only be performed once. In the
automation, one auxiliary type is created, and Isabelle's lifting and
transferpackage is invoked several times. 
BibTeX: 
@article{Lifting_Definition_OptionAFP,
author = {RenĂ© Thiemann},
title = {Lifting Definition Option},
journal = {Archive of Formal Proofs},
month = oct,
year = 2014,
note = {\url{http://isaafp.org/entries/Lifting_Definition_Option.html},
Formal proof development},
ISSN = {2150914x},
}
