Re: [isabelle] Questions about theories distributed with Isabelle
On 27.07.2013 21:49, Josh Tilles wrote:
First, the README<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/README.html>
to type-classes disparagingly. Does the Isabelle community at large believe
that "axiomatic type classes" cannot be "first-class citizens of the
logic"? If so, I'd be interested to know *why* that's the case, but it's
not required so don't spend too much time explaining.
The issue with type classes is that they only work with types. I.e., the
type class group can only used if the whole universe of a type is a
group. So e.g. the type int forms a group (Z). However, we cannot reason
about the subgroups of Z with the group typeclass.
So, HOL-Algebra does use an explicit domain set and locales instead of
type classes. This makes for a more cumbersome (as a user, you always
need to maintain that the elements you are talking about are elements of
the domain), but more general reasoning.
It seems plausible to me that some theories (particularly the dependencies
of Main and/or Complex_Main) would exist as means to some end, only to
compose into a more useful tool. Whereas other theories (certainly most
from IsarMathLib<http://isarmathlib.org/>) are meant as bodies of
mathematical knowledge. Is this a useful distinction to make when browsing
the Isabelle codebase? Does that distinction explain the difference between
Main's theories and Algebra's theories?
Yes, I think this is a good rule of thumb.
This archive was generated by a fusion of
Pipermail (Mailman edition) and