Re: [isabelle] Problem with quickcheck in Isabelle2015

Dear Lars and Jasmin,

thank you for your answers.
The old_datatype is, at least, a workaround that I can use for some time until Jasmin successfully fix it ;-)

Best regards,


Le 03/09/2015 11:41, Lars Hupel a écrit :
Dear Thomas,

I have the following strange behavior of quickcheck on the following
simple theory:

datatype t= A | B "(t list)"

value "B [A,A]"

the "datatype" command has been replaced with a newer implementation since
Isabelle2012. That replacement also meant reimplementation of the old
facilities. Unfortunately, not everything was/could be implemented. I've
stumbled over the same problem before*: Quickcheck generators will only be
installed for datatypes without nested recursion.

Note that the old "datatype" command is still around:

   theory Scratch
   imports "~~/src/HOL/Library/Old_Datatype"

   old_datatype t= A | B "(t list)"

   fun f:: "t ⇒ bool" where "f _= True"

   lemma "f (x::t)= True"

There, the call succeeds. I wouldn't recommend using it, though.


* see also Andreas Lochbihler's mail:

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at

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