This document describes the coding style used by the IsarMathLib project.
The primary objective of the coding style used by by the IsarMathLib project is readability. Any person familiar with the standard mathematical notation should be able to read and follow the proofs. With some effort from the coder, the Isar syntax can get very close to that goal. Here are the principles to follow, in the order of their importance:
Use only the declarative Isar style, no proofs using the old Isabelle style will be allowed in IsarMathlib.
Stay as close as you can to the natural language and standard mathematical notation.
Most of the steps in the proofs can be written in a form similar to
from (local facts) have (statement) using (theorems) by simp
I am sure many proofs in IsarMathLib can be shortened by doing some (eruletac a=a in wfon_induct, assumption, +blast intro! and I am not making this up) magic. We think a couple of additional lines of proof are worth it if we can avoid this low level ugliness. This also concerns naming of the notions you define. Whenever practical, try not to use keywords or names that are not words. If you define the set of integers, don't call them "int", call them Integers. If you define real numbers, don't call them "double".
Write LaTeX comments.
Comments should be written at the start of every theory file, every section, before every definition and theorem. The comments don't have to be very precise or long, but do need to provide some information. We hope that future proof browsers will allow to hyperlink the theorems referenced in the proof and show the comments. Also searching for theorems is easier to implement with the keywords in comments. However, creating an impression that the comments contain a paralel "informal proof" (an oxymoron) should be avoided.
Use locales to define notation.
In IsarMathLib locales are used to separate notation from notions. Mathematical notions are defined using the keyword "definition" on the global level. Locales define notation that is limited in scope. This allows to use different notation conventions in different contexts to describe the same underlying mathematical notions. For example we can use both multiplicative or additive notation for groups without introducing the notion of "additive" or "multiplicative" groups.
In IsarMathLib only notation definitions in locales are added to the simplifier. I think this is a good compromise between making the life easier for the authors and providing "no mystery" proofs with explicit references.
Use \<langle> and \<rangle> instead of "<" and ">" in the ordered pair notation.
Use {<x,E(x)>. x\<in>X} style of defining sets representing functions rather than {<x,y> \<in> X\<times>Y. y = E(x)} style.
In Isar "then have" and "hence" are synonymous. IsarMathLib adopts a convention that "hence" indicates a direct consequence of the previous fact, without a need for any additional explicit references. So, write hence "a \<in> A" by simp, but if you need a reference write then have "a \<in> A" using theorem_10 by simp. The same applies to the "then show" and "thus" synonyms.
Be creative. IsarMathLib coding style is not set in stone and for sure it can be improved.