[isabelle-dev] [isabelle] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]
florian.haftmann at informatik.tu-muenchen.de
Wed Aug 24 20:30:10 CEST 2011
> 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
* 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
The latter is surely needed, especially concerning mem_def; examples can
be found in
Recall most of those affected proofs have already adapted in the
Isabelle repository to keep this final transition minimal and compact.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev