[isabelle] Quickcheck for HOLCF domains?



I would like to use Isabelle's quickcheck facility for quickly testing lemmas in HOLCF before attempting to prove them. This seems to work fine for the simple lemma

  lemma "(LAM x. x) $ (Def x) = Def x"
  quickcheck

However, Isabelle's code generator doesn't seem to know what to do with constructors generated by HOLCF's domain package. Here is an example that the quickcheck method can't handle:

  domain D = B | C

  lemma "(LAM x. x) $ B = B"
  quickcheck

(I'm using development snapshot Isabelle_13-Jul-2005.) Instead, Isabelle generates the following error message:

  *** Unable to generate code for type:
  *** D
  *** required by:
  *** <Top>
  *** At command "quickcheck".

What is needed to add support for HOLCF's domain package to Isabelle's code generator?

Thanks,
-john






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