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

[Andreas Lochbihler]

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.

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
>