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

[Tobias Nipkow]

On 11/07/2014 15:54, Andreas Lochbihler wrote:
> Quickcheck does not use these types, because it is currently configures to only
> use the types finite_1 to finite_3 from Enum, because the finite_types parameter
> is set by default. Quickcheck internally also seems to work differently
> depending on whether the finite_types flag is set.
> 
> I have only little insight how the parameters affect the performance of
> quickcheck, but I remember that Quickcheck originally used int as a replacement.
> Quickcheck_Types clearly is from that time. However, int is an infinite type and
> therefore, quantifiers, set comprehensions and function equality are not
> executable. Later, he switched to the finite_X types, which instantiate enum,
> but not the other type classes.
> 
> Therefore, I recommend the following:
> 
> 1. Temporarily fix Quickcheck_Types such that it works again, but leave it in
> HOL/Library. Then, anyone who wants to use quickcheck with infinite types can do
> so. This way, the Quickcheck_Examples session can also be reactivated.

Thank you for that.

Tobias

> 2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X
> types instances of the lattice type class hierarchy. Probably most of the stuff
> in Quickcheck_Types can be adapted to work with the Enum types as well. Maybe
> even all the test cases in Quickcheck_Lattice_Examples work with the Enum types,
> too.
> 
> I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have
> time for step 2 before the fork of the release branch.
> 
> Andreas
> 
> 
> On 11/07/14 14:28, Tobias Nipkow wrote:
>>
>>
>> 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
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>