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 -- 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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
