Marco David (Mar 17 2023 at 11:33): Marco David (Mar 17 2023 at 11:33):Please see the question here:
https://proofassistants.stackexchange.com/questions/2030/why-are-modules-also-rings-in-the-hol-algebra-library
Manuel Eberl (Mar 29 2023 at 10:10):I vaguely remember that there was some problem with records not being flexible enough. Probably that you don't have multiple inheritance.
Manuel Eberl (Mar 29 2023 at 10:10):In any case it's important to distinguish the representation (the record) from the semantics (the locales group/ring/module).
Manuel Eberl (Mar 29 2023 at 10:11):The representation is indeed awkward and HOL-Algebra is generally a bit old-fashioned and not in a great state.
Manuel Eberl (Mar 29 2023 at 10:11):There is a newer algebra library in the AFP that was first made by Clemens Ballarin as an experiment and then developed more by @Anthony Bordg and others, but I think there is still a lot missing there.
Manuel Eberl (Mar 29 2023 at 10:12):Generally, people just haven't been as interested in doing abstract algebra in Isabelle as e.g. analysis/number theory and it's not 100% clear what the best way to do it is.
Last updated: Apr 26 2024 at 04:17 UTC