介绍伊莎贝尔的类型缩写

Question

我知道如何在Isabelle中创建"term缩写"，但是我能创建以相同方式运行的"type缩写"吗?

我可以使用

定义一个"term缩写"

abbreviation "foo == True"

以后在输出中出现的所有True都将被打印为foo。例如，命令

term "True ⟶ False"

输出"foo ⟶ False"。我想定义一个具有相同行为的"类型缩写"。我知道type_synonym命令，但是当我输入

时

type_synonym baz = "int list"

那么int list在未来输出中的出现是，而不是像我希望的那样用baz替换。如果它还没有以某种形式存在，我认为当定义的右侧相当笨拙时，type_abbreviation命令可能非常方便。

Answer 1

您可以声明类型的语法翻译，就像在引入abbreviation之前必须为术语做的那样。例如，下面使Isabelle将char list漂亮地打印为string。在MicroJava的Isabelle发行版中可以找到更多此类示例。

translations
  (type) "string" <= (type) "char list"

命令translations适用于类型缩写，其中每个类型变量在每一侧只出现一次。如果一个类型变量在右边多次出现，你必须用ML写一个解析翻译。这样的例子可以在AFP中的JinjaThreads中找到(搜索print_translation)。