如何定义type_synonym的类实例？

Question

type是semilattice_sup类的一个实例：

datatype type = BType | IType | AType

instantiation type :: semilattice_sup
begin
end

我还试图将type × bool类型声明为该类的一个实例：

type_synonym stype = "type × bool"

instantiation stype :: semilattice_sup
begin
end

但我得到了以下错误：

Bad type name: "stype"

如何定义type_synonym的类实例？

Answer 1

实际上，在HOL中的Product_Order中已经有一个产品类型的Product_Order实例，所以如果type有一个semilattice_sup实例，那么type × bool也有(如果包括Product_Order )。请注意，这是点序，而不是字典顺序。

如果您需要另一个订单或与您的类型非常特定的东西，您也可以用typedef定义一个全新的类型。

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

这使您可以使用Abs_type'和Rep_type'来在type'和type × bool之间进行转换，而且由于这是一个全新的类型，所以您可以为它提供类型类实例。

为了完整起见，类型类是用locales实现的，您可以手动解释类型类区域设置，给出类型类的所有定义和引理，但当然，与类型类框架的集成将无法工作。首先，type × bool不会像semilattice_sup那样。不过，偶尔，这也是一个可行的解决方案：

interpretation type_bool: semilattice_sup mysup myle myless
proof

(其中mysup、myle、myless是sup、≤、< for type × bool，您必须提供这些信息，然后证明它们符合公理。当然，名字是完全任意的，包括type_bool)