如何定義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）