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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
