Hi all, thanks to many efforts (thanks particularly to Alex, Brian, Cezary, Larry) we already have gained some insights whether and how it would be technically possible to introduce a set type constructor.
As I see the whole story, we have to think carefully how we would proceed in order to manage such a transition smoothly. Currently, we are (re-)separating predicates and sets syntactically, for three reasons: a) figure out whether and how it can be done b) how invasive this is c) improve quality and robustness of proofs where necessary. So, for the moment, the purpose of http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set is to provide a HOL image with a set type constructor as basis for further exploration. It is not meant as any kind of fork, which would weaken our resources. To prevent this, we must try hard to re-propagate proof improvements, duplication elimination etc. to the main repositories. If any substantial is missing (e.g. type class instances for set type constructor), it must be added to isabelle_set in a suitable manner, as is done already here: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l10.42 http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l1.7 The remaining changes should be as little as possible; to be able to observe them, I organize isabelle_set that way that the last changeset is a merge of a genuine main isabelle revision with all the changes necessary to get HOL (and as many subsessions as possible) through. It is a challenge, with a limited time budget, to follow what is going on, and there is high chance I miss some question or similar. So, don't hesitate to ring the bell twice if you think your point got lost or you are stuck. In particular, I am currently not aware how much of the work on AFP theories has found its way back to the main repository or is still in the queue, and how big the discrepancies to a set-specific version still are. I think it is best to leave the AFP aside for the moment and figure out still existing problems in the distribution. According to my knowledge, the following session produce problems: HOL-ex FAILED HOL-Hoare_Parallel FAILED HOL-Nominal FAILED HOL-Library FAILED HOL-Metis_Examples FAILED HOL-MicroJava FAILED HOL-Nitpick_Examples FAILED HOL-Quotient_Examples FAILED HOL-Predicate_Compile_Examples FAILED HOL-Word-SMT_Examples FAILED HOL-TPTP FAILED HOL-Probability FAILED In ex/Set_Theory.thy, there is a non-terminating »force« proof, which is a little bit worrying since I guess that one worked in Isabelle2007. Maybe someone can inspect the history on that? Also Hoare_Parallel is non-terminating. Concerning the *_Examples session, assistance by the corresponding tool maintainers is necessary and appreciated. I guess HOL-Nominal, HOL-MicroJava, HOL-Probability are easily accessible sessions to tackle next. OK, so much to say on that topic by now. 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