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

[Florian Haftmann]

Hi again,

inquit Brian:
> 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.

Important point. Similarly, the generaliziation of class instances from
set to fun has been a noteworthy contribution on its own.

inquit Makarius:
> I am more concerned about the general process of such upheavals, and hope that more time is taken this time to consider the moves.  In particular we are already a bit late in the release schedule, and things are supposed to converge soon. So anything that cannot be finished within very few weeks needs to be postponed. (People who have participated in the 2006/2007 release desaster know what I mean.) 

inquit Brian:
> As long as we put off reintroducing 'a set as a separate type, we will
> continue to accumulate more theories (like Multivariate_Analysis) that
> confuse sets and predicates. The job of introducing 'a set will only
> get more difficult the longer we wait. I would certainly like to see
> the job completed before the next release, although it might require
> more time than we have.

Putting aside that the discussion itself seems not yet finished
(although most voices speak in favor for set, I would not want to
continue without considering Stefan's concerns), from my point of view
it is not realistic to reintroduce the set type constructor before the
next release because it opens too many uncertainties.

Let me briefly sum up where we are standing now: we have figured out
that it is possible in principle, and have found out how we can get
there rather smoothly: eliminate all set-pred mixture from theories and
make proofs robust to persist in both worlds.  Ultimately, this will
enable us to introduce set with a rather minimal-invasive changeset.
But before, there is still a lot of work to do, and (solvable but)
unexpected problems may lurk beyond the corner.  So, the best way now is
to continue eliminating set-pred mixture (also in the AFP of course!)
and discover problems in packages – I'm a little concerned about
quotient since this has been introduced after 2008, but maybe Cezary can
comment on this.  These tasks can proceed side-by-side with release
preparation since they only affect single theories or are independent of
the main repository.

When this is finished (and this will take some time, I guess beyond the
release – I will mail another report on this), we hopefully have learnt
enough to introduce 'a set again and then we have time to consider
2008's changesets thoroughly, discover and iron out remaining
deficiencies and make use of the benefits accordingly, which still will
take some time, but after release time should be available.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110817/8d98cfa0/attachment.sig>