Stream: Beginner Questions

Topic: HOL-Algebra

view this post on Zulip John Hughes (Feb 10 2025 at 12:32):

Two presumably stupid questions

(1) I can't figure out how to import HOL-Algebra in my own theory.

(2) While trying to understand how quotients might be defined in structures like groups, so that one could prove the first isomorphism theorem, for instance (or do things with affine planes, as in my recent question), I thought I'd look at the HOL-Algebra theory itself. But on page 159 of https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL-Algebra/document.pdf
the term G mod H appears for the first time, and I cannot figure out where it came from. Can anyone explain?

(3) Is there a way that I could learn to answer question 2 myself? This chat is great, but it'd be even better if I could learn ways not to rely on it.

view this post on Zulip Christian Pardillo Laursen (Feb 10 2025 at 13:12):

(1) To import HOL-Algebra, import theory "HOL-Algebra.Algebra" at the top of your file. To load quickly, also load heap image HOL-Algebra when starting up Isabelle.
(2) To figure out where things come from, I load up Isabelle and control-click the term in question. In this particular case, Mod is defined in HOL/Algebra/Coset.thy

view this post on Zulip John Hughes (Feb 10 2025 at 15:17):

Thanks. I suppose that if I could have loaded HOL-Algebra.Algebra, I could have clicked on the term -- I already knew how to do that.

I did try to import HOL-Algebra, thinking that I was reading a document describing a theory of that name, but got
image.png

I'm not sure where the "DRAFT" came from, and I still don't know why importing that theory didn't work (although given how long HOL-Algebra.Algebra took to load, I can see that it might have taken a very long time!) I guess the lesson here is that I should have typed

import Alge

and paused until options showed up, and then used "tab" to select one, which would have had the quotation marks (which I left out earlier when trying it for myself) automatically included.

I'm including all this not as. a question, but so that some future person might find it helpful.

view this post on Zulip Christian Pardillo Laursen (Feb 10 2025 at 15:23):

So HOL-Algebra is the name of the session, but you can only import theories. The toplevel theory of HOL-Algebra is called Algebra - this is just standard naming practice for the standard libraries.

view this post on Zulip Christian Pardillo Laursen (Feb 10 2025 at 15:24):

The loading time is why i suggested the heap image - if you load it, by running isabelle jedit -l HOL-Algebra, you'll only have to build once and it'll load instantly after that

Last updated: Mar 09 2025 at 12:28 UTC