On Thu, 7 Oct 2010, Florian Haftmann wrote:
To declare something as a type mapper, the following command could be
introduced
type_mapper map_k
<proof>
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
simiular).
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>
<proof>
Here different parsers could be registered under the umbrella of the
same command. Some possible instances:
prove type_mapper: map_l
<proof>
prove isomorphism: Fset.Fset Fset.member
<proof>
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
future.
* 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
followed:
. Relatively long and explicit command names, separate words with
underscore instead of "multi part" commands.
E.g.
my_tool_foo
my_tool_bar
my_tool_blah
instead of
my_tool foo
my_tool bar
my_tool blah
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.
Makarius
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
