overloading - 在 Isabelle 中定义重载常量

Question

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

例如，我可能想定义一个函数 is_default带类型 '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 reference manual 中的“常量和定义”部分获得。 .此外，还有一篇论文 "Conservative Overloading in Higher-Order Logic"作者 Obua 讨论了在不牺牲稳健性的情况下拥有这样一个框架的一些实现细节和陷阱。