隐藏运算符以避免 AST 中的歧义

Question

我正在尝试 Isabelle 官方教程中的列表示例。我将 # 替换为 :，将 @ 替换为 ++，以具有与 Haskell 相同的语法。现在我收到关于 AST 中歧义的警告。我知道我可以使用 hide_const 隐藏函数，但这不适用于中缀表示法中的运算符。如何在 Isabelle 中隐藏运算符？

确切的警告信息是：

Ambiguous input⌂ produces 2 parse trees:
  ("\<^const>HOL.Trueprop"
    ("\<^const>HOL.eq" ("\<^const>Map.map_add" ("/<^const>toylist.list.Nil") ("_position" ys))
      ("_position" ys)))
  ("\<^const>HOL.Trueprop"
    ("\<^const>HOL.eq" ("\<^fixed>app" ("\<^const>toylist.list.Nil") ("_position" ys)) ("_position" ys)))
Fortunately, only one parse tree is well-formed and type-correct,
but you may still want to disambiguate your grammar or your input.

Answer 1

您可以使用命令 no_notation，它采用与命令 notation（或在常量定义中）的符号声明期间使用的相同参数。

符号:和++已经分别被Set.member和map_add使用。所以你必须找到这些符号声明并在 no_notation:

中使用它们

no_notation Set.member ("(_/ : _)" [51, 51] 50)
no_notation map_add (infixl "++" 100)

然后您可以按照您肯定已经采用的相同方式继续操作，并删除 list 现已过时的语法：

no_notation Cons (infixr "#" 65)
notation Cons (infixr ":" 65)

no_notation List.append (infixr "@" 65)
notation List.append (infixr "++" 65)

term "x : (xs ++ ys)"

Set.member : 的符号不会真的错过，因为已经有 xsymbol/utf-8 符号 ∈。我认为 map_add 没有那么常用，但您可以使用免费符号 @。

Answer 2

隐藏运算符不会删除其符号。有一个单独的命令 no_notation 可以删除现有的符号。在Isabelle/HOL中，++绑定到map_add，从歧义警告可以看出。可以按如下删除。

no_notation map_add (infixl "++" 100)

请注意，您必须重复声明要删除的符号所使用的确切优先级参数。没有简单的方法可以找到常量的符号声明，但是在常量声明附近声明符号是一种很好的风格； Ctrl-单击常量会转到它的声明。

关于:，这默认绑定到Set.member。您可以使用 no_notation Set.member ("(_/ : _)" [51, 51] 50).

删除它

除非是为了演示或探索目的，否则我建议不要过多地更改 Isabelle 的默认语法。否则，其他 Isabelle 用户将难以阅读您的代码，并且您的理论将与其他人的不兼容。原因是当导入不同的理论时，符号会加法合并。因此，如果您在理论 A 中删除 map_add 的符号 ++ 并且理论 B 导入理论 A 和从 [=22= 派生的一些其他理论] 但不是 A，那么 ++ 的歧义在理论上又回来了 B。

隐藏运算符以避免 AST 中的歧义

hiding operators to avoid ambiguities in the AST

isabelle