[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 11 14:44:27 CEST 2011
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>
More information about the isabelle-dev
mailing list