[isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

[Andreas Lochbihler]

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 
top/bot/...).

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.

Andreas


On 11/07/14 13:22, Lawrence Paulson wrote:
> I’m afraid that I don’t even know what it is.
> Larry
>
>
> 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
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>