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



Andreas,

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?

Cheers

Mark

On 28 July 2017 at 10:47, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch
> 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.