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

[Tobias Nipkow]

Am 19/08/2011 00:10, schrieb Stefan Berghofer:
> Tobias Nipkow wrote:
>> Am 12/08/2011 11:27, schrieb Alexander Krauss:
>>> On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
>>>> The benefits of getting rid of set were smaller than expected but quite
>>>> a bit of pain was and is inflicted.
>>> Do you know of any more pain, apart from what Florian already mentioned?
>>
>> 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.

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.

Tobias

> 
>   http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/
> 
> cited by Brian and Alex, Brendan was worried about the fact that one could
> no longer declare arities for sets. In my reply to his mail, I pointed
> out that arities for sets could usually be rephrased as arities for functions
> and booleans. I also asked him to give a concrete example for an arity where
> this was not possible, but I never got a reply, so I assume that this is not
> so much of a problem.
> 
> Greetings,
> Stefan