[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.