[isabelle-dev] Datatype alt_names

[Brian Huffman]

On Wed, Nov 3, 2010 at 8:17 AM, Makarius <makarius at sketis.net> wrote:
> On Wed, 3 Nov 2010, Brian Huffman wrote:
>> The 'typedef' command supports a similar option for alternative names;
>> I am sure that it was originally created for use with non-alphanumeric
>> type names. One could also ask whether the existence of this feature
>> for typedef is still justified, when all types have regular names now.
>
> Do you mean the alternative names for the morphisms?  It is probably the
> standard example of explicit specification of derived names according to
> Florian's thread above.  IIRC, the "morphisms" specification is occasionally
> used in user definitions within theories, too.

No, I am not talking about the "morphisms" option; I meant the
optional name specified in parentheses. Consider this typedef command
from an old version of HOLCF:

typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep
(a::'a) (b::'b)}"

The name "Sprod" sets "Rep_Sprod" and "Abs_Sprod" as the default names
for the morphisms (which could just as well be done with the
"morphisms" option). It also gives the name "Sprod" to the defined
set, and causes the generated theorem names to be qualified with
"Sprod".

I am guessing that the original motivation for this feature is the
same as the reason for the similar feature in the datatype package: to
support non-alphanumeric type names like "**".

- Brian