proof - 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删除来自 plus 的默认加号语法Groups 的类型类理论。

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

然后你可以使用

notation suma (infixl "+" 65)

添加您自己的语法。

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