On Wed, 3 Nov 2010, Brian Huffman wrote:
On Wed, Nov 3, 2010 at 5:56 AM, Florian Haftmann
<[email protected]> 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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
