[isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
andreas.lochbihler at inf.ethz.ch
Fri Jul 11 13:43:14 CEST 2014
Quickcheck_Types defines a number of artificial types that quickcheck can use to
instantiate type variables that occur in a theorem. Normally, quickcheck instantiates them
with int provided that the sort constraints do not prevent this. In Enum.thy, there are
already the types finite_X that quickcheck uses for enumerable types (type class enum)
such that quantifiers can be unfolded into conjunctions or disjunctions.
The types in Quickcheck_Types now do the same for the lattices type class hierarchy,
because int and the finite_X types cannot be used for type variables with sort lattice (or
I believe that it should be fairly simple to adjust Quickcheck_Types to Isabelle2014.
However, this only makes sense if it becomes part of Main. Otherwise, it will remain just
a library theory that hardly anyone knows about and no one uses.
Moreover, we should make sure that Quickcheck_Types fits to the current code generator
setup for lattices. IIRC, Florian has reworked a lot there over the past years. At the
very least, we should have some test cases (e.g. in HOL/ex) to check that Quickcheck_Types
works as expected.
If there's consensus on reviving this theory, I can do the changes to Quickcheck_Types
such that Isabelle2014 digests it. This is probably all that can be done before the
release as most of us will be busy in Vienna next week. A move to Main is something for
the next release.
On 11/07/14 13:22, Lawrence Paulson wrote:
> I’m afraid that I don’t even know what it is.
> On 11 Jul 2014, at 12:21, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>> The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken
>> has not been addressed since before the last release.
>> So, which path to follow? Is there any interested in a serious repair
>> effort? Otherwise, we should honestly drop it.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev