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

[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

-- 

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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110811/8ddb16cf/attachment.asc>