[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Alexander Krauss]

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

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

> 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???)

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

Alex