Re: [isabelle] counter example checking from ML



Lucas Dixon wrote:
- how can I use quickcheck (or nitpick) from the ML level? and I would
love this to be in the Isabelle cookbook (shall I write an entry, once I
find out how to use it?)

Thanks to Omar for pointing this out to me, there is a high level interface for Quickcheck in src/Tools/quickcheck.ML, it has signature:

signature QUICKCHECK =
sig
  val auto: bool ref
  val auto_time_limit: int ref
val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    (string * term) list option
val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
end;

So this does much of what I'm after.

However, I'd like to also have access to:

fun test_goal quiet generator_name size iterations default_T insts i assms state = ...

which seems to be a useful function - I think I'd otherwise need to copy/rewrite chunks of it. Can this be added to the signature?

cheers,
lucas

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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