[isabelle-dev] Datatype alt_names
makarius at sketis.net
Wed Nov 3 16:17:31 CET 2010
On Wed, 3 Nov 2010, Brian Huffman wrote:
> On Wed, Nov 3, 2010 at 5:56 AM, Florian Haftmann
> <florian.haftmann at informatik.tu-muenchen.de> wrote:
>> Traditionally the datatype command would accept optional "alternative
>> names" used in names of type-related facts etc., e.g.
>> datatype (foo) "/*/" = Bar
>> With all HOL types being regulary named, the question arises whether we
>> still have to keep that feature or shall just discontinue it?
> I brought up this issue on the mailing list last year:
> I have since removed a similar feature from the HOLCF domain package.
> It seems to me that such a feature could only be justified if it was
> needed for backward compatibility. But since this feature was broken in
> more than one released version of Isabelle, and nobody has ever
> complained about it, backward compatibility is not an issue for anyone.
On the old quoted thread above I suspected that it was motivated by
old-style unnamed types, such as "*" or "+". We have gotten rid of that
legacy recently, so that explanation is obsolete.
Grepping through the sources for alt_name right now, I get the impression
that there was a second motivation: make really sure that the synthesized
"big_rec_name" variations really work in the target context. Due to loss
of information in base_name, it could in principle clash with other names
bound in the same context. Thus it would be an answer to the conclusion
of the other thread on "liberal" bindings, see
I did not have time to comment on that issue so far -- it appeared to have
been closed while I am was still on vacation. The main fragility of such
"escape hatches" is that they are used very rarely, i.e. when they are
really needed they don't work. (I did not try the one on the Easyjet
Both the "liberal" auto rename feature, and the alt_name argument of many
existing packages are of the same kind here. Since alt_name has been
never used as far as I can remember, it might well be a candidate for
> 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.
More information about the isabelle-dev