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

[Florian Haftmann]

> I'm starting to have doubts about this entire procedure.
> 
> I thought the plan was to get these theories (particularly in the AFP) into a state where they no longer dependent on confusing sets with predicates so that they would work with either version of Isabelle. I'm not sure that's possible. I got DataRefinementIBP working with the set-version, but now it doesn't work with the standard version. For one thing, it needs a class declaration for type set, which obviously cannot work with the standard version, but other proofs also fail to work with the standard version.
> 
> I don't think it's possible to have it both ways. We need to either say we are making this change (and then pushing it through) or not making this change.

Having full compatible versions indeed is illusive.  But we can aim for
the following:
* elimination set/pred mixture from specifications and propositions
* figure out problems in the infrastructure
* cleanup proofs that they are robust enough to be easily translated (in
florid style, replace apply-OF-tac-fancyoption-Proofs by robust Isar
proofs).

The latter is surely needed, especially concerning mem_def; examples can
be found in
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2
Recall most of those affected proofs have already adapted in the
Isabelle repository to keep this final transition minimal and compact.

	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/20110824/2897ee8c/attachment.sig>