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

[Alexander Krauss]

On 08/19/2011 07:06 AM, Tobias Nipkow wrote:
>>> I think he omitted to mention type classes. It comes up again and again
>>> on the mailing list.
>>
>> Really?
>
> Yes. You yourself discovered right away that you cannot just treat a set
> like a predicate in this respect:
>
>    set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
>    func_plus: "f + g == (%x. f x + g x)"
>
> See the emails that Alex sent around recently. We gave up on set_plus.

Ok, this (and set_times, which is similar) is the only instance that I 
knew about, from the old thread.

At the time, we concluded that this one wasn't really so important, and 
I think I would still come to the same conclusion today: The difference 
between the current version and the old version 
(http://isabelle.in.tum.de/repos/isabelle/file/878c37886eed/src/HOL/Library/SetsAndFunctions.thy) 
is mostly notational (we still get the monoid lemmas by a locale 
interpretation), and even the type class version is not fully 
satisfactory compared with mathematical practice, where one would also 
ad-hoc-overload + to write x + A, which has to be x +o A in Isabelle.

> Later, people wanted to do just that more than once. Here is one instance:
>
> http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/1689/focus=1697
>
> There are others.

I wonder if there are also *different* instances, where we actually want 
"set" to be an instance of some type class, which cannot be achieved 
using "fun" and "bool". It seems that in 2008, no other instances had to 
be given up, but maybe new opportunities for use of classes arised after 
that? HOLCF? Multivariate_Analysis? My gut feeling is that there must be 
such cases, but I'd be much more confident if somebody actually showed 
me a few.

Alex