Re: [isabelle] Problem with quickcheck in Isabelle2015



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>




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