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


Thank you for your reply.

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.

I have read "Code Generation from Inductive Predicates in Isabelle/HOL"
March 2009, Lukas Bulwahn. Is this the PhD thesis that you refer to?



On 28 July 2017 at 10:47, Andreas Lochbihler <andreas.lochbihler at
> wrote:

> Dear Mark,
> Unfortunately, I'm not aware of any detailed documentation for these
> options. The option inductify tries to infer intro and elim rules for
> constants that have not been defined with (co)inductive and then call the
> predicate compiler on those such that they can be part of the mode
> inference game. This is particularly useful if you have defined a predicate
> using a first-order formula with quantifiers and want to execute it. You
> might find something on this and random_dseq in Lukas Bulwahn's PhD thesis.
> What do you need these options for?
> Most of these random generators for quickcheck are not used much because
> quickcheck has been configured to use only exhaustive testing by default.
> Cheers,
> Andreas
> On 28/07/17 11:02, Mark Wassell wrote:
>> Hello,
>> In Predicate_Compile_Examples/Examples.thy there are the following uses
>> of
>> code_pred and value:
>> code_pred [inductify] Sâ1p .
>> code_pred [random_dseq inductify] Sâ1p .
>> values [random_dseq 5, 5, 5] 5 "{x. Sâ1p x}"
>> Is there any detailed documentation or description of what the compilation
>> options such as inductify and random_dseq do? Or will I need to read the
>> ML
>> ?
>> What I can tell from the equation lines is that these options result in
>> different code equations with the latter possibly enabling random
>> generation of the members of the inductive set in a quickcheck like
>> manner.
>> Cheers
>> Mark

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