Re: [isabelle] What naming will cause potential errors?
On Sun, 7 Apr 2013, Gottfried Barrow wrote:
For theorem names, I name many theorems starting with uppercase, which
seems to be contrary to the convention in the HOL sources.
I have good reason to do this, because I care more about following
mathematical notation conventions than following Isabelle coding
In some sense the "coding" conventioned deviated by accident (or on
purpose) from what you often see in informal "prose" text, but I would
consider this an improvement. We are not writing for the New York Times
Isabelle sources are coming from certain free-world Unixoid background
where lowercase is preferred. The ancient empire of IBM had enforced
all-caps variable names, and the advent of proper lowercase in ASCII was a
great relieve (together with the invention of the underscore as formal
I did not invent these conventions, but I do think that lower-case is
better for the mass of text. Incidently, Coq prefers capital names and
keywords by default, and just last year some hard-core Coq users pointed
this out as historical accident: it causes a lot of pain to press SHIFT so
often, especially in Proof General. The proposed solution was then to use
vi keyboard mapping for Emacs. (If this is madness, there is method in
Note that I normally don't argue about the ease of *writing* the sources,
since ease of *reading* has the prime priority. This is why the
underscore is important to separate words, and lower-case helps the
Western brain to gloss quickly over large bodies of text (this is why the
scribes of Charlemagne invented the miniscules). Uppercase still has its
role in situations of special emphasis, e.g. "max", "Max", "MAX", but it
would loose that benefit if it were used by default.
However, if someone tells me that my naming scheme will potentially cause
errors, rather than just annoy people
Annoyance only starts when people try to combine several independent
theory libraries into bigger coherent applications.
Until recently, hardly anything was done in this respect, apart from the
main libraries that are shipped with Isabelle (main HOL and HOL/Library).
I am pleased to see that in recent years, some AFP articles have started
to aggregate, and build up beginnings of modest dependency structures.
But I don't want to change my naming scheme without knowing what the
rules are because there are lots of different objects, in particular, in
addition to theorem names, there are locales, classes, and sublocales,
which I see that I may need now.
As a general principle in Isabelle, "different objects" don't differ in
the naming convention, but make them coincide as far as sensible, even
with the actual names. Each category of a separate name space, so you
normally you don't have a dog "foo_dog", cat "foo_cat", mouse "foo_mouse",
but dog "foo", cat "foo", mouse "foo".
In practice, this could mean class "nat", type "nat", const "nat", theorem
"nat". Fine points need to be observed when different categories appear in
clusters: lets say some type "nat" and some const "nat" that both produce
some theorem "nat.induct", which would then clash in the common theorem
This archive was generated by a fusion of
Pipermail (Mailman edition) and