我想了解 Isabelle/HOL 亚型。我在对我最后一个 SO 问题的部分回答中解释了为什么它对我很重要：
基本上，我只有一种类型，所以如果我可以通过子类型利用 HOL 类型的力量，这可能对我有用。
我在 Isabelle 文档、Web 和 Isabelle 邮件列表中进行了搜索。使用了“子类型”这个词，虽然不多，而且它似乎不是 Isabelle 词汇表中非常重要的一部分。
部分地，我只想知道如何正确使用“子类型”这个词。我不想在 Isabelle 中将某些不是子类型的东西称为子类型。
根据 Wiki，子类型是特定于语言的：
https://en.wikipedia.org/wiki/Subtyping
有人可以给我一个创建 Isar 子类型的 Isar 命令列表吗？我正在调查typedef，正如上面链接的问题中所解释的那样。我倾向于称其为子类型，但isar-ref.pdf在解释命令时不使用“子类型”。
如果还有其他方法可以创建 Isabelle/HOL 子类型，我想知道。
Isabelle/HOL 没有可替代性意义上的亚型。这意味着如果你需要一个类型的值a，那么你必须提供一个类型的值a——你不能与不同的类型相处b。特别是，Isabelle 没有子类型的概念，其中子类型的值满足某些附加属性。
有一些方法可以模拟子类型的某些方面，这就是使用概念子类型的地方：
类型参数的替换有时会让您产生子类型化的错觉。该record包使用它来扩展记录，以便可以使用扩展记录q代替非扩展记录r。在内部， 的附加字段被填充到记录类型q泛化的附加类型参数中。r从技术上讲，没有发生亚型多态性。因此，扩展记录的顺序很重要。
typedef引入了一种新类型t，其类型全域是某些现有 HOL 类型值的非空子集a。有时，这被称为t是 的子类型a，但您不会获得可替代性。Rep_t当您想将 的值t用作 之一时，您总是必须明确提及嵌入态射a。不管你是用typedef还是通过其他方式定义你的类型，任何单射函数都可以作为这样的强制。
Isabelle 参考手册（第 12.4 节）中描述的强制子类型使 Isabelle 自动推断和插入此类强制。这只适用于类型和子类型都是没有参数的类型构造函数。用于declare [[coercion_enabled]]启用强制子类型化并使用declare [[coercion Rep_t]]. 因此，您不必自己插入嵌入函数。