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

[Florian Haftmann]

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

-------------- 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/20110825/cde8454e/attachment.sig>