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.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
