如何定义 type_synonym 的 class 实例？

Question

type 是 semilattice_sup 的实例 class:

datatype type = BType | IType | AType

instantiation type :: semilattice_sup
begin
end

我也在尝试将 type × bool 类型声明为此 class 的实例：

type_synonym stype = "type × bool"

instantiation stype :: semilattice_sup
begin
end

但是我得到以下错误：

Bad type name: "stype"

如何定义 type_synonym 的 class 实例？

Answer 1

你不能。事实上，在 HOL-Library Product_Order 中，是已经有一个 semilattice_sup 的产品类型实例，所以如果 type 有一个 semilattice_sup 实例，那么 type × bool 也是如此（如果您包括 Product_Order。请注意，这是逐点顺序，而不是字典顺序。

如果您需要其他顺序或非常适合您的类型的东西，您还可以使用 typedef:

定义一个全新的类型

typedef type' = "UNIV :: (type × bool) set"
  by auto

这给你态射 Abs_type' 和 Rep_type' 在 type' 和 type × bool 之间转换，因为这是一个全新的类型，你可以提供类型 class 个实例。

为了完整起见，type classes 是用 locales 实现的，您可以手动解释 type class locale，为您提供 type [=45] 的所有定义和引理=]，当然，与类型 class 框架的集成将不起作用。首先，type × bool 不会是 semilattice_sup 那种类型。偶尔，这仍然是一个可行的解决方案：

interpretation type_bool: semilattice_sup mysup myle myless
proof

（其中 mysup、myle、myless 是 sup、≤、< for type × bool，其中你必须提供然后证明它们满足公理。名称当然是完全任意的，包括 type_bool)

如何定义 type_synonym 的 class 实例？

How to define a class instance of type_synonym?

isabelle