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

[Florian Haftmann]

Hi again,

as feasibility study I re-introduced the good old set type constructor
at a recent revision in the history.  The result can be inspected at


http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329

This is by no means meant as a thorough treatment of the whole issue,
just to get some experience with which problem we would have to cope if
we would go ahead.

The whole work took approximately seven hours (excluding writing this
report).  As always which such things, the issue itself (re-introduction
of set) took approximately a quarter of the time, solving of
not-so-trivial problems (e.g. type check for set type in ML) a third,
and the rest was dedicated for re-engineering of poor proofs which
hindered the whole matter (btw. this has found its way to the main
repository already, e.g.
http://isabelle.in.tum.de/reports/Isabelle/rev/b5e7594061ce).  A
classification of the changes follows:

  Reintroduction of set type constructor itself:
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l15.7
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l23.1
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l15.40
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l1.16

  Correction of bad type annotations:
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l3.8

  Correction of predicate/set misfits:
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l8.9

  Tuning of metis proofs involving Collect_def or mem_def:
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l5.2

  Proof text quality improvement in order to facilitate migration:
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l10.117
  *
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l16.15

  Ad-hoc adaptations in packages:
  * Sledgehammer:
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l24.1
  * Meson:
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l19.7
  * Quotient:
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l21.7

These last changesets nicely demonstrate how the situation with sets
affects packages:
* some (sledgehammer) circumvent problems which would not occur with a
set type constructor
* for others (quotient) it is not clear how much effort a
re-introduction would cost (I doubt that there is any package which
inherently depends on the set-predicate identification)

The changes above were not systematic, just to get a HOL image built.
Then the following sessions fail:
  HOL-Algebra
  HOL-Auth
  HOLCF
  HOL-ex
  HOL-Hahn_Banach
  HOL-Hoare_Parallel
  HOL-IMP
  HOL-Imperative_HOL
  HOL-Induct
  HOL-Library
  HOL-Matrix
  HOL-Metis_Examples
  HOL-MicroJava
  HOL-Multivariate_Analysis
  HOL-Nitpick_Examples
  HOL-Nominal
  HOL-NSA
  HOL-Old_Number_Theory
  HOL-Predicate_Compile_Examples
  HOL-Quotient_Examples
  HOL-TPTP
  HOL-UNITY
  HOL-Word-SMT_Examples

I estimate that half of these failures are marginal and are just due to
use of mem_def or Collect_def in proofs.  In particular for
HOL-Quotient_Examples an elimination of the failure needs a careful
adaptation of the quotient package to the new situation.  Other failures
are caused by some constructs which somehow exploit the set-predicate
identification (Library/Cset.thy "set = member",
HOL-Multivariate_Analysis "mono (S :: 'a set ==> _"), but this can be
changed with comparably little effort.

What can be drawn for that?  If there is an agreement that
re-introducing set is a good idea, this requires some effort, but it is
not unrealistic.  A working plan could look like the following:

Step A
* eliminate predicate / set »misfits«
* eliminate proofs with mem_def / Collect_def
* repair proofs which fail in this ad-hoc adjustment setup
The advantage is that these quality improvements can be committed to
Isabelle as it is by now and do not demand a reintroduction of set
immediately, but eliminate obstacles later on.

Step B
* solve problems which existing packages (quotient)
* re-construct from relevant changesets what still has to be done to
keep the system consistent
* re-introduce 'a set

Step C
* cleaning up the situation: type class instantiations for sets,
appropriate simp rules for predicates, …
* code generation setup for sets

It should be self-evident that nothing beyond Step A can be undertaken
before the next release.

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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110811/18c08116/attachment.asc>