[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
krauss at in.tum.de
Tue Aug 23 23:24:43 CEST 2011
On 08/23/2011 01:51 PM, Lawrence Paulson wrote:
> I'm starting to have doubts about this entire procedure.
> I thought the plan was to get these theories (particularly in the
> AFP) into a state where they no longer dependent on confusing sets
> with predicates so that they would work with either version of
Only where this is possible. The purpose of all this work is to see
where it is not possible and find out why. After all, these issues may
point to difficulties that users will later experience with the change
> I'm not sure that's possible. I got DataRefinementIBP
> working with the set-version, but now it doesn't work with the
> standard version. For one thing, it needs a class declaration for
> type set, which obviously cannot work with the standard version,
Shouldn't one remove quite a bit of duplication first? The classes
distributive_complete_lattice and complete_boolean_algebra are now part
of HOL (the former as complete_distrib_lattice) (see the FIXME). The set
instances for those should be in/go into Florian's HOL repository as well...
(but maybe you already did this???)
> other proofs also fail to work with the standard version.
I'd like to (and others probably too) look at those proofs. Is there
anything fundamental hidden there???
Can you send me a bundle of your changes, so that I can put them on the
web for people to look at?
- hg ci # commit your changes locally
- hg bundle SOME_FILENAME http://afp.hg.sourceforge.net/hgweb/afp/afp/
- send me the file SOME_FILENAME, created in the previous step
The second command will produce a file which contains all your
changesets that are not in the central afp repos (i.e., your new changes).
I'll put it up somewhere where people can look at it...
More information about the isabelle-dev