overloading - 在 Isabelle 中定义重载常量

Question

如何在 Isabelle 中定义一个函数，该函数根据其参数的类型或使用它的上下文的类型而具有不同的定义？

例如，我可能想is_default用 type定义一个函数'a ⇒ bool，其中每种不同的类型'a都有一个可能不同的“默认值”。（为了论证，我还假设现有的概念如zero不合适。）

Answer 1

Isabelle 通过定义一个常量名称，然后为该常量提供不同类型的新定义来支持重载定义。这可以通过consts定义常量名的命令，然后defs (overloaded)提供部分定义的命令来完成。

例如：

consts is_default :: "'a ⇒ bool"

defs (overloaded) is_default_nat:
  "is_default a ≡ ((a::nat) = 0)"

defs (overloaded) is_default_option:
  "is_default a ≡ (a = None)"

上面的方法在没有参数的情况下也可以工作(overloaded)，但会导致 Isabelle 发出警告。

该defs命令还被赋予了一个名称，它是由 Isabelle 生成的包含定义的定理的名称。然后可以在以后的证明中使用此名称：

lemma "¬ is_default (Some 3)"
  by (clarsimp simp: is_default_option)

Isablle/Isar 参考手册中的“常量和定义”部分提供了更多信息。此外，Obua的一篇论文“Conservative Overloading in Higher-Order Logic”讨论了一些实现细节和在不牺牲可靠性的情况下拥有这样一个框架的问题。

Answer 2

这种重载看起来非常适合类型类。首先，您为所需的功能定义一个类型类is_default：

class is_default =
  fixes is_default :: "'a ⇒ bool"

然后你引入任意实例。例如，对于布尔值

instantiation bool :: is_default
begin
definition "is_default (b::bool) ⟷ b"
instance ..
end

并列出

instantiation list :: (type) is_default
begin
definition "is_default (xs::'a list) ⟷ xs = []"
instance ..
end