推測一個相互遞歸的數據類型家族

Question

是否有可能使用quotient_type機制和一族等價關係對Isabelle/HOL中的一系列相互遞歸數據類型進行商數？

如果是這樣，那麼這個地方有沒有好的例子？搜索Isabelle文檔以及描述改進的quotient_type機制的文章並不是很有幫助。

Answer 1

命令quotient_type一次只能處理一種類型。如果你想在幾種相互類型上做一個商，你必須手動進行編碼和解碼，但這很簡單。

假設您的兩種類型是t1和t2，其等價關係爲r1 :: t1 => t1 => bool和r2 :: t2 => t2 => bool。然後，

quotient_type q = "t1 + t2"/"rel_sum r1 r2" 

是組合商類型。然後，您可以定義兩個商的預測：

lift_definition Abs1 :: "t1 ⇒ q" is "Inl" . 
lift_definition Abs2 :: "t2 ⇒ q" is "Inr" . 

typedef q1 = "range Abs1" by blast 
typedef q2 = "range Abs2" by blast 

隨着setup_lifting，您可以用升降包註冊q1和q2了。然後，您可以獲得體面的自動化以獲取證明和定義。您只需執行兩個提升步驟（首先從t1 + t2到q，然後從q到q1或q2）以獲取定義和兩個未舉證步驟。