Title: Introducing type abbreviations in Isabelle
Tags: isabelle
Question: I know how to make "term abbreviations" in Isabelle, but can I make "type abbreviations" that behave in the same way?
I can define a "term abbreviation" using
abbreviation "foo == True"
Henceforth all appearances of True in the output will be printed as foo. For instance, the command
term "True ⟶ False"
outputs "foo ⟶ False". I would like to define a "type abbreviation" that has this same behaviour. I know about the type_synonym command, but when I type
type_synonym baz = "int list"
then appearances of int list in future output are not replaced with baz as I would like them to be. If it doesn't already exist in some form, I think a type_abbreviation command could be quite handy when the right-hand side of the definition is rather unwieldy.
Comment: @chris Mm, good point, I guess `'a seq` should stay a `type_synonym` rather than a `type_abbreviation`. As a counterexample, though, I think I'd always prefer to see `string` instead of `char list`.

Comment: By the way, one possible workaround that I'm aware of is to introduce a constructor, e.g. `datatype baz = Baz "int list"`. One can then tag terms with `Baz` to make Isabelle print the type as `baz` type rather than `int list`.

Comment: I don't think that there is a good solution. In general it is not clear when you really would like to replace types by their abbreviation. Of course the same holds for terms (but for terms ambiguities occur less frequently). E.g., when working on a theory on infinite sequences, I thought it was a good idea to use the abbreviation `'a seq` for `nat => 'a`. But would you really like to replace all occurrences of this type? I don't. Consider `nth 75b5:f2c1:f5d7:b954:8dc3:cee9:baf:a8c0 'a list => 'a seq`.

Here is the accepted answer: You can declare syntax translations for types just as it had to be done for terms before abbreviation was introduced. For example, the following makes Isabelle pretty-print char list as string. More examples of this kind can be found in the Isabelle distribution in MicroJava.
translations
(type) "string" <= (type) "char list"
The command translations works for type abbreviations where each type variable occurs exactly once on each side. If you have multiple occurrences of a type variable on the right hand side, you have to write a parse translation in ML. Examples of this can be found in JinjaThreads in the AFP (search for print_translation).


{'source': 'StackExchangeDataset', 'subset': 'stackoverflow.com', 'metadata': {'AnswerCount': 1, 'CommentCount': 3, 'ContentLicense': 'CC BY-SA 3.0', 'CreationDate': '2014:00:05/25/14', 'FavoriteCount': 1.0, 'PostTypeId': 1, 'Tags': '<isabelle>', 'Title': 'Introducing type abbreviations in Isabelle', 'ViewCount': 644, 'id': 23852843, 'user_AboutMe': "<p>I'm a computer scientist, doing research at Imperial College London.</p>\n", 'user_AccountId': 1374085.0, 'user_DisplayName': 'John Wickerson', 'user_Reputation': 1516.0, 'user_Views': 257.0, 'user_id': 1308444.0}}