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,

Thomas

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"
   begin

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

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

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

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

Cheers
Lars



* see also Andreas Lochbihler's mail:
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00061.html>


--
Thomas Genet
ISTIC/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.