[isabelle-dev] [isabelle] counter example checking from ML

[Florian Haftmann]

Hi Lucas,

indeed the whole quickcheck matter has grown into a complex story.

First, we currently (e.g. following development in the hg repository)
have a kind of fork:  there is the "old" quickcheck, residing in
Pure/codegen.ML, and the "new" one in HOL/Quickcheck.thy; the most
prominent difference between both is that the "new" one tries to
internalize as much as possible into the logic, which allows to use type
classes and avoids tinkering too much with glueing raw ML snippet
strings together.

Concerning determinism, the "old" quickcheck is inherently randomized.
The "new" one uses an open state monad which passes a random seed around
explicitly and can thus be also used to enforce determinism.  If you
want to use this, be aware of the pitfalls which arise when using
unofficial intermediate stages of development rather than official releases!

The key for understanding is in HOL/Tools/quickcheck_generators.ML,
function mk_generator_expr (export it on demand and try something like
Quickcheck_Generators.mk_generator_expr @{theory} @{term
"\<lambda>n::nat.  n ~= n^2"} [@{typ nat}]);  for further background
knowledge on this machinery, refer to §4.4 in
http://www4.in.tum.de/~haftmann/phd.shtml.  Don't hesitate to ask
further questions.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 260 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090921/6f30406b/attachment.sig>