On Thu, Aug 11, 2011 at 5:44 AM, Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> wrote: > 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
> 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 Working from a copy of Florian's repo, I have got HOLCF and HOL-Multivariate_Analysis working again. I transferred the changes back to the main repo as well: http://isabelle.in.tum.de/repos/isabelle/rev/bdcc11b2fdc8 http://isabelle.in.tum.de/repos/isabelle/rev/510ac30f44c0 > I estimate that half of these failures are marginal and are just due to > use of mem_def or Collect_def in proofs. Indeed, many of the changes are simply removing mem_def and Collect_def (possibly adding mem_Collect_eq) from calls to metis. HOLCF required one such change in Library/Infinite_Set.thy, removing Collect_def in a metis call. The other HOLCF changes were in ML code in packages: Specifically, when building terms, I was sometimes using "T --> boolT" instead of "mk_setT T". Overall, HOLCF was very good about respecting the distinction between sets and predicates, probably because most of it was written before 2008, back when 'a set and 'a => bool were actually distinct types. > 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. There was a lot more of this kind of thing in the Multivariate_Analysis libraries. This was to be expected, since much of it was written in 2009 or later, after 'a set became an abbreviation. In the case of "mono" used at type "'a set => bool", I ended up defining a separate constant called "mono_set". This seems to work just fine, although it is a user-visible change. In other cases, an single operation was defined in the library, and then used sometimes as a set, and other times as a predicate. In these situations, I had to decide on a specific type signature for each constant, and restate some lemmas accordingly. Making these decisions is not trivial, and requires a bit of understanding of the library involved, and how the constants defined in them are usually used. > 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. I have already started on this, and I will continue to do more. > 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. 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. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev