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

[Florian Haftmann]

envisaged working plan
----------------------

a) general
* continue discussion about having set or not, end with a summary (for
the mailing list archive)
* provide repository
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/ with
newest changesets from Isabelle main repository, keep HOL image building
(Florian)
* figure out with type class instances for set to add (maybe as a
provisory in a separate theory)
  > grep -rIPn '(instantatiation|instance).*(bool|"fun").*::' src/HOL
* examine changesets e8cc166ba123 to ec46381f149d for changes done to
packages etc., from there distill/assert necessary back-changes to
inductive_set etc.

b) elimination of set/pred mixture
* backport admissible changes from isabelle_set to isabelle (Florian)
* eliminate occurences of mem_set and Collect_def in distribution and
AFP theories AFAP, propagate back to main repository
* figure out problem with »force« in ex/Set_Theory.thy
* figure out problem with »refute« in ex/Refute_Examples.thy with
"distinct [a, b]" (examine changes done to refute since 2008)

c) consolidation
* get isabelle_set running
* (maybe)
  > hide_fact (open) Set.mem_def Set.Collect_def
  to indicate that something is going on with these

d) RELEASE

e) introduce set type constructor
* backport necessary changes (as little invasive as possible) from
isabelle_set
* distribute type class instances for set over theories appropriately
* add naive code generator setup for sets in Set.thy
* drop theory Executable_Set
* drop optional special type alias treatment in Pure/Isar/code.ML (Florian)
* drop theory CSet (naive version, maybe not quotient version)
* mark _apply rules for pointwise operations on functions as [simp]
* provide theories Dlist_Set, RBT_Set (or maybe Mapping_Set), etc.

	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/20110818/c161fed5/attachment.sig>