如何聲明類的類的「free」實例？

Question

我試圖在Isabelle/HOL中對一些程序分析建模。分析計算有界晶格中的值，但是（現在和一般性）我不想承擔任何具體的晶格定義;我所關心的只是一些結果是否最低。我正在尋找一種方法來聲明一個抽象類型，該類型是Isabelle/HOL的類型實例的一個實例，不需要提交具體實例。

也就是說，類似於我怎麼能寫

typedecl some_data 
type_synonym my_analysis_result = "var => some_data" 

其中some_data是完全免費的，我希望能夠寫類似

typedecl "some_lattice::bounded_lattice" 
type_synonym my_analysis_result = "var => some_lattice" 

其中some_lattice將是「自由「有界晶格除了滿足晶格定律外我什麼都不需要。這種特殊的語法不是由伊莎貝爾/ HOL接受，也不是像

type_synonym my_analysis_result = "var => 'a::bounded_lattice" 

我可以通過定義一個具體的數據類型，並使它成爲bounded_lattice一個實例解決這個問題，但我不明白爲什麼有不應該是一個更一般的方法。是否有一些簡單（或複雜）的語法來實現我正在做的事情？我必須（不知何故，我不確定它是否會起作用）將我的整個開發都放在context bounded_lattice區塊內？或者有什麼理由可以通過typedecl獲得完全免費的類型，但沒有按類型限制的免費類型？

Answer 1

如果類型類具有相互矛盾的假設，則將未指定類型作爲類型類的實例可能會引入不一致。爲了使這種公理性顯而易見，你必須對實例化進行公理化。這裏有一個例子：

typedecl some_lattice 
axiomatization where some_lattice_bounded: 
    "OFCLASS(some_lattice, bounded_lattice_class)" 
instance some_lattice :: bounded_lattice by(rule some_lattice_bounded) 

注：幾年前，你也可以使用命令arities，但這已經停產強調未指定類型的類實例化的公理性質。

或者，您可以爲格子使用類型變量。這是更靈活的，因爲如果你需要一個具體的有界格，你可以稍後實例化類型變量。但是，您必須始終攜帶該類型變量。例如，

type_synonym 'a my_analysis_result = "var => 'a" 

Isabelle不支持使用排序約束的類型同義詞（因爲無論如何都沒有多大意義）。如果添加排序約束，您將收到一條警告消息，即將被忽略。無論何時需要bounded_lattice實例，類型推斷都會添加排序約束（或者必須爲類型變量顯式提及）。