[isabelle-dev] Datatype alt_names

[Florian Haftmann]

Am 03.11.2010 16:26, schrieb Tobias Nipkow:
>>> 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.
> 
> It is, and one of the reasons is that the default abs/rep names can be
> quite confusing (eg: which one is which?). I don't think we should get
> rid of it.

Yes, we have to disinguish the "alternative name" of typedefs
(immediately in parnethesis after the typedef keyword), which is still
sometimes used (for what reasons ever), from the explicit morphisms
names, which are an integral part of the user interface, e.g.
considering multisets:

typedef 'a multiset = "{f :: 'a => nat. finite {x. f x > 0}}"
  morphisms count Abs_multiset

Here "count" is a regular user-space operation.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101103/82364e10/attachment.sig>