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)I get 时"Suc (Suc (Suc 0))" :: "nat"，这意味着 Isabelle 仍在使用来自 Nat 的加号定义。我怎样才能让它使用我对 + 的新定义？

谢谢

Answer 1

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

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

然后你可以使用

notation suma (infixl "+" 65)

添加您自己的语法。

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