[isabelle-dev] Declaration depending on user proofs

[Makarius]

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