关于 Isabelle 中的子类型的问题在这里非常冗长。所以我的简单问题是，如果我将 A 定义如下，我如何将类型 B 定义为 A 的子类型：
typedecl A
通过这样做，我想让 B 类型的元素可以访问在 A 上定义的所有操作和关系（它们未在此处打印）。
一个更复杂的例子是将 B 和 C 定义为 A 的子类型，这样 B 和 C 是不相交的，并且 A 的每个元素要么属于 B 类型，要么属于 C 类型。
谢谢
Isabelle 没有子类型，尽管可以模拟子类型的某些方面，如另一个线程中所述。如果您想对不同类型使用相同的操作，您可能需要查看 Isabelle 的类型类。