Re: [isabelle] What do the predicate compilation options such as inductify and random_dseq do?



Dear Mark,


On 31/07/17 11:11, Mark Wassell wrote:
My general interest is understand in detail how the code generation for inductive predicates works. My specific interest in random_dseq is in being able to randomly generate terms in a language from its inductive definition (for example terms of a particular type) and to do so in a manner where I have some control over the distribution. I was wondering if the options to random_dseq in the values statement provided this control or similar.

Sorry, I cannot help you here. I've never used those smart generators.

I have read "Code Generation from Inductive Predicates in Isabelle/HOL" March 2009, Lukas Bulwahn. Is this the PhD thesis that you refer to?
No. This is the Lukas' Master's thesis on the predicate compiler. It contains a few more details about the predicate compiler, but not the integration with quickcheck. Lukas' PhD thesis is available here:

https://mediatum.ub.tum.de/node?id=1115870

All the best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.