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

[Tobias Nipkow]

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-dev at in.tum.de 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev