[isabelle] Questions about theories distributed with Isabelle



I was looking at the HOL-Algebra
"session"<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/index.html>
and
I had a few questions.

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.

Second, many of the theories listed in HOL-Algebra are topically similar to
theories included in HOL's Main. Why are they split out?
Examples:

Algebra's Group<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Group.html>
vs
Main's Groups <http://isabelle.in.tum.de/dist/library/HOL/Groups.html>

Algebra's Lattice<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Lattice.html>
vs
Main's Lattices <http://isabelle.in.tum.de/dist/library/HOL/Lattices.html>
 & Complete_Lattices<http://isabelle.in.tum.de/dist/library/HOL/Complete_Lattices.html>

Algebra's Bij<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Bij.html>
vs
Main's Fun <http://isabelle.in.tum.de/dist/library/HOL/Fun.html>

Algebra's FuncSet<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/FuncSet.html>
vs
a number of theories in Main.


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?

I'd really appreciate any answers —or even guidance— you can provide.
--Josh Tilles

(if it's useful to know anything about my background: I'm a programmer, not
a mathematician. I'm using Isabelle in conjunction with a few other
materials to review and explore math, but I'm probably won't venture
outside of upper-undergraduate-level mathematics for a while.)



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