James Hanson (Feb 14 2024 at 17:22): James Hanson (Feb 14 2024 at 17:22):I'm trying to understand certain aspects of the existing HOL libraries for structuring a project.
In HOL/Boolean_Algebras.thy, Boolean algebras are defined in two different (related) ways. There's the abstract_boolean_algebra locale, which builds off of the abel_semigroup locale from elsewhere, then later there's the boolean_algebra class and the boolean_algebra sublocale of abstract_boolean_algebra.
Unpacking definitions, Boolean algebras end up being objects built on types in a direct way (i.e., everything in the underlying type is an element of the Boolean algebra). This is as opposed to the apparent design philosophy in HOL/Algebra/Group.thy where the group locale ultimately builds off of the partial_object record, which is a type 'a together with a designated subset carrier :: "'a set". My understanding is that this is so that we can smoothly get around not having dependent types (i.e., if we want to talk about an infinite family of groups, it will be implemented with the monoid_scheme record meaning that the groups' carriers will all be various subsets of some fixed set).
First of all, am I understanding the design principles here correctly?
Second of all, is the treatment of Boolean algebras in HOL/Boolean_Algebras.thy 'out of date' since it's not using something like the partial_object record? As it sits, there's no good way to talk about infinite families of Boolean algebras, right? (There very well might be issues involving optimizing automation that I don't understand here.)
Does this mean that if I want to do something that might require this, I should avoid the existing boolean_algebra locale?
Lukas Stevens (Feb 14 2024 at 17:42):About the first question.
The hierarchy of algebraic structures in HOL is sort of duplicated in HOL/Algebra because the one in HOL uses type classes which are nice for proving things within the type class since you don't need to worry about the carrier set. This, however, gives you weaker results as soon as you have a structure that does not cover the whole carrier type (you can use Types_To_Sets to remedy but it introduces a new axiom). For this reason, HOL/Algebra uses the explicit carrier sets.
James Hanson (Feb 14 2024 at 17:46):Thanks. If I don't care about consistency strength, is there any particular reason to avoid using Types_To_Sets?
Lukas Stevens (Feb 14 2024 at 17:50):To do reason about algebra, you should definitely use HOL-Algebra. If you just apply results, you might get away with Types_To_Sets. But Types_To_Sets is also not straightforward to use because you need to explicitly name all theorems that you want to transfer from the type class to the settting with the explicit carrier set. Sometimes using transfer in this setting is non-trivial. On the other side, it has definitely been used that way for non-trivial things. See here.
Lukas Stevens (Feb 14 2024 at 17:59):I think this also sort of answers the second question. To reason about infinite families of boolean algebras, you should use the HOL-Algebra style.
James Hanson (Feb 14 2024 at 18:00):Right okay, but this hasn't already been done somewhere, right? I would need to write that too?
Lukas Stevens (Feb 14 2024 at 18:05):I am not well versed about the content of HOL-Algebra. But I also don't find anything on search.isabelle.in.tum.de. So you probably need to do it yourself. You could of course use Types_To_Sets to get started and then work with the HOL-Algebra style from there.
Last updated: Apr 28 2024 at 12:28 UTC