The Theorem keyword is a prettier way of writing `store_thm`, which, as the
name suggests, is indeed for theorems. In other words, the choice of Theorem
merely reflects our existing naming convention.
If you have a lemma that shouldn’t be “stored”, then you should probably be
using `Q.prove` (or `prove`). The use of theory files that make theorem values
persistent is the way in which users can distinguish important results that
should persist (that is, “theorems”), and those that should be more ephemeral.
The existing `save_thm` entrypoint has the same problem with requiring
redundant typing of names. I’m thus tempted to invent a Theorem analogue to map
to it. My current feeling is to go for something like
Theorem(calculated) thmname (ML code);
Or
Computed_Theorem thmname (ML code)
Or …?
Suggestions welcome.
Michael
From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
Date: Thursday, 3 January 2019 at 23:20
To: Makarius <makar...@sketis.net>
Cc: Michael Norrish <michael.norr...@data61.csiro.au>, hol-info
<hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] New grammar of defining theorems?
So the key is to make sure that they’re not distinguished internally by some
tools, and if some tools do, it’s their problems but HOL’s.
I personally don’t like the keyword “Theorem” because I think many small
theorems with 3 lines of tactics do not deserve the name “Theorem”. The correct
way of using these conventions should be aligned with majority math books,
which I believe there must be some “rules” mentioned somewhere.
On the other side, HOL4 users always have multiple ways to build a theorem. For
example, sometimes I perfer using “save_thm” to build theorems forwardly and
put the statement as comments before it, sometimes multiple theorems were put
into a “local” block sharing common tactics. As a result, HOL4 proof scripts
were *not* documents but essentially raw ML programs, thus extremely flexible.
I may not adopt this new grammar in a complex proof script in which different
ways of building theorems were used together.
—Chun
P. S. Coq seems to have even more synonyms: (do Coq users here share the same
concerns?)
Lemma ident [binders] : type.
Remark ident [binders] : type.
Fact ident [binders] : type.
Corollary ident [binders] : type.
Proposition ident [binders] : type.
These commands are synonyms of Theorem ident [binders] : type.
Il giorno 03 gen 2019, alle ore 12:23, Makarius
<makar...@sketis.net<mailto:makar...@sketis.net>> ha scritto:
On 03/01/2019 11:23, Chun Tian (binghe) wrote:
Hi Michael,
thanks for fixing the bugs. (now I see why I can’t find its definition…)
Going in this direction, have you considered adding also “Lemma” and
“Corollary”? Internally they're equivalent with “Theorem”, but they could
literally help writers (and readers) identifying different levels of theorems,
like those in math books.
This reminds me of Isabelle/Isar. Some decades ago I introduced these
variants of 'theorem' and it became a running gag of confusion and
unclear corner cases, because aliases were not really identical, but
distinguished internally by some tools.
Recently, we even introduced 'proposition' as another variant, but it is
unclear if it is more prominent than 'theorem' or less prominent than
'lemma'. Thus it depends on local conventions of particular
formalization projects how to treat it, e.g. in document presentation.
If I had another chance today, I would probably eliminate all funny
aliases of Isar commands.
Makarius
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
