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



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.