On 15/08/2014 09:30, Andreas Lochbihler wrote: > In 51aa30c9ee4e, I have added lattice instances for the Enum.finite_* types. > As > expected, this suffices for the quickcheck examples in > Quickcheck_Lattice_Examples (see 9225b2761126). > > This now raises the question what we should do with > HOL/Library/Quickcheck_Types. Within the Isabelle distribution and the AFP, > this > theory is no longer used anywhere. I expect that almost nobody relies on the > quickcheck setup in there. From the quickcheck point of view, we can therefore > drop this theory. Anyone who needs it can keep their own local copy. > > However, the constructions might still be useful, as the following comment > from > Peter Lammich's AFP entry Refine_Monadic shows. > > (* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides > an isomorphic contruction. *)
Peter, does that mean you could replace your specific construction by something in Quickcheck_Types.thy? In that case I would recomment to keep Quickcheck_Types.thy (or some part of it) alive, maybe under a less specific name, and Peter uses it in his AFP entry. Tobias > So, should we keep Quickcheck_Types (maybe under a different name, say > Lattice_Constructions) or drop it? > > Andreas > > On 11/07/14 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. >> >> 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.haftm...@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-...@in.tum.de >>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>>>> >>>> _______________________________________________ >>>> isabelle-dev mailing list >>>> isabelle-...@in.tum.de >>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>> _______________________________________________ >>> isabelle-dev mailing list >>> isabelle-...@in.tum.de >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev