Nicolò Cavalleri (May 16 2021 at 23:59): Nicolò Cavalleri (May 16 2021 at 23:59):I am a bit confused about the HOL standard library organization as for algebraic structures: why is there a file "Groups.thy" and a file "Algebra.Group.thy"? Which of the two is the official? Also, why in the file "Groups.thy" algebraic structures are defined both as locales and as classes? What is the relation between them and which of the two is usually used?
Manuel Eberl (May 17 2021 at 08:18):HOL-Algebra (the stuff residing in the Algebra folder) is mostly intended for abstract algebra. It allows you to talk about things like subgroups. Also, it is historically older than locales and type classes (if I recall correctly) and its approach with operations records is a bit old-fashioned these days. People are still using it for abstract algebra formalisations occasionally, but people have been trying different approaches with some success lately (tagging @Anthony Bordg ).
The stuff from HOL.Groups has a more pragmatic flavour: it uses typeclasses to furnish types with a canonical group/ring/field/etc. structure, types such as nat, int, real, complex, 'a poly where you look at the type and immediately have a canonical algebraic structure on the entire type in mind.
Type classes are much nicer to use than the HOL-Algebra stuff, but they give you less flexibility. Once you say ‘int is a ring with these operations’, you can never change what the operations are ever again to look at a different ring structure on int, and you also can't look at a subset of int either. It has to be on the entire type universe. That also means that you cannot talk about e.g. subgroups or quotients (in most cases).
The reason why a group locale also exists is probably mainly because there are type classes for additive groups and for multiplicative ones and you want to avoid having to prove all the basic properties twice. Converting a locale to a type class is easy, so it makes sense to do as much as you can in a locale context first and then convert it to a type class in the end. In fact, this approach is somewhat similar to what @Anthony Bordg has been doing, except that I think his structures still have an explicit carrier set whereas the group locale does not. That makes things a lot easier, but again, you lose some flexibility (in particular subgroups).
Nicolò Cavalleri (May 17 2021 at 12:36):Thank you very much for such a complete answer
Nicolò Cavalleri (May 17 2021 at 12:40):Manuel Eberl said:
Converting a locale to a type class is easy, so it makes sense to do as much as you can in a locale context first and then convert it to a type class in the end.
This is not what has been done in the file Groups though, right? I mean it seems that there classes are built with a hierarchy from former classes and not on their corresponding locales
Nicolò Cavalleri (May 17 2021 at 12:42):Moreover I can't really find a type class for multiplicative groups, although I can find the locale and the type class for additive groups... What is it called?
Nicolò Cavalleri (May 17 2021 at 12:44):Can't one just develop a theory of subgroups for groups defined with type classes as other groups with a monomorphism into the given group?
Nicolò Cavalleri (May 17 2021 at 12:45):Also why can't one just use carriers with type classes (with fixes) just as one does with locales?
Nicolò Cavalleri (May 17 2021 at 12:54):And finally, if I understand correctly, the same approach was not used in the file Rings and in the file Fields, meaning that Rings and Fields have only been defined as type classes but not as locales. Why? My ultimate goal is to work with fields, and I am a bit lost as for what should I import
Manuel Eberl (May 17 2021 at 12:55):Nicolò Cavalleri said:
Moreover I can't really find a type class for multiplicative groups, although I can find the locale and the type class for additive groups... What is it called?
Bad example; I meant multiplicative monoids. There are no multiplicative groups because you always have 0 in the type and you can't have a multiplicative group when there's a 0.
Manuel Eberl (May 17 2021 at 12:58):Nicolò Cavalleri said:
And finally, if I understand correctly, the same approach was not used in the file Rings and in the file Fields, meaning that Rings and Fields have only been defined as type classes but not as locales. Why? My ultimate goal is to work with fields, and I am a bit lost as for what should I import
Probably because it doesn't pay off for the purpose for the standard library. The definitions in the standard library are not so much to do reasoning about algebraic structures, but rather just to set things up in such a way that you can use specific simple algebraic structures (like the field of real numbers etc.)
It depends on what you want to do with fields exactly. Anything fancy will probably require the kind of flexibility offered by HOL-Algebra. Although I must warn you that HOL-Algebra is very annoying to use. In my opinion, the basic algebra library is not in a great state in Isabelle at the moment. Maybe talk to @Anthony Bordg and see what his opinion is on that.
Last updated: Apr 27 2024 at 01:05 UTC