[isabelle-dev] Datatype alt_names

[Makarius]

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?
>>
>>        Florian
>
> I brought up this issue on the mailing list last year:
>
> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2009-May/000578.html
>
> 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 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2010-October/001105.html

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 
plane either.)

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 
gradual deletion.


> 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.


 	Makarius