如何查找数据类型的构造函数？

我特林与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

如何查找数据类型的构造函数？

回答

相关问题