[isabelle-dev] Group theory developments on Jacobson Basic Algebra

[Lawrence Paulson]

Clemens gave us a new formalisation of basic algebra that has many advantages over the earlier HOL-Algebra: https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html

Other AFP entries have added onto it. There is new material in Grothendieck_Schemes and I’ve prepared additional material for a pending submission. The question is what to do with all this.

One idea would be to put it all into Clemens’ original development, but that can’t be right because was his experiment on the formalisation of a particular textbook (by Jacobson). But would it be right to make a copy of this AFP entry and just keep adding to it over time? This also is not normal for the AFP. Or should it be added directly to the distribution?

Having a new copy would also make it easier to make changes to suit further developments. In particular, Clemens overloads the / symbol to denote division on groups, which could be irritating in contexts where people need real division.

Thoughts would be welcome!

Larry