Re: [isabelle-dev] [isabelle] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]
On 08/24/2011 08:30 PM, Florian Haftmann wrote: 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. Why exactly? From a naive POV sets and predicates are isomorphic and results about them could be transferred at any time. Not that I advocate this on a large scale, but where does this break down? Tools? Is this intrinsic or rather an artifact of Isabelle or HOL? I am asking because I still believe that one day (somewhat distant, even given my levels of optimism ^^) theorem proving will be modulo isomorphisms. I.e. Voevodsky et. al.'s vision should become true not only in the fancyful calculi they are designing. Cheers, Andy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]
> 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 signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]
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. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
