The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Sticking with something merely to avoid change is not a strong argument. This time we know what we go back to and the real benefits (and the few losses). Hence I would be in favour.
Tobias Am 11/08/2011 14:43, schrieb Florian Haftmann: > Hello together, > > recently in some personal discussions the matter has arisen whether > there would be good reason to re-introduce the ancient set type > constructor. To open the discussion I have carried together some > arguments. I'm pretty sure there are further ones either pro or > contra, for which this mailing list seems a good place to collect > them. > > Why (I think) the current state concerning sets is a bad idea: * > There are two worlds (sets and predicates) which are logically the > same but syntactically different. Although the logic construction > suggests that you can switch easily between both, in practice you > can't – just do something like (unfold mem_def) and your proof will > be a mess since you have switched to the »wrong world«. * Similarly, > there is a vast proof search space for automated tools which is not > worth exploring since it leads to the »wrong world«, making vain > proof attempts lasting longer instead just failing. * The logical > identification of sets and predicates prevents some reasonable simp > rules on predicates: e.g. you cannot have (A |inf| B) x = A x & B x > because then expressions like »set xs |inter| set ys« behave > strangely if the are eta-expanded (e.g. due to induction). * The > missing abstraction for sets prevents straightforward code generation > for them (for the moment, the most pressing, but not the only > issue). > > What is your opinion? > > In a further e-mail I give some estimations I gained through some > experiments to figure out how feasible a re-introduction would be in > practice. > > Btw. the history of the set-elimination can be found here: > http://isabelle.in.tum.de/repos/isabelle/shortlog/26839 > > Cheers, Florian > > > > > _______________________________________________ isabelle-dev mailing > list isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev