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