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

[Amine Chaieb]

I am also in favor of the set type-constructor. The issue of 
compatibility with other HOL provers could very probably be solved by 
the transfer mechanism. If not immediately from the generic setup, the 
surely from a tailored one dedicated to this issue, if enough people are 
concerned.

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