# [isabelle] Quickcheck problem?

Dear all Isabelle users,

`I am playing a bit with Isabelle (MacOSX version, Isabelle2009-2.dmg)
``and had the following problem: quickcheck always answers
`
*** Term to be tested contains type variables
*** At command "quickcheck".

`whatever the theorem to be proved. I even tried with the example of the
``quickcheck paper:
`
---------------
theory ToyList3
imports Datatype
begin
datatype 'a list= Nil ("[]")
| Cons 'a "'a list" (infix "#" 65)
primrec take::"nat => 'a list => 'a list"
where
"take n [] = []" |
"take n (x # xs) =
(case n of
0 => [] |
Suc m => x # take m xs)"
primrec drop::"nat => 'a list => 'a list"
where
"drop n [] = []"|
"drop n (x # xs) =
(case n of
0 => x # xs |
Suc m => drop m xs)"
theorem "take j (drop i xs) = drop i (take j xs)"
quickcheck
------------
Note that nitpick succeeds to find a counterexample.
What did I do wrong?
Thanks in advance,
Thomas
--
Thomas Genet
IFSIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet

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