[isabelle-dev] Declaration depending on user proofs
makarius at sketis.net
Tue Nov 2 15:06:53 CET 2010
On Thu, 7 Oct 2010, Florian Haftmann wrote:
> To declare something as a type mapper, the following command could be
> type_mapper map_k
> which would issue an appropriate declaration. Attributes are
> inappropriate here since the user cannot be expected to write down the
> theorems to prove explicitly.
This looks like the standard solution, i.e. you have a command of the
"interaction type" theory_to_proof, the framework asks the user to produce
a proof, the tool applies the final result to the context.
The wording is also quite standard: a substantive that names the main
concept "type_mapper", without mentioning the "proof" in the name, because
that is already part of the Isar proof syntax (via "proof ... qed" or
> However I am always reluctant to introduce new keywords, both for
> aesthetic and technical reasons. So I am asking myself whether we
> should introduce a command for generic user-proof-dependent
> declarations, e.g.
> prove <args>
> Here different parsers could be registered under the umbrella of the
> same command. Some possible instances:
> prove type_mapper: map_l
> prove isomorphism: Fset.Fset Fset.member
> Any opinions?
So what are the "aesthetic and technical reasons" here?
There are a few caveats when introducing new commands, but this should not
invalidate the whole idea.
* Proof General requires pre-compiled keyword tables. This artifact
will disappear together with the PG interaction model in the near
* Newly defined commands can only be used in a later theory node. This
restriction is still there in the Isabelle/Scala document model: it
allows to gain precious microseconds of performance by interleaving
outer syntax parsing and command execution in a liberal way.
* Command keywords are a scarce global resource with a danger of clashes
with popular names already used as identifiers in user theories.
This is not really a problem if some guidelines for command names are
. Relatively long and explicit command names, separate words with
underscore instead of "multi part" commands.
The agglomerated my_tool_foo scheme is also more convenient for
users due to command keyword completion (which normally works
except for some Emacsen on Mac OS X).
. Very short command names should be avoided, or require at least
3 rounds of rethinking.
More information about the isabelle-dev