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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
