什么是Isabelle/HOL的子类型？哪些Isar命令会生成子类型？

Question

什么是Isabelle/HOL的子类型？哪些Isar命令会生成子类型？

8

我想了解Isabelle/HOL的子类型。我在上一个SO问题的部分答案中解释了为什么这对我很重要：

基本上，我只有一个类型，所以如果我可以通过子类型利用HOL类型的功能，那对我可能会很有用。我已经在Isabelle文档、Web和Isabelle邮件列表中进行了搜索。虽然“subtype”一词被使用，但并不多见，而且似乎并不是Isabelle词汇的一个非常重要的部分。部分原因是，我想知道如何正确地使用“subtype”这个词。我不想在Isabelle中称某些东西为子类型，而它实际上不是子类型。根据Wiki，子类型化是语言特定的：

https://en.wikipedia.org/wiki/Subtyping

重要的最后一部分; 请提供命令

有人能给我一个创建Isar子类型的Isar命令列表吗？我正在调查上面链接的问题中解释的typedef。我倾向于称之为子类型，但isar-ref.pdf在解释该命令时没有使用“subtype”。

如果有其他创建Isabelle / HOL子类型的方法，我想知道。

- user2190811

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Andreas Lochbihler · Accepted Answer

Isabelle/HOL中没有子类型的概念，也就是说，如果您需要一个a类型的值，则必须提供一个a类型的值-您不能使用不同的类型b。特别地，Isabelle没有子类型的概念，其中子类型的值满足某些附加属性。

有一些方法可以模拟子类型的某些方面，这就是子类型的概念所使用的地方：

类型参数的替换有时可以创造子类型的幻象。 record 包使用这个方法扩展记录，使得可以用扩展后的记录 q 替代非扩展的记录 r。在内部，q 的附加字段被塞入 r 记录类型的泛化的一个附加类型参数中。从技术上讲，没有子类型多态发生；因此，扩展记录的顺序很重要。
typedef 引入一个新类型 t，其类型宇宙是某个现有 HOL 类型 a 的值的非空子集。有时，这被称为 t 是 a 的子类型，但你不能得到可替换性。当你想将 t 的值之一用作 a 的值时，你必须明确地提到嵌入态射 Rep_t。无论你是用 typedef 还是其他方式定义你的类型，任何单射函数都可以作为这样的强制转换。
在 Isabelle 参考手册 (第 12.4 节) 中描述的强制子类型化使 Isabelle 自动推断和插入这样的强制转换。这仅在类型和子类型都是没有参数的类型构造函数时才有效。使用 declare [[coercion_enabled]] 来启用强制子类型化，并使用 declare [[coercion Rep_t]] 注册你的强制转换函数。因此，你不必自己插入嵌入函数。