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

[Tobias Nipkow]

On 11/07/2014 13:43, Andreas Lochbihler wrote:
> 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.

It looks mildly useful. But then Qickcheck would need to use it, which it
currently obviously does not. If you (or somebody) is able to make that happen,
then I am in favour of reviving that theory.

Tobias

> 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
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev