如何查找數據類型的構造函數？

我特林與this one定義類推以下功能：如何查找數據類型的構造函數？

fun int_divide :: "int option ⇒ int option ⇒ real option" where 
    "int_divide _ (Some (int 0)) = None" 
| "int_divide (Some a) (Some b) = Some (a/b)" 
| "int_divide _ _ = None" 

fun real_divide :: "real option ⇒ real option ⇒ real option" where 
    "real_divide _ (Some (real 0)) = None" 
| "real_divide (Some a) (Some b) = Some (a/b)" 
| "real_divide _ _ = None"

但這些類型沒有int或real構造。 int和real類型被定義爲quotient_type。我找不到在理論上看起來像構造函數的東西。

下面的定義不工作：

definition int0 :: "int" where 
    "int0 = Abs_Integ (0,0)" 

fun int_divide :: "int option ⇒ int option ⇒ real option" where 
    "int_divide _ (Some int0) = None" 
| "int_divide (Some a) (Some b) = Some (a/b)" 
| "int_divide _ _ = None"

如何找到一個類型的所有構造函數？或者至少對於quotient_type？或者如何定義所需的構造函數？

來源

2017-08-29 Denis

不是每個類型都是從免費構造函數構建的。套'a set和真實real沒有。當然可以顯示同構並將其聲明爲構造函數，例如在集合'a set和謂詞'a => bool之間，但是這對定義函數和證明沒有用處。

您可以使用ML塊查找已註冊構造函數的類型。例如，以下顯示nat的構造函數。

ML ‹Ctr_Sugar.ctr_sugar_of @{context} @{type_name nat} |> Option.map #ctrs›

用戶定義的構造可使用free_constructors，其在tutorial on (co)datatype definitions（可從文檔面板）記錄中註冊。

我已經說過了，我不認爲在試圖爲各種數字類型定義自由構造函數方面有很多要點，因爲您還必須證明有關數字上的所有操作如何表現w.r.t.對這些新的構造函數。這是很多工作。這可能是更容易只是使用條件，而不是模式匹配的，說

fun int_divide :: "int option ⇒ int option ⇒ real option" where 
    "int_divide (Some a) (Some b) = (if b = 0 then None else Some (a/b))" 
| "int_divide _ _ = None"

另一個建議是使用option單子和排序功能Option.bind避免一切option S IN的參數。

來源

2017-08-29 08:13:41

添加到Andreas的答案中，Isabelle/HOL中的類型定義總是以某種基礎基類型爲模。例如。整數被定義爲自然數對的商。

上這樣的類型定義函數的典型方式起初是直接通過從類型定義獲得態射，其下面的基底的類型和新的類型（通常像Abs_mytype和Rep_mytype）或通過lift_definition之間進行轉換，它允許你直接將一個函數從基類型提升到新類型。

但是，對於像int和real這樣的庫類型，這不可取。你不應該偷看這些類型的內部表示，而應該抽象地使用它們，就像你在'普通'筆和紙的數學中一樣。

來源

2017-08-29 14:06:58

如何查找數據類型的構造函數？

回答

相關問題