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

[Stefan Berghofer]

Florian Haftmann wrote:
> just do something like (unfold mem_def) and your proof will be a mess
> since you have switched to the "wrong world".

Like any definition of a primitive operator, mem_def is not really intended
to be unfolded by the user, so don't be surprised if your proof is a mess
after unfolding this definition. You wouldn't unfold the definitions of
logical operators like "conj" or "disj" either, except for proving
introduction- or elimination rules for these operators.

> * 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).

This sounds more like a problem with the underlying infrastructure that should
be fixed, rather than working around the problem by introducing new type constructors.
Can you give an example of a proof by induction, where eager eta expansion leads
to an unnecessarily complicated proof?

Greetings,
Stefan