isabelle - 隐藏运算符以避免 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删除现有的符号。在伊莎贝尔/霍尔，++绑定(bind)到 map_add从歧义警告中可以看出。您可以按如下方式删除它。

no_notation map_add (infixl "++" 100)

请注意，您必须重复声明要删除的符号的确切优先级参数。找到常量的符号声明没有简单的方法，但是声明符号接近常量的声明是一种很好的风格；按住 Ctrl 键单击一个常量会将您带到它的声明处。

关于 : , 默认绑定(bind)到 Set.member .您可以使用 no_notation Set.member ("(_/ : _)" [51, 51] 50) 删除它.

除非出于演示或探索目的，我建议不要过多更改 Isabelle 的默认语法。否则，其他 Isabelle 用户将难以阅读您的代码，您的理论将无法与其他人兼容。原因是在导入不同的理论时，符号会相加合并。因此，如果您删除符号 ++对于 map_add理论上 A和理论 B导入理论 A以及源自 Main 的其他一些理论但不是 A , 那么 ++ 的歧义回到理论上 B .