[isabelle] quickcheck in locales



I'd like to use quickcheck and autoquickcheck when proving theorems inside locales. I'm using Isabelle2008. For example:

locale l =
  fixes a::nat
begin

fun foo :: "nat => nat" where
   "foo 0 = 0"
|  "foo (Suc n) = a + foo n"

end

lemma (in l) "foo n = a * n"
quickcheck

However, quickcheck complains with the following error:

*** Unable to generate code for term:
*** arbitrary
*** required by:
*** locale_quickcheck.l.foo_sumC, locale_quickcheck.l.foo, <Top>
*** At command "quickcheck".

Apparently the [code] attribute for foo that is installed by the function package is not being applied to l.foo.simps?

Thanks,
-john







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