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"

  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:

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