Isabelle 中的运算符重载

Question

我想在 Isabelle 中使用 nat 类型，但我想重载一些现有的定义，例如加法。我写了下面的代码：

theory Prueba
imports Main HOL
begin

primrec suma::"nat ⇒ nat ⇒ nat" where
"suma 0 n = 0" |
"suma (Suc x) n = 0"
no_notation suma (infix "+" 65)

value "2 + (1 :: nat)"

我试图用一个始终输出 0 的新定义来重载加法。但是，当我评估 2 + (1 :: nat) 时，我得到 "Suc (Suc (Suc 0))" :: "nat"，这意味着 Isabelle 仍在使用 Nat 的 plus 定义。我怎样才能让它使用我对 + 的新定义？

谢谢

Answer 1

您必须使用 no_notation 删除来自 Groups 理论的 plus 类型 class 的默认加号语法。

no_notation Groups.plus_class.plus (infixl "+" 65)

然后你可以使用

notation suma (infixl "+" 65)

添加您自己的语法。

（我从来没有尝试过推翻定义的这些基本部分。我想这可能会导致奇怪的情况——尤其是对于其他人之后试图使用你的理论。）

Isabelle 中的运算符重载

Operator overloading in Isabelle

proof

isabelle