Introducing type abbreviations in 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.

Answer 1

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