*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Questions about theories distributed with Isabelle*From*: Josh Tilles <merelyapseudonym at gmail.com>*Date*: Sat, 27 Jul 2013 15:49:58 -0400

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

**Follow-Ups**:**Re: [isabelle] Questions about theories distributed with Isabelle***From:*Lars Noschinski

**Re: [isabelle] Questions about theories distributed with Isabelle***From:*Makarius

- Previous by Date: [isabelle] AFP: The Königsberg Bridge Problem and the Friendship Theorem
- Next by Date: [isabelle] AFP: IEEE Floating Points
- Previous by Thread: [isabelle] AFP: The Königsberg Bridge Problem and the Friendship Theorem
- Next by Thread: Re: [isabelle] Questions about theories distributed with Isabelle
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list