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

Question

我试图类比来定义以下函数：

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？或者如何定义所需的构造函数？

Answer 1

并非每种类型都是由免费构造函数构建的。集合 '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 monad 和函数 Option.bind 进行排序来避免参数中的所有 option。

Answer 2

添加到 Andreas 的回答中，Isabelle/HOL 中的类型定义总是对某些底层基类型取模。例如。整数被定义为自然数对的商。

最初在此类类型上定义函数的典型方法是直接通过从类型定义中获得的态射，它在基础基类型和新类型（通常类似于 Abs_mytype 和 Rep_mytype) 或通过 lift_definition，它允许您直接将函数从基本类型提升到新类型。

但是，对于 int 和 real 这样的库类型，这是不可取的。你不应该窥视这些类型的内部表示，而只是抽象地使用它们，就像你在“普通”的纸笔数学中一样。

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

How to find constructors of a datatype?

isabelle