如何定义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产品类型的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之间转换，并且由于这是一个全新的类型，所以可以为其提供类型类实例。

为了完整起见，使用语言环境实现类型类，并且您可以手动解释类型类语言环境，从类型类中为您提供所有定义和引理，但当然，与类类框架的集成不管用。首先，type × bool将不是排序semilattice_sup。不过，偶尔，这可能是一个可行的解决方案：

interpretation type_bool: semilattice_sup mysup myle myless 
proof 

（其中mysup，myle，myless是sup，≤，<为type × bool，你必须提供并证明它们符合公理的名称。当然是完全随意的，包括type_bool）