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

[Brian Huffman]

On Fri, Aug 12, 2011 at 2:27 AM, Alexander Krauss <krauss at in.tum.de> wrote:
> What are, actually, the losses when going back? This has not yet been
> touched by this thread at all (except the compatibility/import issue
> mentioned by Brian), and at least myself I wouldn't feel comfortable
> answering this question just now...

I think the simplest solution to the import issue is just to use
predicates for everything, and don't try to map anything onto the
Isabelle set type. For example, set union and intersection in
HOL-Light can translate to "sup" and "inf" on predicates in Isabelle.
Since Isabelle has pretty good support for predicates now, I think
this would work well enough.

Overall, I must say that I am completely in favor of making set a
separate type again. But I also believe that the sets=predicates
experiment was not a waste of time, since it forced us to improve
Isabelle's infrastructure for defining and reasoning about predicates:
Consider the new inductive package, complete_lattice type classes,
etc.

Perhaps this is mostly just a personal preference, but I am also in
favor of having the standard Isabelle libraries emphasize (curried)
predicates more than sets. We have been moving in this direction for
the past few years, and I think that is a good thing. (For example, I
think a transitive closure operator on type 'a => 'a => bool is more
valuable than on ('a * 'a) set.) I think that library support for
predicates is the main thing that would allow importing from other
HOLs to work well, regardless of whether 'a set is a separate type or
not.

- Brian