isabelle - 在 Isabelle 中引入类型缩写

Question

我知道如何在 Isabelle 中制作“术语缩写”，但我可以制作行为相同的“类型缩写”吗？

我可以定义一个“术语缩写”使用

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 中编写解析翻译。这方面的例子可以在 JinjaThreads 中找到。在 AFP 中(搜索 print_translation)。