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>
refers
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.

  -- Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.